How the Center of Excellence is Expanding the seL4 Ecosystem in the U.S.

Posted on January 6, 2021 by Matthew Russell

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:

seL4 Based Products – seL4 is more than just an academic product.

Dual personality phones

seL4 can enable dual personality phones.

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.

Military devices

seL4 can enable security in military devices.

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.

Medical equipment

seL4 can enable security in medical equipment.

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:

  • Remote equipment monitoring
  • Maintenance and update scheduling
  • Patches that fix problems before equipment breaks down

seL4 SDK

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.

seL4 Fundamentals – What makes seL4, seL4.

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:

  • Undefined behavior
  • Memory leaks
  • Buffer overflows
  • Null pointer dereferences (Pointer errors in general)
  • Arithmetic overflows and exceptions

The tutorial track at this year’s summit showed seL4 development in action by programming Pong on a seL4-based platform.

Platform Stacks leveraging seL4 – Security requires both secure hardware and software.

Two new seL4 platforms were covered at the CoE Summit:

  • Draper Laboratory’s ISP running seL4. A security co-processor that can enforce arbitrary security policies.
  • the seL4 microkernel can enable platforms on Microchip's PolarFire SOC Icicle Kit.

    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.

seL4 Features (and Requests) – Making seL4 even better.

The following seL4 features were discussed as potential drivers of secure product development:

  • One of the most interesting presentations was the introduction of IceCAP, which can leverages Trustzone on ARM v8.2 processors to take advantage of the secure world protections in seL4 without requiring a world switch. Even more impressive was the Rust Virtual Machine Monitor running on IceCap to launch Mirage OS microkernels.
  • Past seL4 development has been hampered by the lack of a common or standardized methods to extend the microkernel. Several presentations were given to discuss proposed solutions to this issue:
    • Driver API
    • Core Platform
    • Non-POSIX Application API
  • For many platforms a network stack is a necessary component, but also a large potential security vulnerability. Continuing with its previous work, Kestral is developing a Verified Network Stack to extend the assurance story of seL4 to include network functionality.
  • For yet other applications with strict timing requirements, seL4 provides several mechanisms for meeting these non-functional guarantees, which were covered in several presentations, such as:
    • Time Sliced Scheduling with the Domain Scheduler
    • Multiple Criticality Scheduler
  • One of the more unique feature requests at the summit was the desire to have a flat-address space version of seL4 with Memory Protection Unit support. While this would expand seL4 support to more lower end devices, since the seL4 proof depends on the more complicate Memory Management Unit, such a change would require adapting the proof and kernel to work using the limit windows provided by a MPU, but it could be an interesting competitor to the more barebones real-time executives such as FreeRTOS that usually run on these devices.

seL4 Foundation and CoE Governance.

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.

CSIRO Data61
seL4 Foundation
Linux Foundation

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:

  • Training
  • Outreach
  • Development/maintenance
  • Innovation

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.

Get Involved

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.

Matthew Russell
by Matthew Russell
Marketing Specialist
Matthew Russell is a marketing specialist at DornerWorks.