Real-world engagement
We have a strong track record of collaboration with government and industry partners for deploying our technology outside the lab. We apply our formal methods and >software stack to solve real-world problems, with verified guarantees that are unprecedented in the industry. Many of these collaborations now happen through the seL4 Foundation and its growing number of providers of services for the deployment of seL4.
We provide research, consulting and development services around deployment and verification of seL4 and seL4-based systems.
Get in touch if you have a real-world security or safety problem that could benefit from seL4.
Examples of seL4 and Trustworthy Systems solving real-world problems
Cyberattack-proof autonomous vehicles
We have an ongoing partnership with the US Defense Advanced Research Projects Agency (DARPA). In the SMACCM team of the DARPA HACMS project we demonstrated that formally verified software effectively prevents cyberattacks on embedded computers in autonomous drones, helicopters, land robots and trucks.
Cyber Assured Systems Engineering
Our current DARPA collaboration is Cyber Assured Systems Engineering (CASE). We are developing reusable design, analysis and verification tools that allow software engineers to design-in cyber resiliency when building embedded computing systems from scratch.
Secure display of classified information
We partnered with the Australian Defence Science and Technology Group (DST) on the development of the Cross Domain Desktop Compositor (CDDC) (CDDC).
The CDDC is a device that leverages seL4's isolation and information security capabilities to enable the concurrent display of information from networks of different classifications, while guaranteeing no cross-domain leakage.
Next-generation hardware-software stack
We have partnered with the German company HENSOLDT Cyber to build a secure computing stack on top of seL4.
Building on the open RISC-V hardware architecture, HENSOLDT Cyber developed the MiG-V processor, which uses innovative logic encryption to defeat supply-chain attacks. For MiG-V HENSOLDT Cyber developed the TRENTOS operating system with seL4 at its core.
Protecting critical infrastructure
We are working with industry partners and utilities to protect vulnerable critical infrastructure from cyber attacks. The project develops the seL4-based Laot device, which sits between the vulnerable control system and the Internet. We are aiming to deploy this in a public utility by the end of 2021.
Communication security for humanitarian organisations
This collaboration aims at developing a secure Operating System by building a Qubes-like OS on seL4 instead of Xen.