Skip navigation
Please use this identifier to cite or link to this item:
Title: System design and verification methodologies for secure computing
Authors: Li, Chunxiao
Advisors: Jha, Niraj K.
Contributors: Electrical Engineering Department
Keywords: Computer security
Embedded system security
Subjects: Computer engineering
Issue Date: 2012
Publisher: Princeton, NJ : Princeton University
Abstract: The security of computing systems can be threatened through compromise of system confidentiality, integrity, and availability. As the complexity, programmability, and network connectivity of computing systems increase, ensuring the security of these systems becomes more challenging. This thesis describes system design and verification methodologies for secure computing systems. These methodologies are built on the observation that despite the huge complexity of computing systems -- hardware, firmware, and various layers of software, many security-critical functions may depend on only a small subset of these components with careful system design. The security goals of confidentiality, integrity, and availability can be achieved by only protecting this subset. The thesis explores several computing system designs, in which security-critical functions are identified and analyzed for different threat models, and then isolated in a separate and trusted execution environment. For security-critical software running on embedded computing systems that interact with the physical world, such as medical devices, this thesis also introduces a novel approach of software verification at real-world interfaces. The thesis first discusses the security of software-defined radio and proposes an architecture based on robust separation of the radio operation environment from the user application environment, so that the security-critical functions for radio operation can be protected inside the radio operation environment. The thesis next discusses the security of virtual machine execution, and proposes an architecture that significantly reduces the size of the software components set that virtual machine execution depends on. The thesis also investigates the security of input/output interfaces for web applications, and separates them from a potentially compromised operating system or application. The thesis also explores attacks against and defenses for medical devices, and proposes methodologies to improve the trustworthiness of their security-critical software components with formal verification methods.
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 
Li_princeton_0181D_10438.pdf7.87 MBAdobe PDFView/Download

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