Stephen Beard will present his FPO, "TRUSTGUARD: A MODEL FOR PRACTICAL TRUST IN REAL SYSTEMS" on Tuesday, 5/21/2019 at 1:30pm in CS 301. The members of his committee are as follows: David August (adviser); Readers: Andrew Appel and Jothy Rosenberg (CEO Dover Systems); Examiners: Aarti Gupta and Arvind Narayanan. A copy of his thesis, is available upon request. Everyone is invited to attend his talk. The talk abstract follows below. 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.