Edge Rewrite
everything Source code View original
// HTMLRewriter · presentation

This page was redesigned at the edge.

Cloudflare fetched the original article and streamed it through HTMLRewriter to apply an entirely new visual system without rebuilding the source page.

// request.cf · coarse context

A page that knows where it met you.

Only coarse request metadata is shown. This demo does not display or persist visitor IP addresses.

Country
US
Cloudflare location
CMH
Connection
HTTP/2
Language
Not provided

Ray ID: a42f042d898f386c

Jump to content

Draft:L4Re Operating System Framework

From Wikipedia, the free encyclopedia
  • Comment: I've reverted my rejection as a bad reject, but I will still decline for WP:V reasons. To blythely self quote myself: 我的天了, that was a bad reject. Apologies, Paul-Franitza, 不好意思不好意思. But I still will decline. The only reason I remember from last night that remains valid is that Internet Archive is not a publisher, please see Help:Cite on guidelines on how to cite a source properly. I also noticed today that Dresden Real Time Operating System is a 404 link. Additionally, you have a number of self published sources, including Genode and anything by Kernkonzept themselves. That's all I notice as of now. guninvalid (talk) 03:20, 17 September 2026 (UTC)
  • Comment: Serious signs of AI generation, with AI citations screwing up the sources, failing WP:V. If you are to continue, start over from scratch and please follow WP:BACKWARD. guninvalid (talk) 08:48, 16 September 2026 (UTC)
  • Comment: Thank you for disclosing your affiliation. This draft has a lot of phrases common to AI-generated text and uncommon in human-written text. Please see WP:NOLLM and WP:LLMRESP and rewrite the LLM-generated parts, paying careful attention to WP:NOTPUBLICITY and WP:NPOV. See the partial copyedit I did for a few examples of more neutral language (although not a deep enough copyedit to mitigate LLM issues).
    The article would benefit from more citations to secondary sources unaffiliated with people who develop or work on the L4re, such as books.
    Note that statements such as "Together, these certifications establish L4Re as one of the few operating system frameworks validated for deployment in both classified government and critical infrastructure contexts." would need to be cited. Dreamyshade (talk) 00:33, 30 August 2026 (UTC)


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][3]
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[4]
Official websitel4re.org

The L4Re Operating System Framework (abbreviated as L4Re OSF or L4Re) is an 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 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 is an operating system, hypervisor, or runtime environment designed to enable applications to interact with hardware in a secure and reliable way, based on the microkernel architecture.

The framework is used in systems in the high-assurance, embedded system, automotive,[5] data security, and computer security industries.

History

[edit]

The L4Re Operating System Framework derives from the L4 microkernel family. This line 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 focusing on performance and minimalism.[6]

Development of what would become L4Re began at TU Dresden in 1995. In 1997, the team around Hermann Härtig presented L4Linux at SOSP. They demonstrated 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, restricting Linux to its own address space at the lowest privilege level but preserving its POSIX interface and driver ecosystem.[7]

In 1998, Michael Hohmuth introduced Fiasco, an L4 reimplementation written in C++ rather than the assembly-language approach used by Liedtke. The goal of Fiasco was to improve maintainability and extensibility. Additionally, an interruptible kernel design and lock-free and wait-free algorithms were introduced to achieve real-time behavior.[8][9][10]

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

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

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. It was referred to as the "Merkelphone" because it was supposed to be used by Chancellor Angela Merkel.[15] SiMKo 3 used a Samsung Galaxy S3 with an ARM processor and L4Re as a virtualization layer to run two operating systems simultaneously. This made it possible to replace 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.[16] SiMKo 3 represented the first practical large-scale deployment of L4Re and led to the founding of Kernkonzept GmbH. This company consists of former TU Dresden researchers that maintain and further develop L4Re and Fiasco.OC as the L4Re microkernel.[1]

Architecture

