The operating system (OS) exercises complete control over applications, thus a compromise of the OS compromises every application. Software developers have little recourse to improve security in the face of system compromise---they cannot defend against OS vulnerabilities, nor can they reasonably substitute a secure version of the millions of lines of code that constitute a modern OS.
Rather than require applications to blindly trust OS interactions, this project investigates a system architecture that enables trusted applications to efficiently verify OS interactions with the help of a small, trusted hypervisor. Most verification work is performed within the C language runtime, minimizing changes to legacy code and shielding developers from increased programming complexity. The prototype system, called InkTag,improves upon prior work in several key areas: it provides more efficient techniques to verify system call results, implements usable access control for resources managed by an untrusted OS, and introduces hardware and software techniques to further reduce the size of the trusted computing base.
Cloud computing provides energy and economic efficiencies, but suffers from the inability to give meaningful security guarantees to hosted applications. This project demonstrates that system security is possible without trusting the OS---a large part of the hosted infrastructure. This project is also developing new materials for undergraduate and graduate curricula that combine core knowledge of systems with an understanding of how systems provide security properties, equipping future computer professionals with a better understanding of what security guarantees a system can meaningfully provide.
