Secure Software Components Leveraging the seL4 Microkernel

The overall objective of this topic is to build applications that expand the ecosystem of secure software components around the seL4 operating system microkernel. The CTI/SU teams interpretation of this is broad, including an application primarily as a demonstration of the utility of a more fundamental expansion of the ecosystem: to release to the community, as open source, a minimized Trusted Computing Base (TCB) that strongly isolates VMs, supports capability based security and computer resource management, is amenable to independent formal verification and penetration testing, has been formally verified and penetration tested at least once, and facilitates mixed proof / factored security arguments where components vary in their trustworthiness and pedigree. The objective of Phase II is to develop secure software components together with a demonstration application, on top of seL4. The secure software components will be the Syracuse Assured Boot Loader Executive (SABLE) and the Genode operating system framework. The demonstration application will be the Geographically Aware & Target Secure Information Dissemination (GATSID) pub-sub-query DDS. The real impact is that developers are enabled to construct explicitly mixed-trust systems on a trustworthy base and administrators are enabled to assess objectively the trust they should repose in such systems.