Researcher: Karl Crary
Research Area: Trustworthy Computing Platforms and Devices
Scope: In today's operating systems, protection is provided by dynamic checking, buttressed by hardware-based mechanisms. Roughly speaking, an operating system monitors the activities of applications, and if an application performs a disallowed operation (such as writing outside its address space), the application is terminated. We argue that the basic protection mechanisms of the operating system can instead be provided more reliably and flexibly by static checking of applications. Furthermore, such a static checking regime can be leveraged to go beyond basic protection and provide high confidence in the system's overall security. We propose to implement a static operating system based on these principles.
Outcomes: Specification of a security logic; a theoretic analysis and validation of the security logic; a prototype kernel implementation.