seL4 Summit 2025 Abstracts

Collaborators:

• Kansas State University/Aarhus University – Robby, Jason Belt, Stefan Hallerstede
• Collins Aerospace – Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin
• Dornerworks – Robert VanVossen, Nathan Studer
• UNSW – Gernot Heiser, Robert Sison
• ProofCraft – Gerwin Klein, Rafal Kolanski, June Andronick

The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain for seL4 with integrated formal methods. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework, whose development is led by researchers at Kansas State University, is a key part of the INSPECTA tool chain. Developed on the DARPA CASE project within Collins Aerospace team and on other US Department of Defense projects led by Galois, HAMR originally supported system modeling using the SAE standard AADL modeling language. On these projects, HAMR generated infrastructure code and application code thread skeletons in C and in Slang (a safety-critical subset of Scala developed at Kansas State University). HAMR supported system deployments on the Java Virtual Machine (JVM), Linux, and the seL4 micro-kernel using CAmkES. HAMR supported the GUMBO AADL contract language (jointly developed by KSU and Galois) that enabled engineers to formally specify interface behaviors of AADL thread components using familiar contract-based idioms. These model-level contracts were translated as part of HAMR’s code generation to code-level contracts (allowing SMT-based tools to verify that user application code conforms to contracts) and executable contracts (enabling testing frameworks to use these as test oracles and run-time monitoring to use them as run-time checks on thread input/output behavior). In this talk, we describe a number of new capabilities of HAMR developed on the INSPECTA project. First, the modeling layer of HAMR has been extended to support SysMLv2 – a new version of the widely-used

SysML modeling language standardized by the Object Modeling Group (OMG). We describe how HAMR- supported AADL-based specifications and tooling, including the GUMBO contract language, are being integrated within SysMLv2 modeling environments, including the SysIDE extension for VSCode. Second, we have extended HAMR’s code generation to support the Rust programming language and seL4 microkit. This provides both C and Rust-based development on seL4 with both CAmkES and microkit. For example, Rust implementations of SysMLv2/AADL threads can be deployed in seL4 microkit protection domains, with auto-generated microkit system description files and developer-facing microkit APIs for threading and channel communication. Finally, we have added contract generation support in Rust code for both formal contracts for the Verus verification tool and Rust executable contracts. The talk will provide short demos of all of these features – including showing Verus verification of seL4-deployed Rust thread component application code conformance to HAMR-generated contracts and automated property-based testing of Rust thread component code against HAMR-generated executable contracts. These new capabilities of HAMR are being applied by Dornerworks and Collins Aerospace engineers on military applications including mission control software for UAVs. HAMR is available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).

The Cyberagentur has launched its research program “Ecosystem formally verifiable IT – provable Cybersecurity (EvIT)” to take cybersecurity to the next level. It encompasses what the creators of seL4 set out to achieve but goes even further: in addition to kernel and operating system, the goal is to verify the entire IT stack. Five research projects are funded with partners from Australia, Germany, the Netherlands, and New Zealand. They take complementary approaches over the next four years or so, including: extending the seL4 microkernel to allow multikernel operation, to harden it against side-channel attacks, to allow verification of device drivers, and to support the creation of seL4-based operating systems; verifying a unikernel operating system written in Rust and the RISC V-based microprocessor it runs on in a single, holistic verification approach; a compositional approach to verifying hardware, ISA, and operating system; and extending a functional hardware description language for ASICs and FPGAs to allow formal verification of both hardware and software designs. In addition, a community building program aims to make the benefits of formal verification known more widely, both to attract future talent to the field and to broaden its adoption.

The vision driving the program is introducing a new cybersecurity paradigm: security by design, not as an afterthought. More research will be necessary both taking the topics covered in EvIT even further, and covering more aspects outside of EvIT. One intriguing speculation I like to indulge in is to employ formal verification as an alternative to certification. I would like to kickstart a debate on whether that is feasible and likely to succeed.