Mixed Semiformal and Formal Modeling of Hypervisor Source Code for Security Property Understanding

Period of Performance: 06/03/2008 - 12/03/2008


Phase 1 SBIR

Recipient Firm

Luna Innovations, Inc.
301 1st St Suite 200
Roanoke, VA 24011
Principal Investigator


Luna Innovations Incorporated will work as part of the Naval Research Laboratory s hypervisor agile development team to advance the state of open source hypervisors. Namely, we will design, develop, and integrate a blend of semiformal and formal open source modeling tools for the purpose of understanding and verifying important security properties of both open source hypervisors and cross domain systems built upon them. All tools we develop or features we add will be open source and we will collaborate with NRL s other contractor partners.