Services, Training and Products
endorsed by the Foundation
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 establishing endorsement schemes for services, training and products. As a first step we started to 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 full endorsement scheme is in place, but we expect that all interim-endorsed services and products will achieve full endorsement, and will support the members to get there. The endorsement scheme will be open to anyone for a fee.
The endorsement indicates:
- that a particular service provider has the skills and experience to provide high-quality services to adopters of seL4;
- that a particular training program is of high quality and effective in providing useful skills for deploying the seL4 microkernel;
- that a particular product utilises seL4 capabilities correctly and is helpful to the community for building high-assurance seL4-based systems.
Service Providers
|
DornerWorks Ltd 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. |
|
Breakaway Consulting 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. |
|
UNSW Sydney The Trustworthy Systems (TS) team is the creator of seL4 and the seL4 Foundation, and for a long time was the sole source of support. With the seL4 Foundation now in place, and at its new home at UNSW, TS can now focus on seL4-related research and driving development, leaving engineering mostly to other ecosystem players. However, TS happy to take on research and consultancy contracts, as well as providing engineering (systems and verification) services when no commercial player is available. UNSW has received interim endorsement as a Trusted Service Provider for seL4-based systems. |
|
Proofcraft Pty Ltd Formal verification is what makes seL4 unique. With increasing uptake and adoption, seL4 is evolving, supporting more platforms, architectures, configurations, and features. An increasing number of high assurance systems are built with seL4 as a trustworthy foundation. As seL4 code evolves, so must its formal proofs. As more systems are built on seL4, there is an increased need to ensure correct configuration and initialisation, and correctness of critical components. Proofcraft is here to help. Founded by the seL4 verification leaders, it offers commercial support, verification projects, training and consulting on formal verification in general, and involving seL4 specifically. By applying mathematical machine-checked software verification, Proofcraft increases critical software systems' reliability, safety and security, for a verified future. Proofcraft has received interim endorsement as a Trusted Service Provider for seL4-based systems.
|
|
Kry10 Limited Kry10 offers support to enable seL4-based secure projects to be affordable, maintainable, and remotely manageable. Kry10 offers a full-featured operating system on top of the seL4 kernel, along with tooling, services, key management and more. The Kry10 Platform is a fast and easy way to build highly secure, next-generation cyber-physical devices. We leverage the verification of seL4 to bring you a secure, self-healing, truly dynamic system with minimal downtime, even during upgrades. Whether you are working on national assets, vehicles or sensors on a wall, you require deep confidence and easy to use tools. Come talk to us. Kry10 has received interim endorsement as a Trusted Service Provider for seL4-based systems. |
Training
|
|
Advanced Operating Systems at UNSW COMP9242 “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! |
|
|
TRENTOS training This course introduces the fundamental aspects of TRENTOS, a novel seL4-based secure embedded operating system developed by HENSOLDT Cyber. The course is split in a lecture part, which covers the theoretical background including the basic aspects of seL4 and CAmkES, and a practical part that provides a basic case in order to teach participants how to create their very first TRENTOS application. HENSOLDT Cyber's TRENTOS training has received interim endorsement as seL4 training. To access the training, please email info@hensoldt-cyber.com or use the contact form on HENSOLDT Cyber's website. |
Products
|
|
TRENTOS With the Trusted Entity Operating System (TRENTOS), HENSOLDT Cyber provides secure IT from the bottom up, by building upon the mathematically proved seL4 microkernel and its software ecosystem and trusted open-source components. With the TRENTOS SDK, HENSOLDT Cyber provides a complete development environment that equips a developer with all the tools required for building, testing and deploying TRENTOS-based systems to the real world. The SDK contains the actual operating system (OS) source code, consisting of seL4, CAmkES and TRENTOS, but also offers a collection of additional resources designed to make developer’s work easier by increasing efficiency and reducing complexity. For more information about TRENTOS, see HENSOLDT Cyber's blog posts:
To access TRENTOS, please email info@hensoldt-cyber.com. A request can also be submitted through HENSOLDT Cyber's website contact form. |