Deriving Abstractions to Address Hardware Platform Security Challenges

Abstract

Today's computing devices store and process an enormous amount of security-critical assets. These assets are a lucrative target for cybercriminals and protecting them from malicious actors remains a key challenge in computer security. Hardware is especially important in this context: security protections implemented in software may be invalidated by faulty hardware.

Ensuring hardware remains secure is becoming difficult. Deverticalization and globalization of the semiconductor industry have led to the separation of integrated circuit (IC) design houses from foundries and rendered ICs vulnerable to the threat of malicious design changes, i.e., hardware trojans. The emergence of systems-on-chip (SoC) designs, which comprise multiple programmable cores, firmware and application-specific accelerators, poses new verification challenges. In particular, verifying that SoC security requirements are met is challenging due to the need for co-verification of firmware and hardware.

This thesis first tackles the problem of algorithmic reverse engineering of digital circuits which can help analysts detect hardware trojans. We present a comprehensive portfolio of algorithms which analyze a flat unstructured netlist and output a high-level netlist with components such as register files, counters, adders and subtracters. Our techniques are fully-automated and scalable to designs with hundreds of thousands of gates.

Next, we present a methodology for system-level security verification of SoCs. The methodology is based on the construction of instruction-level abstractions (ILA). The ILA raises the level of abstraction of hardware modules to be similar to that of instructions in programmable processors. It can be used instead of the cycle-accurate and bit-precise hardware description for scalable co-verification of system-level security properties in SoCs. We introduce techniques to semi-automatically synthesize the ILA and show how it can be proven to be a correct abstraction of the underlying hardware. We then show how the ILA is used for security verification by designing a specification language and verification algorithm for information-flow properties.

In summary, this thesis presents a set of techniques to address security challenges in modern SoCs. In particular, it provides a methodology for verifying security of SoCs where security properties hold for the complete system, not just individual components such as the hardware or firmware alone.