SeL4 mikrokernele on tehtud formaalne turvalisuse valideerimine AArch64 arhitektuuri jaoks
Mõisted ja matemaatiline formaalne valideerimine seL4 mikrokernele töökindluse ja turvalisuse üle AArch64 arhitektuuril on lõpetatud. Valideerimine põhineb matemaatilisel tõestusel seL4 korrektse toimimise kohta, mis tõestab selle täielikku vastavust määratud formaalsele spetsifikatsioonile. Usaldusväärsuse tõestamine võimaldab kasutada seL4 kritiliselt olulistes süsteemides ARM64 protsessoritel, millel on vajaliku turvalisuse ja […]