[edit]

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. All higher-level services are executed in user space as isolated components.[17]

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.[8] By this, it coordinates 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, and communication endpoints) is referenced by an unforgeable capability token held in a per-task capability namespace.[18] Access to any resource requires a corresponding capability that 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). Therefore, its codebase and TCB remain small, application-specific, and approachable for auditing and formal verification.[6][19][20]

All services outside 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-based IPC.[17] This means that a fault, crash, or compromise in any individual service is strictly contained. Therefore, it cannot corrupt the kernel, access resources it does not hold a capability for, or destabilize peer components.

This isolation model applies uniformly to all components at the application layer, regardless of their nature. For the L4Re microkernel, there is no difference between a native L4Re application (Micro-App) and a hosted virtual machine (VM) guest operating system such as Linux. They are treated as peers within the same capability framework.[21][22] Both run in user space, both are subject to the same IPC and memory access controls, and neither is more trusted than the other unless it is explicitly granted through additional capabilities. This allows for 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.[5]

Safety and Security

[edit]

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. This property is known as data separation.[23] Traditional monolithic kernels make such guarantees difficult to formally verify due to their large TCBs. 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.[24]

The L4Re Secure Separation Kernel VS and the L4Re Secure Separation Kernel CC are specialized variants of L4Re. They are 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.[25][26] 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.[27] Together, these certifications establish L4Re as an operating system framework validated for deployment in both classified government and critical infrastructure contexts.

Open-Source Licensing

[edit]

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.[4] This license provides users with greater flexibility in using and modifying the software.

References

[edit]
  1. 1 2 3 "Kernkonzept GmbH". Kernkonzept GmbH. Retrieved 2026-02-27.
  2. ↑ "Fiasco Snapshot". 1998-12-07. Retrieved 2026-09-24.
  3. ↑ "Fiasco – TU Dresden Operating Systems Group". Fiasco – TU Dresden. 2007-01-17. Retrieved 2026-09-24.
  4. 1 2 "Fiasco – License". GitHub. Retrieved 2026-02-27.
  5. 1 2 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.
  6. 1 2 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.
  7. ↑ 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.
  8. 1 2 Hohmuth, Michael (December 10, 1998). The Fiasco Kernel: Requirements Definition (Report). Technische Universität Dresden, Fakultät Informatik. ISSN 1430-211X.
  9. ↑ 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.
  10. ↑ 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.
  11. ↑ Reuther, Lars (2003). "L4 Region Mapper Reference Manual". Technische Universität Dresden, Department of Computer Science. Retrieved 2026-03-04.
  12. ↑ 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.
  13. ↑ 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.
  14. ↑ "Base Platforms – Overview of the different kernels supported by Genode". Genode Labs. Retrieved 2026-02-27.
  15. ↑ 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.
  16. ↑ "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.
  17. 1 2 "Introduction – L4Re Operating System Framework". Kernkonzept GmbH. Retrieved 2026-03-17.
  18. ↑ "Capabilities – L4Re Operating System Framework: Interface and Usage Documentation". Kernkonzept GmbH. Retrieved 2026-03-17.
  19. ↑ "Looking further: getting formal verification for L4Re". Kernkonzept GmbH. 2022. Retrieved 2026-03-17.
  20. ↑ "VERSEcloud" (in German). Forschungsprogramm zur IT-Sicherheit und Kommunikationssysteme. Retrieved 2026-03-17.
  21. ↑ Lackorzynski, Adam; Warg, Alexander; Peter, Michael (2010). "Virtual Processors as Kernel Interface" (PDF). Proceedings of the 12th Real-Time Linux Workshop. Nairobi, Kenya.
  22. ↑ Liebergeld, Steffen; Peter, Michael; Lackorzynski, Adam (2010). "Towards Modular Security-conscious Virtual Machines" (PDF). Proceedings of the 12th Real-Time Linux Workshop. Nairobi, Kenya.
  23. ↑ 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.
  24. ↑ 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.
  25. ↑ 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.
  26. ↑ "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.
  27. ↑ 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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Draft:L4Re_Operating_System_Framework&oldid=1376470609"