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 seL4-based 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, although only if no suitable commercial provider is available. 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
Another DARPA-sponsored collaboration was Cyber Assured Systems Engineering (CASE). We developed reusable design, analysis and verification tools that allow software engineers to design-in cyber resiliency when building embedded computing systems from scratch.
Industrial Scale Proof Engineering for Critical Trustworthy Applications
Our latest DARPA project is Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA). We develop the highly modular, fast, secure and adaptable LionsOS, work a repeatable engineering process for verifying its components, and support our partners in deploying it on their real-world platforms.
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.
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.