Researchers: Anupam Datta, Jonathan McCune
Research Area: Trustworthy Computing Platforms and Devices
Scope: Numerous hypervisors and security kernels have been developed recently both at CyLab and elsewhere with a focus on providing or enforcing security properties. A common focus during development has been small code size with the hopes that this will enable (at least partially) automated formal verification. The purpose of this project is to investigate effective mechanisms for verifying existing hypervisors, and, if necessary, to re-design a hypervisor to make the verification task easier.
Outcomes: We hope to achieve a result that enables us to verify one or more modular components of a security hypervisor with dramatically less manual effort than has been required in previous verification efforts. We may modify an existing hypervisor in the process, or engineer a new one.