Die mathematische formale Verifizierung der Zuverlässigkeit und Sicherheit des Mikrokerns seL4 auf Systemen mit der Architektur des Befehlssatzes AArch64 wurde abgeschlossen. Die Verifizierung reduziert sich auf den mathematischen Beweis der Korrektheit der Funktion von seL4, der die vollständige Übereinstimmung mit den auf der formalen Sprache festgelegten Spezifikationen belegt. Der Beweis der Zuverlässigkeit ermöglicht den Einsatz von seL4 in sicherheitskritischen Systemen basierend auf ARM64-Prozessoren, die ein erhöhtes Sicherheitsniveau erfordern und garantieren, dass es zu keinen Ausfällen kommt.
Ursprünglich wurde der Mikrokern seL4 für 32-Bit-ARM-Prozessoren verifiziert, später dann für 64-Bit-Architekturen wie x86 und RISC-V. Die Verifizierung stellt sicher, dass im Falle eines Ausfalls in einem Teil des Systems dieser Ausfall nicht auf den Rest des Systems und seine kritischen Teile übergreift. Im Kontext der Sicherheitsgewährleistung bestätigt die Verifizierung, dass der Mikrokern das erforderliche Maß an Isolation für Anwendungen gewährleistet, ihnen keinen Zugriff auf Informationen ohne Autorisierung erlaubt und sicherstellt, dass im Falle einer Kompromittierung sekundärer Anwendungen die Angriffe nicht auf sicherheitskritische Anwendungen übergreifen.
Die Architektur des Mikrokerns seL4 zeichnet sich durch die Auslagerung von Teilen zur Ressourcenverwaltung des Kerns in den Benutzermodus aus und der Anwendung derselben Zugriffssteuerungsmechanismen für diese Ressourcen wie für Benutzerressourcen. Der Mikrokern bietet keine fertigen hochgradigen Abstraktionen zur Verwaltung von Dateien, Prozessen, Netzwerkverbindungen usw., sondern stellt lediglich minimale Mechanismen zur Verwaltung des Zugriffs auf den physischen Adressraum, Unterbrechungen und Prozessorressourcen zur Verfügung. Hochgradige Abstraktionen und Treiber für die Interaktion mit der Hardware werden separat auf Basis des Mikrokerns in Form von Aufgaben, die im Benutzermodus ausgeführt werden, implementiert. Der Zugriff dieser Aufgaben auf die beim Mikrokern vorhandenen Ressourcen wird durch die Festlegung von Regeln organisiert.
Quelle: opennet.ru
