Ongoing seL4 Research

Key people: Gernot Heiser

The Trustworthy Systems (TS) group aims to make truly secure and safe operating systems a reality. As a direct successor of the team that originally created and verified seL4, it is focussed on principled and verifiable seL4-based OS designs that achieve unprecedented security for real-world systems without compromising performance.

TS’s approach is to re-think and re-develop system architecture from scratch, using fine-grained modularity, strict separation of concerns and radical simplicity. TS also contributes to on-going development of seL4, evaluating and improving kernel performance, and adding missing features required by real-world systems.

TS’s current main activities are time protection – hardware and kernel mechanisms for principled prevention of microarchitectural timing channels, LionsOS, a statically architected, provably-secure, deployable OS for embedded/cyberphysical systems, Pancake, a verification-friendly systems programming language with a verified compiler that is used for implementing and verifying LionsOS, and Djawula, a proof-of-concept of a general-purpose OS that can be proved to enforce a fairly arbitrary security policy. TS open-sources all project code and proofs.

Key people: John Hatcliff; Robby

SAnToS Lab conducts both theoretical and applied research on Specification, Analysis, and Transformation of Software. Integration of practical and scalable formal methods and testing in user-friendly development tools is a special emphasis of the lab. Current research projects related to seL4 include the HAMR framework (High-Assurance Model-based Rapid Engineering of Embedded Systems). HAMR is an open-source code generation and system build framework for embedded systems whose architecture is specified using the SAE standard Architecture, Analysis, and Design Language (AADL) or OMG standard SysMLv2 modeling language. HAMR includes multiple integrated formal methods and contract based reasoning in both models and code. It can be used to create applications that run on top of seL4 (using seL4 Microkit or CAmkES) and other platforms, where components within the application are optionally assured using contract-based verification or automated property-based testing. HAMR was used on the DARPA CASE program by Collins Aerospace to build seL4/C-based applications for UAV mission computing. Currently, HAMR is being enhanced on the Collins Aerospace DARPA PROVERS INSPECTA project to support Rust-based development of verified applications using seL4 Microkit.

Key people: Perry Alexander

KU's seL4-related reseach include trustworthy layered attestation, enabling trust in a remote party while leveraging seL4 to provide a verified level of software-based process isolation. The team was part of the DARPA-funded CASE program, contributing StairCASE, an effort to develop semantics and tools for integrating remote attestation with static analysis and develop formally verified and synthesised remote attestation infrastructure. The team is now part of the currently running DARPA PROVERS program where they will also be contributing AI-enhanced proof repair technology.

Key people: Timothy Roscoe (Mothy); Roman Meier; Zikai Liu; Daniel Schwyn; David Cock

The Systems Group is one of the groups at ETH Zürich whose work includes seL4-related research. The group focuses on Operating System Design and Implementation and contributes seL4-based trustworthy BMCs (board management controllers) using cyber retrofit for server board controllers. It also works on the co-generation of drivers and hardware for seL4, as part of the Sockeye project.

Key people: Nils Wistoff

The work of the Digital Circuits and Systems Group at ETH also includes seL4-related research. As part of its PULP (Parallel Ultra Low Power) flagship project, the Digital Circuits and Systems Group contributes expertise in hardware to timing channels discovery and mitigation to the seL4 time protection project. Work is being done in collaboration with TS at UNSW.

Key people: Alain Kägi

Alain Kagi and his group at Lewis & Clark College are working on a verifiable minimal networking stack for seL4, leveraging the seL4 Microkit and the seL4 Device Driver Framework.