The seL4 Center of Excellence (CoE) and the related seL4 CoE Summit make it easier for US-based developers to get training and development support for their own export-controlled projects. In turn, this accelerates the adoption of seL4 as a trusted base of software applications.
The third CoE Summit, the first to be held virtually, took place in November 2020 and covered new seL4 based products and platforms, additions to the seL4 feature set, and the future of the seL4 ecosystem.
Some of the highlights of the conference:
People travelling overseas might have previously needed multiple SIM cards or multiple devices to remain in touch with trusted contacts. Dual personality phones enable two SIM profiles on a single device. The trusted base provided by seL4 further ensures that sensitive data is not unintentionally transferred from one application or profile to another.
As more military devices are connected to the internet, the risk of data breach has grown. Where network-connected devices carry information on the location or status of troops in the field, seL4 provides a means of separating that classified data from open channels.
One way connected medical devices can be made more secure while maintaining market momentum is by separating critical software processes from non-critical ones and isolating communication channels between higher privileged domains. seL4 helps accomplish this by providing a trusted software foundation for medical devices. In turn, this makes life easier on both developers and users by providing a secure environment for:
The Trusted Entity Operation System software development kit (TRENTOS-SDK) developed by HENSOLDT Cyber contains everything a developer needs to create a seL4-based system that can secure applications running on an IoT network by isolating communication channels. Given the complexity of applying seL4 and its related proof to hardware platforms, SDKs are a popular choice of implementation as they greatly simplify the process.
Speakers at the CoE Summit gave an overview of the seL4 proof, which provides confidence to developers that core aspects of a system are actually secure. The binary code of the seL4 microkernel correctly implements the behavior described in its abstract specification and nothing more. This prevents:
The tutorial track at this year’s summit showed seL4 development in action by programming Pong on a seL4-based platform.
Two new seL4 platforms were covered at the CoE Summit:
Microchip’s PolarFire SoC – the first commercially available multi-core FPGA System-on-Chip that can support these mixed-criticality systems on open source Linux and the RISC-V Core IP from SiFive. It enables the determinism needed for real-time hardware applications, while living up to the interoperability promise of RISC-V. seL4 provides a trusted base for critical software components built on these devices.
The following seL4 features were discussed as potential drivers of secure product development:
The seL4 microkernel community has largely grown by online contribution through a wiki and Github. It was first developed in 2009 by CSIRO’s Data61, as a high-assurance, high-performance operating system microkernel.
The seL4 Foundation was created in the spring of 2020 under the greater Linux Foundation to, “Support the seL4 Foundation and community by providing expertise and services to increase community engagement, contributors and adopters, helping to take the OS ecosystem to the next level.” said Michael Dolan, VP of strategic programs for the Linux Foundation. “The open governance and standards-based model will provide a neutral, mature, and trustworthy framework to help advance an operating system that is readily deployable and optimized for security.”
This independent nonprofit seL4 Foundation aims to provide ongoing technical leadership, responsiveness, and support for the seL4 community.
The inaugural seL4 summit was held in 2018. The same year DARPA, in conjunction with Intelligent Automation Inc. and DornerWorks, formed the CoE as a US-based clearing house and ecosystem hub for seL4-related development efforts.
Now in its third year, the CoE has hosted separate summit events targeting US-based attendees. As seL4 is proving a valuable technology for the U.S. Armed Forces and NASA, the seL4 CoE has been and continues to be instrumental in providing resources for companies working on these projects.
The CoE currently supports four key components:
Having transitioned from a SBIR project to a stand-alone entity, the CoE is currently seeking members to further these goals, and hopes to select an initial board from these members in the next several months.
As one of the members of the seL4 Foundation and CoE, DornerWorks helps companies integrate the seL4 microkernel as the trusted software base for their products. Schedule a meeting with us when you are ready to enhance the security of your own systems. In the meantime, start using seL4 and contribute your own ideas, or sign up to become a member of the seL4 Foundation or seL4 CoE.
Chief Separation Technology Engineer Nathan Studer Contributed to this article.