Puna e verifikimit formal matematikor për qëndrueshmërinë dhe sigurinë e funksionimit të mikro-bërthamës seL4 në sistemet me arkitekturë komandash AArch64 ka përfunduar. Verifikimi përmbledh provimin matematikor të saktësisë së funksionimit të seL4, i cili dëshmon pajtueshmërinë e plotë me specifikimet e dhëna në një gjuhë formale. Prova e qëndrueshmërisë lejon përdorimin e seL4 në sisteme kritike të bazuara në procesorë ARM64, që kërkojnë një nivel të lartë sigurie dhe garantojnë mungesën e dështimeve.
Fillimisht, mikro-bërthama seL4 u verifikua për procesorë 32-bit ARM, dhe më vonë për procesorë 64-bit x86 dhe RISC-V. Verifikimi garanton që në rast të një dështimi në një pjesë të sistemit, kjo dështim nuk do të përhapet në pjesën tjetër të sistemit dhe në pjesët e tij kritike. Në kontekstin e sigurimit, verifikimi konfirmon se bërthama siguron nivelin e zakonshëm të izolimit të aplikacioneve, nuk lejon që ato të aksesojnë informacionin pa autorizim dhe garanton që në rast të kompromisit të aplikacioneve dytësore, sulmi nuk do të përhapet në aplikacionet kritike.
Arkitektura e mikrokernelit seL4 dallohet për zhvendosjen e pjesëve të menaxhimit të burimeve të kernelit në hapësirën e përdoruesit dhe për përdorimin e të njëjtave mekanizma të kontrollit të aksesit për këto burime si për burimet e përdoruesit. Mikrokerneli nuk ofron abstraksione të gatshme të nivelit të lartë për menaxhimin e skedarëve, proceseve, lidhjeve të rrjetit etj.; në vend të kësaj, ai ofron vetëm mekanizmat minimalë për menaxhimin e aksesit në hapësirën fizike të adresave, ndërprerjet dhe burimet e procesorit. Abstraksionet e nivelit të lartë dhe drajverët për ndërveprim me pajisjet implementohen veçmas mbi mikrokernelin në formën e detyrave që ekzekutohen në nivel përdoruesi. Aksesi i këtyre detyrave te burimet që mikrokerneli ka në dispozicion organizohet përmes përcaktimit të rregullave.
Burimi: opennet.ru
