Przeprowadzono formalną weryfikację bezpieczeństwa mikrojądra seL4 dla architektury AArch64.
Zakończono prace nad matematyczną formalną weryfikacją niezawodności i bezpieczeństwa działania mikrojądra seL4 na systemach z architekturą zestawu instrukcji AArch64. Weryfikacja sprowadza się do matematycznego dowodu poprawności działania seL4, co świadczy o pełnej zgodności z wymaganiami określonymi w formalnych specyfikacjach językowych. Dowód niezawodności pozwala na zastosowanie seL4 w systemach krytycznych opartych na procesorach ARM64, które wymagają podwyższonego poziomu bezpieczeństwa i […]
