Draft:L4Re Operating System Framework


L4Re
The logo of L4Re
DeveloperKernkonzept GmbH[1] (formerly TU Dresden)
Written inC++
OS familyL4 microkernel family
Working stateCurrent
Source modelOpen source
Initial releaseOctober 1998; 27 years ago (1998-10) [2]
Marketing targetEmbedded systems, Real-time computing, Cyber security and Cloud computing
Supported platformsCurrent: x86, x86-64, ARM32 and ARM64 for ARM Cortex-R and ARM Cortex-A, MIPS, RISC-V

Prototyping: PowerPC-32, SPARC

Debugging: Lauterbach TRACE32

Former: Intel Itanium IA64
Kernel typeRTOS (microkernel)
LicenseMIT[3]
Official websitel4re.org

The L4Re Operating System Framework (short form L4Re OSF or only L4Re) is a modular and open-source operating system framework designed for embedded systems, real-time applications, and virtualization. It is a descendant of the L4 microkernel family and provides a flexible, user space environment for running applications on top of the L4Re microkernel Fiasco.

The system is maintained by a German company, Kernkonzept GmbH,[1] founded in 2012. L4Re serves as an operating system, hypervisor, or runtime environment, enabling applications to interact with hardware in a proven secure and reliable manner, based on the microkernel architecture.

As of 2026, the framework is used in a variety of systems in the high-assurance, embedded system, automotive,[4] data security, and computer security industries.

History

The L4Re Operating System Framework has its roots in the L4 microkernel family. This lineage of microkernels was originally developed by Jochen Liedtke in the 1990s. Liedtke designed L4 as a second-generation microkernel, improving upon his earlier L3 microkernel by emphasizing performance and minimality as guiding design principles.[5]

Development of what would become L4Re began at TU Dresden in 1995. In 1997, the team around Hermann Härtig presented L4Linux at SOSP, demonstrating that the Linux kernel could run as an unprivileged task inside an L4-based system, communicating with its Linux processes via inter-process communication (IPC). This followed the microkernel philosophy of minimizing kernel bloat and fault domains, confining Linux to its own address space at the lowest privilege level while preserving its POSIX interface and driver ecosystem.[6]

In 1998, Michael Hohmuth introduced Fiasco, an L4 reimplementation written in C++ rather than the assembly-language approach used by Liedtke. Fiasco aimed for better maintainability and extensibility while introducing an interruptible kernel design and lock-free and wait-free algorithms to achieve real-time capability.[7][8][9]

Between 2000 and 2003, Lars Reuther and colleagues extended the L4 userland with dataspaces and a region manager, laying the groundwork for the higher-level resource management infrastructure called L4Env.[10]

Alexander Warg and Adam Lackorzynski undertook a groundbreaking redesign of Fiasco from 2005 to 2009, driven by the latest advances in cybersecurity research and placing security at the very core of its architecture, which culminated in the 2009 release of Fiasco.OC (Fiasco with Object Capabilities). This pioneering work introduced a capability-based mandatory access control model,[11] elevating Fiasco to a third-generation microkernel with IPC gates as communication channels and a mapping database for bookkeeping and revocation of capabilities. This approach enables fine-grained, verifiable access control across isolated components.[12] Additionally in 2009, Fiasco gained symmetric multiprocessing (SMP) support.[13]

In 2012, L4Re was deployed in the SiMKo 3, a cryptographically secured smartphone developed by Deutsche Telekom for the German Federal Ministry of the Interior as a classified communications device, colloquially referred to as the "Merkelphone" due to plans for its use by Chancellor Angela Merkel.[14] Built on a Samsung Galaxy S3 with an ARM processor, SiMKo 3 used L4Re as a virtualization layer to run two operating systems simultaneously, replacing the commercially available software of its predecessors, which had run on Windows Mobile. In 2013, SiMKo 3 received German Federal Office for Information Security (BSI) approval for processing VS-NfD (for internal use only) classified information.[15] SiMKo 3 represented the first practical large-scale deployment of L4Re and led to the founding of Kernkonzept GmbH, a company established by former TU Dresden researchers to maintain and further develop L4Re and Fiasco.OC as the L4Re microkernel.[1]

Architecture

L4Re is a microkernel-based operating system framework. Its architecture follows the principle of least privilege and strict separation of concerns. Only the most fundamental system functions are handled by the kernel itself, while all higher-level services execute in user space as isolated components.[16]

The L4Re microkernel Fiasco forms the lowest layer of the architecture and is the only component running in privileged mode. The kernel is reduced to a small set of essential services, namely thread scheduling, communication, and basic memory management.[7] By this, it is capable of coordinating the execution of threads across available CPU cores, providing synchronous and asynchronous communication channels between isolated components, and managing physical memory at the page level.

