All layers of today’s computing systems, from hardware to software, are vulnerable to

attack. Market and economic pressure push companies to focus on performance and features, leaving security and correctness as secondary concerns. As a consequence, systems

must frequently be patched after deployment to fix security vulnerabilities. While this nonvirtuous exploit-patch-exploit cycle is insecure, it is practical enough for companies to use.

Formal methods in both software and hardware can guarantee the security they provide.

Ideally, modern systems would be comprised of formally verified and secure components.

Unfortunately, such methods have not seen widespread adoption for a number of reasons,

such as difficulty in scaling, lack of tools, and high skill requirements. Additionally, the

economics involved in securing and replacing every component in all systems, both new

and currently deployed, result in clean slate solutions being impractical. A practical solution should rely on a few, simple components and should be adoptable incrementally.

TrustGuard, the first implementation of the Containment Architecture with Verified

Output (CAVO) model developed at Princeton, showed how a simple, trusted Sentry could

protect against malicious or buggy hardware components to ensure integrity of external

communications. This was accomplished by ensuring the correct execution of signed software, with support from a modified CPU and system architecture. However, TrustGuards

practicality was limited due to its reliance on modified host hardware and its requirement

to trust entire application stacks, including the operating system.

The work presented in this dissertation seeks to make the CAVO model a practical solution for ensuring the integrity of data communicated externally in an untrusted commodity

system. This work extends CAVO in two ways. First, it makes the Sentry compatible with

a wide range of devices without requiring hardware modifications to the host system, thus

increasing its flexibility and ease of integration into existing environments. Second, it gives

developers the option to use trusted code to verify the execution of untrusted code, thus reducing the size of the trusted code base. This is analogous to the small, trusted Sentry

ensuring correctness of execution of a large amount of complex, untrusted hardware.