System design and verification methodologies for secure computing

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.