After completing the proofs offunctional correctnessandintegrity,
Proofcraft has now established the proof that seL4 enforcesconfidentialityon
AArch64, providing a formal mathematical proof that the kernel prevents an
application running on top of seL4 from learning information without
authorisation.
Thanks to continued support fromNCSC, this milestone completes the formal
proof that the seL4 implementation code on AArch64 enforces security isolation
of the applications running on top (under the assumptions listedhere). This
isolation prevents attacks on non-critical applications from propagating to
critical applications and compromising them.
The paperThe Algebra of Iterative Constructionsby Kevin Batz,
Benjamin Lucien Kaminski, Lucas Kehrer, Gerwin Klein, Henning Urbat, and Todd
Schmid was presented at the 41st Annual Symposium on Logic in Computer Science
(LICS) in Lisbon this week. This paper in theoretical computer science is
about an algebraic abstraction and reasoning principles for the iterative
construction of fixed points. Fixed points are a recurring theme in computer
science with many famous results such as the Kleene fixed point theorem. The
algebra shown in this paper allows expressing such theorems concisely and
enables reasoning about them in an abstract and streamlined way that can be
implemented efficiently in proof assistants such as Isabelle/HOL, which
Proofcraft is using for the verification of the seL4 microkernel.
The highly automated Isabelle/HOL implementation of iteration algebra in this
paper resulted from a spontaneous collaboration between Proofcraft’s Chief
Scientist Gerwin Klein and Benjamin Kaminski that started at the IFIP Working
Group 2.3 (Programming Methodology) meeting in Athens in 2025. It shows that
proof engineering ranges from practical application all the way to deep theory.
Proofcraft achieved a significant milestone in theseL4verification roadmap
that was years in the making: the MCS configuration of seL4, providing support
for mixed-criticality systems, is now proved to be correct on RISC-V.
This configuration is the largest new seL4 feature, indispensable for mixed
criticality real-time applications such as automotive use cases. It contains
wide-ranging changes to the kernel’s implementation and API. Its verification
therefore required considerable effort and has been a priority in the seL4
roadmap for a long time.
Proofcraft has now completed, for the very first time, the verification of
functional correctness for seL4 with MCS. Functional correctness is the largest and most central
proof in theseL4 verification stack. The proof targets the RISC-V architecture
and will now be ported to the Arm 64-bit architecture, as part ofDARPA’s PROVERS program.
Proofcraft delivered the implementation and formal proof of more flexible
domain scheduling inseL4.
Before the change, the seL4 security proofs, and in particular the proof of
information flow enforcement, required a fully static schedule that was
compiled into the kernel. This meant that, when using seL4 to enforce the
information flow boundaries between applications, developers were required
to provide a fixed predetermined amount of time for each domain, for the
entire lifetime of the running system. This strict policy made it hard to apply
information flow control in practice and to support in SDK-style development such
as theMicrokit.
Proofcraft proposed a new seL4 runtime API (Application Programming Interface)
allowing the loading of semi-static domain schedules. This means that a system
with information flow protection can go through different phases at runtime that
can satisfy different domain timing requirements. For instance, a boot phase of
the system can have longer time slices to allow virtual machines to start
without overrunning their domain time allocation, and an operational phase of
the system can provide shorter time slices so that each domain can be responsive
to outside interaction. Additionally, an SDK-based system such as the Microkit
can use the new API to set a domain schedule at boot time.
This new seL4 API is implemented, verified and available in seL4 15.0.0.
On May 21st 2026,CDIS– Swedish research Center for Cyber Defense and
Information Security – held itsspring conferenceat KTH Royal Institute of
Technology in Stockholm.