Arbetet med den matematiska formella verifieringen av tillförlitlighet och sÀkerhet för mikroarkitekturen seL4 pÄ system med AArch64-kommandosetarkitektur Àr slutfört. Verifieringen omfattar ett matematiskt bevis för seL4:s korrekthet, vilket bekrÀftar att det helt överensstÀmmer med specifikationerna uppstÀllda pÄ det formella sprÄket. Beviset för tillförlitlighet möjliggör anvÀndning av seL4 i kritiska system baserade pÄ ARM64-processorer som krÀver en högre sÀkerhetsnivÄ och garanterar att inga fel intrÀffar.
ĂndĂ„ blev mikroarkitekturen seL4 först verifierad för 32-bits ARM-processorer och senare för 64-bits x86- och RISC-V-processorer. Verifieringen garanterar att om det intrĂ€ffar ett fel i en del av systemet, sĂ„ sprider sig inte detta fel till resten av systemet och dess kritiska komponenter. I sĂ€kerhetskontexten bekrĂ€ftar verifieringen att kĂ€rnan upprĂ€tthĂ„ller en adekvat isoleringsnivĂ„ för applikationer, förhindrar att de fĂ„r Ă„tkomst till information utan auktorisation och garanterar att om sekundĂ€ra applikationer komprometteras, sprider sig inte attacken till kritiska applikationer.
Arkitekturen för mikroarkitekturen seL4 kĂ€nnetecknas av att man flyttar delar av kĂ€rnans resurskontroll till anvĂ€ndarutrymmet och tillĂ€mpar samma Ă„tkomstkontrollmetoder för dessa resurser som för anvĂ€ndarresurser. Mikroarkitekturen tillhandahĂ„ller ingen fĂ€rdig hög-nivĂ„-abstraktion för hantering av filer, processer, nĂ€tverksanslutningar osv., utan ger endast minimala mekanismer för att hantera Ă„tkomsten till det fysiska adressutrymmet, avbrott och processorresurser. HögnivĂ„abstraktioner och drivrutiner för interaktion med hĂ„rdvara implementeras separat ovanpĂ„ mikroarkitekturen i form av uppgifter som körs pĂ„ anvĂ€ndarnivĂ„. Ă
tkomsten för sÄdana uppgifter till mikroarkitekturens resurser organiseras genom faststÀllande av regler.
KĂ€lla: opennet.ru
