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.