Skip navigation
Please use this identifier to cite or link to this item:
Title: Deriving Abstractions to Address Hardware Platform Security Challenges
Authors: Subramanyan, Pramod
Advisors: Malik, Sharad
Contributors: Electrical Engineering Department
Keywords: abstraction
Subjects: Computer engineering
Computer science
Electrical engineering
Issue Date: 2017
Publisher: Princeton, NJ : Princeton University
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.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Electrical Engineering

Files in This Item:
File Description SizeFormat 
Subramanyan_princeton_0181D_12023.pdf1.4 MBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.