{"id":183094,"date":"2026-08-25T04:53:36","date_gmt":"2026-08-25T02:53:36","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/vypolnena-formalnaya-verifikacziya-bezopasnosti-mikroyadra-sel4-dlya-arhitektury-aarch64"},"modified":"2026-08-25T04:53:42","modified_gmt":"2026-08-25T02:53:42","slug":"formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","status":"publish","type":"post","link":"https:\/\/prohoster.info\/de\/blog\/news\/formal-security-verification-completed-for-the-sel4-microkernel-on-aarch64","title":{"rendered":"Formale Sicherheitsverifikation des Mikrokernels seL4 f\u00fcr die Architektur AArch64 abgeschlossen","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Die mathematische formale Verifizierung der Zuverl\u00e4ssigkeit 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\u00e4ndige \u00dcbereinstimmung mit den auf der formalen Sprache festgelegten Spezifikationen belegt. Der Beweis der Zuverl\u00e4ssigkeit erm\u00f6glicht den Einsatz von seL4 in sicherheitskritischen Systemen basierend auf ARM64-Prozessoren, die ein erh\u00f6htes Sicherheitsniveau erfordern und garantieren, dass es zu keinen Ausf\u00e4llen kommt. <\/p>\n
Urspr\u00fcnglich wurde der Mikrokern seL4 f\u00fcr 32-Bit-ARM-Prozessoren verifiziert, sp\u00e4ter dann f\u00fcr 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 \u00fcbergreift. Im Kontext der Sicherheitsgew\u00e4hrleistung best\u00e4tigt die Verifizierung, dass der Mikrokern das erforderliche Ma\u00df an Isolation f\u00fcr Anwendungen gew\u00e4hrleistet, ihnen keinen Zugriff auf Informationen ohne Autorisierung erlaubt und sicherstellt, dass im Falle einer Kompromittierung sekund\u00e4rer Anwendungen die Angriffe nicht auf sicherheitskritische Anwendungen \u00fcbergreifen. <\/p>\n
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\u00fcr diese Ressourcen wie f\u00fcr 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\u00fcgung. Hochgradige Abstraktionen und Treiber f\u00fcr die Interaktion mit der Hardware werden separat auf Basis des Mikrokerns in Form von Aufgaben, die im Benutzermodus ausgef\u00fchrt werden, implementiert. Der Zugriff dieser Aufgaben auf die beim Mikrokern vorhandenen Ressourcen wird durch die Festlegung von Regeln organisiert. \n Quelle: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"