Skip to main content

Designing Security Kernels for Verification

Researchers: Anupam Datta, Jonathan McCune

Research Area: Trustworthy Computing Platforms and Devices

Abstract

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.