Higher Assurance and Lower Cost Separation Kernels

We propose to build a separation kernel with stronger evidence of correctness than any current product on the market. We will do this by building on work done by Australia's National Information Communications Technology Research Center (NICTA), which includes a complete code-level formal proof of correctness of the L4.verified microkernel running on the ARM processor. Working with NICTA, we will build a system with the separation properties specified by the Separation Kernel Protection Profile (SKPP), and we will augment the proofs of correctness to include the separation properties. If the Common Criteria defined an EAL 8, this system would meet that level of assurance. To reduce the costs of developing and deploying software on a MILS platform, we will enable R & D customers to defer their deployment hardware/software platform selection until later in the development stage by developing an open source prototyping environment for separation kernel projects. We intend to make the set of tools freely available and open source. This should allow preoperational capabilities to be demonstrated with little-to-no cost beyond developer time. Delaying platform lock-in will create a more cost- and feature-competitive marketplace for hardware and software selection.