Formale Sicherheitsverifikation des Mikrokernels seL4 für die Architektur AArch64 abgeschlossen
Die Arbeiten an der mathematischen formalen Verifikation der Zuverlässigkeit und Sicherheit des Mikrokernels seL4 auf Systemen mit der Architektur AArch64 wurden abgeschlossen. Die Verifikation reduziert sich auf den mathematischen Nachweis der Korrektheit des Betriebs von seL4, was die vollständige Übereinstimmung mit den im formalen Spezifikationssprache festgelegten Anforderungen belegt. Der Nachweis der Zuverlässigkeit ermöglicht die Verwendung von seL4 in kritischen Systemen basierend auf ARM64-Prozessoren, die ein erhöhtes Sicherheitsniveau erfordern und […]
