Ongoing seL4 Research

Key people: Gernot Heiser

Trustworthy Systems (TS) is a research group in the School of Computer Science and Engineering (CSE) at UNSW Sydney. TS works on building highly secure operating systems for the real world. Their approach is based on highly principled designs that support the use of rigorous formal methods to ensure security and reliability without compromising performance.

Currently, TS's main activities are: Time protection, a principled, fundamental approach for the systematic prevention of timing channels and its implementation and verification in seL4; LionsOS, an seL4-based, fast, secure and adaptable operating system for embedded and cyber-physical systems; Pancake, a new low-level programming language designed to enable the implementation and verification of low-level systems code, such as device drivers; the design of a provably-secure seL4-based general-purpose OS.

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.