On lõpetatud matemaatilise formaalse verifitseerimise töö mikrokiibi seL4 usaldusväärsuse ja turvalisuse kohta AArch64 arhitektuuriga süsteemides. Verifitseerimine seisneb seL4 töö korrektsete matemaatiliste tõendite koostamises, mis tõendavad täielikku vastavust formaalses keeles esitatud spetsifikatsioonidele. Usaldusväärsuse tõendamine võimaldab kasutada seL4 kriitiliselt olulistes ARM64 arhitektuuriga süsteemides, mis nõuavad kõrgemat turvalisuse taset ja garantii, et rikkepunkte ei esine.
Alguses oli mikrokiip seL4 kinnitatud 32-bitiste ARM-protsessorite jaoks, hiljem aga 64-bitiste x86 ja RISC-V protsessorite jaoks. Verifitseerimine tagab, et kui ühes süsteemi osas juhtub tõrge, siis see ei levita ülejäänud süsteemile ja selle kriitilistele osadele. Turvalisuse tagamise kontekstis kinnitab verifitseerimine, et kiip tagab rakenduste sobiva isolatsiooni taseme, ei luba neil saada volitusteta ligipääsu teabele ning garanteerib, et kui sekundaarsed rakendused on ohustatud, ei levi rünnak kriitilistele rakendustele.
Mikrokiibi seL4 arhitektuur on tähelepanuväärne, kuna osade kernelite ressursside haldamine on viidud kasutajaruumi, rakendades neid samu juurdepääsukontrolli meetodeid, mis on ette nähtud kasutajaressursside haldamiseks. Mikrokiip ei paku valmis kõrgema taseme abstraktsioone failide, protsesside, võrguühenduste jms haldamiseks, vaid pakub ainult minimaalset mehhanismi füüsiliste aadressiruumide, katkestuste ja protsessori ressursside juurdepääsu haldamiseks. Kõrgema taseme abstraktsioonid ja draiverid riistvaraga suhtlemiseks rakendatakse eraldi mikrokiibi pinnal kasutatavate ülesannete kujul, mis toimuvad kasutaja tasemel. Aksesne nendel ülesannetel olevate mikrokiibi ressursside valitsemiseks korraldatakse reeglite määratlemise kaudu.
Allikas: opennet.ru
