Stephen Beard will present his Pre FPO "Containment Architecture with Verified Output: A Model for Practical Trust in Real Systems" in CS 302 on Monday, August 14th at 1pm.
The members of his committee are as follows:
David August (advisor)
Andrew Appel (reader)
Jothy Rosenberg (Dover Microsystems) (reader)
Aarti Gupta (non-reader)
Arvind Narayanan (non-reader)
Everyone is invited to attend his talk. The talk abstract follows below:
Abstract:
All layers of today’s computing systems, from hardware to software, are vulnerable to attack. Market and economic pressure generally result in companies focusing on performance and features, leaving security and correctness as post deployment concerns. Thus, systems must frequently be patched or augmented after deployment to fix security vulnerabilities. While this non-virtuous exploit-patch-exploit cycle is not the most secure, it is practical enough for companies to use. Formal methods in both software and hardware can give true guarantees as to the security they provide. Ideally, modern systems would be comprised of entirely 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, are a major factor in clean slate solutions being unrealistic. Thus, a practical solution should rely on a few, simple components and should be adoptable incrementally.
As the first implementation of the Containment Architecture with Verified Output (CAVO) model developed at Princeton, TrustGuard 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, TrustGuard’s 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. The first extension is to make 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. The second extension is to give 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 similar to the way that the small, trusted Sentry can ensure correctness of execution of a large amount of complex, untrusted hardware.
