Separation Kernel
In this Phase I and II SBIR (Small Business Innovation Research) project, our work had two goals: 1) reduce the cost of developing for and deploying high assurance, separation kernel-based systems, and 2) improve the assurance level achievable by separation kernel implementations.
The motivation is that today, both the per-unit cost and development cost of writing applications for separation kernels are prohibitive. Further, even though separation kernels have high assurance, there is demand for even higher-assurance software based systems. Better solutions are needed on both of these fronts.
The low cost part of the solution we proposed was to allow separation kernel application developers to defer their deployment platform selection until later in the development stage by making use of an open source Linux-based prototyping environment. We built on pre-existing open source components and tools to reduce the development cost of this prototyping environment. This allowed pre-operational capabilities to be demonstrated with minimal cost beyond developer time. This platform allows developers to demonstrate separation kernel capabilities earlier and will help to create a more cost- and feature-competitive marketplace for hardware and software selection.
Our approach to addressing the high assurance problem was to build a separation kernel with stronger evidence of correctness than any current product on the market. We accomplished this by building on work done by NICTA on the seL4.verified microkernel, which includes a complete code-level formal proof of correctness running on the ARM processor. We continue to work with NICTA on extending the microkernel and its proof so that it provides code-level proof of separation properties guided by the Separation Kernel Protection Profile.
