Safe, Secure, High-Performance Hypervisor: Partitioning Approach to Isolating Untrusted Software

We will continue development of ARINC 653 extensions for Xen, completing time and space partitioning and adding the I/O subsystem (building on our prototype serial driver). We will use more automated tools for our formal methods analysis by collaborating with the Advanced Technology Center of Rockwell Collins. This should allow us to analyze more of the system than we previously considered. Our demonstration of the updated system will show multiple RTOS products running in the unprivileged domains. During this phase we will also move from PC-based development to actual embedded hardware representative of JTRS platforms. We will test the demonstration system by contracting with an independent security testing organization, who will attempt to break the system by adding malware to the partition running an open source application and then endeavor to breach the isolation barriers erected by the hypervisor to modify (or at least read) data in one of the safety-critical or highly secure partitions. We will also subject our certification artifacts to an independent audit by an FAA Designated Engineering Representative (DER) consultant, to confirm the safety of our system.