BSI-DSZ-CC-1177-2025
L4Re Secure Separation Kernel CC, Version 1.0.1
| Antragsteller / Applicant | Kernkonzept GmbH Buchenstraße 16 b |
| Prüfstelle / Evaluation Facility |
atsec information security GmbH |
| Prüftiefe / Assurance |
EAL4+, ALC_FLR.3 |
| Ausstellungsdatum / Certification Date |
18.02.2025 |
| gültig bis / valid until |
17.02.2030 |
Zertifizierungsreport / Certification Report
Sicherheitsvorgaben / Security Target
Zertifikat / Certificate
Der EVG ist der L4Re Secure Separation Kernel CC 1.0.1 (L4Re SSK). L4Re SSK ist eine Open Source Distribution der L4Re Betriebssystemumgebung. Demzufolge basiert dieses Betriebssystem auf dem L4Re Microkernel der dritten Generation mit einem modernen Capability-basierten Zugriffskontrollmodell. Mit diesem Modell kann eine Separierung von Anwendungen in unterschiedliche Sicherheitszonen erzwungen werden, deren Informationsfluss jederzeit kontrolliert und begrenzt bleibt, und denen verschiedene Ressourcen und Kommunikationskanäle zugewiesen werden. Darüber hinaus unterstützt der L4Re Microkernel parallel sowohl statische als auch dynamische Anwendungen, welche zur Laufzeit gestartet oder angehalten werden können.
Der L4Re SSK wird in der evaluierten Konfiguration als ein Separationskern eingesetzt, welcher die Sicherheitsleistungen erbringt, die im ST spezifiziert sind. Der EVG unterstützt sowohl native Anwendungen, als auch virtuelle Maschinen (VM). Der Zugriff auf Systemressourcen wie Speicher, Geräte und CPU Kerne wird mittels Capabilities geschützt. Anwendungen und VMs können ausschließlich auf Ressourcen zugreifen, wenn sie die dazugehörige Capability mit den entsprechenden Rechten halten.
The TOE is the L4Re Secure Separation Kernel CC 1.0.1 (L4Re SSK). L4Re SSK is a distribution of the
open-source L4Re Operating System Framework. As such it is based on the L4Re Microkernel. The
L4Re Microkernel is a 3rd-generation microkernel with a state-of-the-art capability-based mandatory access control security model. It allows the separation of applications into different security domains, information flow control, and, subject to access control, dynamic assignment of resources and communication channels. Further the L4Re Microkernel supports static workloads alongside dynamic workloads, which allows to start, restart and shutdown applications during runtime.
L4Re SSK is configured to act as a separation kernel, to provide the security features claimed by the ST. The TOE supports native applications as well as virtual machines (VMs). Access to every resource including but not limited to memory, hardware devices and CPU cores is protected by capabilities. Applications and VMs can only access a resource if they possess a capability with suitable permissions for that resource.