Beyond these primitives, the microkernel exposes a capability-based security model in which every resource (such as memory regions, threads, communication endpoints) is referenced by an unforgeable capability token held in a per-task capability namespace.[17] Access to any resource requires possession of a corresponding capability, which can be selectively delegated between components. This enforces the principle of least privilege at the kernel interface level.

Because the microkernel deliberately excludes device drivers, file systems, network stacks, and similar services from its trusted computing base (TCB), both its codebase and TCB remain small, application specific and approachable to auditing and formal verification.[5][18][19]

All services beyond the microkernel's minimal set run as isolated server processes in user space. Each service occupies its own protection domain and can only interact with other components through capability-mediated IPC.[16] This means that a fault, crash, or compromise in any individual service is strictly contained. Therefore, it cannot corrupt the kernel, access resources it holds no capability for, or destabilize peer components.

This isolation model applies uniformly to all components at the application layer, regardless of their nature. Native L4 applications (Micro-Apps) and full virtual machines (VM) hosting guest operating systems such as Linux are treated as peers within the same capability framework.[20][21] Both run in user space, both are subject to the same IPC and memory access controls, and neither is inherently more trusted than the other unless explicitly granted additional capabilities. This allows safety-critical Micro-Apps and general-purpose VM workloads to coexist on the same hardware with provable separation. This separation allows for mixed criticality systems in domains such as automotive and industrial control.[4]

Safety and Security

High-security environments such as defense, aerospace, and critical infrastructure require operating systems to enforce strict isolation between processes handling data at different classification levels. A system processing both classified and unclassified data simultaneously must provide verifiable guarantees that information cannot leak across these boundaries, which is a property known as data separation.[22] Traditional monolithic kernels make such guarantees difficult to formally verify due to their large TCB. A microkernel-based separation kernel, in comparison, reduces the TCB to a small, formally auditable core, making it a preferred architecture for high-assurance certification.[23]

The L4Re Secure Separation Kernel VS and the L4Re Secure Separation Kernel CC are specialized variants of L4Re certified and accredited for high-assurance security environments. In 2024, the L4Re Secure Separation Kernel VS was accredited by the German Federal Office for Information Security for the processing of information classified up to GEHEIM (German SECRET) and NATO SECRET.[24][25] In 2025, the L4Re Secure Separation Kernel CC 1.0.1 received Common Criteria (CC) certification at Evaluation Assurance Level EAL4+, confirming that its security properties have been not only claimed but independently verified through formal analysis and rigorous testing of the design.[26] Together, these certifications establish L4Re as one of the few operating system frameworks validated for deployment in both classified government and critical infrastructure contexts.

Open-Source Licensing

L4Re is a fully open-source software that was originally released under the GNU General Public License version 2 (GPLv2). In September 2025 there was a switch to the MIT License.[3] This license provides users with greater flexibility in using and modifying the software.

