seL4-Sicherheitsbeweise auf AArch64 abgeschlossen
SeL4 security proofs now complete on AArch64
Proofcraft hat den formalen Beweis erbracht, dass der seL4-Microkernel auf AArch64 die Vertraulichkeit von Anwendungen gewährleistet. Damit ist die vollständige Sicherheitsisolation auf der 64-Bit-Arm-Architektur mathematisch abgesichert. Der Beweis verhindert, dass Angriffe auf nicht-kritische Anwendungen auf kritische Systeme übergreifen. Möglich wurde dies durch die fortgesetzte Unterstützung des britischen NCSC. Dieser Meilenstein vervollständigt die formale Verifikation der Sicherheitseigenschaften von seL4 auf AArch64.
Dieser Meilenstein vervollständigt den formalen Beweis, dass der seL4-Implementierungscode auf AArch64 die Sicherheitsisolation der darauf laufenden Anwendungen durchsetzt.
- StilesCrisis
Bald erhältlich: ein Seitenkanal-Timing-Angriff, der dieses Ergebnis komplett zunichtemacht.
- i_am_a_peasant
Lies das Kleingedruckte: "non-MCS (Mixed-Criticality-Systeme), Unicore".
- kvuj
Welche Betriebssysteme verwenden seL4? Ich kenne die folgenden:
- GenodeOS
- LionsOS
- Ein chinesischer Autohersteller nutzte es meines Wissens als Hypervisor in seinen Autos.
- Was noch? Gibt es private Bereitstellungen, von denen ihr wisst?
- avadodin
Der Embedded- und Militärmarkt mag sie auf absehbare Zeit weiter finanzieren, aber sie brauchen ein natives seL4/Linux, wenn sie ehrlich behaupten wollen, mit ihrem Capability-Modell die Sicherheit von Systemen zu verbessern.
Secure-Boot-Virtualisierungsplattformen gibt es heutzutage wie Sand am Meer.