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.
seL4 Foundation
A core part of our engagement with the wider community is our membership in, and leadership of, the seL4 Foundation. We are a founding member of the Foundation, a key contributor to seL4, and TS Leader Gernot Heiser is its founding chairman.
seL4 itself was created by TS, when it was part of NICTA, and many of its creators are still with TS or its spin-off Proofcraft. We continue to develop components of the seL4 ecosystem, and, where appropriate, hand them over to the Foundation, the seL4 Microkit is an example.
Community Projects
We actively engage with the wider seL4 community and encourage it to participate in the development and deployment of seL4-based artefacts. In particular, we have created newcomer-friendly community projects around LionsOS.
We are also developing a new programming language Pancake, which is a verification-friendly language suitable for low-level systems programming (a draft syntax reference here). We plan to create a similar community project for verifying LionsOS components implemented in Pancake – stay tuned!
Services
We provide research, consulting and development services around deployment and verification of seL4 and seL4-based systems, where 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 worked with industry partners and utilities to protect vulnerable critical infrastructure from cyber attacks. The project developed the seL4-based Laot device, which sits between the vulnerable control system and the Internet. This project led to the development of the seL4 Microkit.