References

  1. ^ a b c "Kernkonzept GmbH". Kernkonzept GmbH. Retrieved 2026-02-27.
  2. ^ "Fiasco – TU Dresden Operating Systems Group". Internet Archive. 1999-05-08. Retrieved 2026-02-27.
  3. ^ a b "Fiasco – License". GitHub. Retrieved 2026-02-27.
  4. ^ a b Serdyuk, Yuriy; Kondikov, Alexey (2022). Back-connect to the connected car: Search for vulnerabilities in the VW electric car (PDF). Black Hat Europe 2022. NavInfo Europe Cybersecurity Team. Retrieved 2026-02-27.
  5. ^ a b Liedtke, Jochen (1995-12-03). On µ-Kernel Construction. Proceedings of the 15th ACM Symposium on Operating Systems Principles (SOSP '95). Copper Mountain Resort, Colorado: Association for Computing Machinery. pp. 237–250. doi:10.1145/224056.224075.
  6. ^ Härtig, Hermann; Hohmuth, Michael; Liedtke, Jochen; Schönberg, Sebastian; Wolter, Jean (1997-10-05). The Performance of µ-Kernel-Based Systems (PDF). Proceedings of the 16th ACM Symposium on Operating Systems Principles (SOSP '97). Saint-Malo, France: Association for Computing Machinery. Retrieved 2026-03-04.
  7. ^ a b Hohmuth, Michael (December 10, 1998). The Fiasco Kernel: Requirements Definition (Report). Technische Universität Dresden, Fakultät Informatik. ISSN 1430-211X.
  8. ^ Baumgartl, R.; Borriss, M.; Härtig, H.; Hamann, Cl.-J.; Hohmuth, M.; Reuther, L.; Schönberg, S.; Wolter, J. (1998). Dresden Realtime Operating System. Proceedings of SDA '98. Dresden, Germany: Department of Computer Science, Dresden University of Technology.
  9. ^ Hohmuth, Michael; Härtig, Hermann (2001). Pragmatic Nonblocking Synchronization for Real-Time Systems (PDF). Proceedings of the 2001 USENIX Annual Technical Conference (USENIX '01). USENIX Association. Retrieved 2026-03-04.
  10. ^ Reuther, Lars (2003). "L4 Region Mapper Reference Manual". Technische Universität Dresden, Department of Computer Science. Retrieved 2026-03-04.
  11. ^ Lackorzynski, Adam; Warg, Alexander (2009). "Taming Subsystems: Capabilities as Universal Resource Access Control in L4" (PDF). Proceedings of the Second Workshop on Isolation and Integration in Embedded Systems (IIES '09). Nuremberg, Germany: ACM. pp. 25–30. ISBN 978-1-60558-464-5.
  12. ^ Peter, Michael; Schild, Henning; Lackorzynski, Adam; Warg, Alexander (March 2009). "Virtual Machines Jailed: Virtualization in Systems with Small Trusted Computing Bases". Proceedings of the 1st EuroSys Workshop on Virtualization Technology for Dependable Systems (VTDS '09). ACM. pp. 18–23. doi:10.1145/1518684.1518688. ISBN 978-1-60558-473-7.
  13. ^ "Base Platforms – Overview of the different kernels supported by Genode". Genode Labs. Retrieved 2026-02-27.
  14. ^ Sicheres mobiles Arbeiten [Secure Mobile Working] (PDF) (Report) (in German). Bundesamt für Sicherheit in der Informationstechnik (BSI). 2016-10-01. Retrieved 2026-03-04.
  15. ^ "Hochsicherheitshandy der Telekom erhält BSI-Zulassung" [Telekom's High-Security Mobile Phone Receives BSI Approval] (PDF) (Press release) (in German). Deutsche Telekom AG. 2013-09-09. Retrieved 2026-03-04.
  16. ^ a b "Introduction – L4Re Operating System Framework". Kernkonzept GmbH. Retrieved 2026-03-17.
  17. ^ "Capabilities – L4Re Operating System Framework: Interface and Usage Documentation". Kernkonzept GmbH. Retrieved 2026-03-17.
  18. ^ "Looking further: getting formal verification for L4Re". Kernkonzept GmbH. 2022. Retrieved 2026-03-17.
  19. ^ "VERSEcloud" (in German). Forschungsprogramm zur IT-Sicherheit und Kommunikationssysteme. Retrieved 2026-03-17.
  20. ^ Lackorzynski, Adam; Warg, Alexander; Peter, Michael (2010). "Virtual Processors as Kernel Interface" (PDF). Proceedings of the 12th Real-Time Linux Workshop. Nairobi, Kenya.
  21. ^ Liebergeld, Steffen; Peter, Michael; Lackorzynski, Adam (2010). "Towards Modular Security-conscious Virtual Machines" (PDF). Proceedings of the 12th Real-Time Linux Workshop. Nairobi, Kenya.
  22. ^ Heitmeyer, Constance L.; Archer, Myla; Leonard, Elizabeth I.; McLean, John (2006). Formal specification and verification of data separation in a separation kernel for an embedded system. Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS '06). Alexandria, Virginia, USA: Association for Computing Machinery. pp. 346–355. doi:10.1145/1180405.1180448. ISBN 1595935185.
  23. ^ Rushby, J. M. (1981). Design and verification of secure systems. Proceedings of the Eighth ACM Symposium on Operating Systems Principles (SOSP '81). Pacific Grove, California, USA: Association for Computing Machinery. pp. 12–21. doi:10.1145/800216.806586. ISBN 0897910621.
  24. ^ Vergleichstabelle der Geheimhaltungsgrade [Comparison Table of Classification Levels] (PDF) (Report) (in German). Bundesministerium des Innern und für Heimat (Federal Ministry of the Interior and Community). Retrieved 2026-03-04.
  25. ^ "L4Re Secure Separation Kernel VS – BSI-Schrift 7164: Liste der zugelassenen IT-Sicherheitsprodukte und -systeme" (in German). Bundesamt für Sicherheit in der Informationstechnik (BSI). Retrieved 2026-03-04.
  26. ^ Certification Report BSI-DSZ-CC-1177-2025 for L4Re Secure Separation Kernel CC Version 1.0.1 (Report). V1.0. Bundesamt für Sicherheit in der Informationstechnik (BSI). 2025-02-18. BSI-DSZ-CC-1177-2025. Retrieved 2026-03-04.

Content Disclaimer

Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.

  1. The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
  2. There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
  3. It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
  4. Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
  5. Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.