Advances in agentic AI are making it increasingly easy for attackers to find and exploit vulnerabilities in software. The Fraunhofer Institute for Applied and Integrated Security AISEC is therefore joining the seL4 Foundation and conducting research into the use of the formally verified seL4 microkernel as the foundation for provably secure systems. An initial focus is on virtual machines and confidential computing.

Software, and operating systems in particular, are a central component of nearly all digital systems – from industrial plants and cloud services to medical devices and connected components. At the same time, pressure is mounting to protect these systems from targeted attacks: Thanks to new developments in the field of Agentic AI, attackers are increasingly able to analyze software automatically, identify vulnerabilities more quickly, and prepare and execute attacks in a more targeted and automated manner. This makes systems whose security can not only be tested but also mathematically proven all the more important.

Fraunhofer AISEC has therefore joined the seL4 Foundation. The institute uses the formally verified seL4 microkernel as a foundation and builds upon it to develop robust and trustworthy system architectures. These can be used in particular in critical infrastructure, embedded systems, medical technology, and virtualized IT environments.

Formally Verified Microkernel as a Smaller Attack Surface

The seL4 microkernel is a particularly lightweight operating system kernel. It is limited to basic functions such as memory management, communication between components, and access control. Other functions, such as device drivers, run separately from the kernel in isolated areas of the system.

To clarify: A kernel manages hardware resources (such as the CPU and RAM) and allows applications to access them in a controlled manner. Drivers encapsulate the specific hardware characteristics of a physical device and make them available to the operating system as a standardized, hardware-independent interface (API).

This separation of functions reduces the attack surface and limits potential damage in the event of a successful attack. Due to its small size, seL4 can be formally verified. This means that key security properties of the microkernel are proven using mathematical methods. seL4 thus provides a foundation for systems with high requirements for security, reliability, and traceability. The kernel is verified by the seL4 community. Fraunhofer AISEC builds on this and expands the ecosystem to include features for confidential computing.

Focus on Virtual Machines and Confidential Computing

One of the primary areas of focus for Fraunhofer AISEC is virtual machines (VMs) and confidential computing. VMs make it possible to run multiple operating systems independently of one another on a single physical computer. They are a central component of modern cloud and data center infrastructures.

Confidential computing technologies protect data and applications within a VM from access by the hypervisor – software that manages multiple VMs – or by the operator of the underlying infrastructure. Nevertheless, communication interfaces, device drivers, and extensive operating system components remain potential points of attack. Particularly in the case of large operating system kernels, a vulnerability in a driver or another kernel component can have far-reaching consequences.

Fraunhofer AISEC has extended the seL4 microkernel so that it can run as a guest system in a virtual machine protected by AMD’s SEV-SNP technology. SEV-SNP cryptographically protects the memory of virtual machines and makes it difficult for hypervisors or data center operators to access data processed within them. In the institute’s reference environment – consisting of a Linux host and QEMU/KVM virtualization – smaller seL4-based applications can already be run.

Based on this, Fraunhofer AISEC is gradually developing trustworthy platforms for secure virtualized systems. The goal is to combine the advantages of virtualization and confidential computing with a significantly smaller, formally verified trust base.

Further Development Toward Open Processor Architectures

In addition, the institute is investigating the use of seL4 on the open RISC-V processor architecture, which is becoming increasingly important, particularly in embedded and safety-critical systems. The combination of a formally verified microkernel and an open hardware architecture provides the foundation for trustworthy systems. The goal is to build robust, trustworthy platforms for secure system architectures in the cloud, industry, and connected devices based on the seL4 microkernel.