seL4 is an attractive platform for building highly resilient systems, but to do so requires a fair degree of understanding of the technology. Fortunately, help is available from a growing number of community members offering products that ease system development and assurance, and provide training, consulting and development services around seL4.
The Foundation is working with members on developing certification schemes for services, training and products. Until these are in place, we provide interim endorsements, which are based on a fast and relatively shallow assessment. Interim endorsements are available to seL4 Foundation members only and will lapse once the (thorough) certification schemes are in place. We will support members with interim endorsements in achieving full certification. Certification will be open to anyone.
The certification (for now endorsement) will indicate:
Innovative companies are building products on a trusted software base with the guidance of DornerWorks engineers. As a founding member of the seL4 Foundation, DornerWorks can accelerate the integration of seL4 as the trusted software base for your products.
DornerWorks Ltd has received interim endorsement as a Trusted Service Provider for seL4-based systems.
Sydney-based company Breakaway Consulting offers consulting services on architecture, design and implementation of seL4-based systems. Through Founder and Managing Director Ben Leslie, Breakaway comes with 20 years of experience in L4 microkernels and systems based on various L4 kernels. Prior to founding Breakaway, Ben was a student with what is now the Trustworthy Systems Group, and then VP Engineering of Open Kernel Labs.
Breakaway Consulting has received interim endorsement as a Trusted Service Provider for seL4-based systems.
Cog Systems Inc
As the leading integrator of type-1 visualization solutions based on seL4, Cog leverages modularity to isolate critical functions and services on connected devices. All of this is available for the IoT market with the flexibility to run all applications effectively and securely.
Cog Systems Inc has received interim endorsement as a Trusted Service Provider for seL4-based systems.
HENSOLDT Cyber GmbH
In the development of high assurance systems with military grade security, HENSOLDT Cyber works intensively with the seL4 microkernel. As we aim to increase the usability of seL4 technologies, we develop user-friendly components bundled in the seL4 operating system TRENTOS, providing an easy-to-use basis for the development of embedded systems. We support our customers by guiding them with our seL4 experience and improving their development time by advising them on the correct application of the seL4 technologies.
HENSOLDT Cyber GmbH has received interim endorsement as a Trusted Service Provider for seL4-based systems.
Advanced Operating Systems at UNSW
COMP9424 “Advanced Operating Systems” (AOS) is a highly advanced course at UNSW Sydney, taught since 1997. Since 2011 the course has been based on seL4, and as of 2020, recordings of all seL4-related lectures are available on YouTube.
UNSW's AOS has received interim endorsement as seL4 training.
Note that this is a full-trimester course where students learn about microkernels in general, and seL4 in particular, in great detail. This means that the lecture material goes to much greater depth than is appropriate for a day- or week-long training session. Keep this in mind when trying to base your own training on AOS!
No product has been endorsed or certified at this stage.
Consider adding yours!
See process here.