Pabeigta matemātiskā formālā verifikācija seL4 mikro kodola uzticamības un drošības nodrošināšanai AArch64 arhitektūras sistēmās. Verifikācija attiecas uz matemātisku pierādījumu par seL4 darbības pareizību, kas apliecina tās atbilstību noteiktajām specifikācijām formālajā valodā. Uzticamības pierādījums ļauj izmantot seL4 kritiskās svarīgās sistēmās, kas balstītas uz ARM64 procesoriem, kas prasa augstāku drošības līmeni un garantē kļūdu prombūtni.
Sākotnēji seL4 mikro kodols tika verificēts 32-bit ARM procesoriem, bet vēlāk arī 64-bit x86 un RISC-V procesoriem. Verifikācija garantē, ka gadījumā, ja kādā sistēmas daļā rodas kļūda, tā neizplatās uz pārējo sistēmu un tās kritiskajām daļām. Drošības nodrošināšanas kontekstā verifikācija apstiprina, ka kodols nodrošina atbilstošu lietojumprogrammu izolāciju, nepieļaujot piekļuvi informācijai bez autorizācijas un garantējot, ka gadījumā, ja sekundārās lietojumprogrammas tiek kompromitētas, uzbrukums neizplatās uz kritiski svarīgām lietojumprogrammām.
seL4 mikro kodola arhitektūra izceļas ar to, ka kodola resursu pārvaldības daļas ir pārvietotas uz lietotāja telpu un šiem resursiem tiek pielietoti tie paši piekļuves ierobežošanas līdzekļi, kā lietotāju resursiem. Mikro kodols nesniedz gatavas augsta līmeņa abstrahācijas failu, procesu, tīkla savienojumu un tamlīdzīgu pārvaldībai, bet gan piedāvā minimālus mehānismus fiziskās adresācijas telpas, traucējumu un procesora resursu piekļuves pārvaldībai. Augsta līmeņa abstrahācijas un vadītāji, lai sadarbojoties ar aparatūru, tiek realizētas atsevišķi virs mikro kodola kā uzdevumi, kas tiek izpildīti lietotāja līmenī. Šo uzdevumu piekļuve mikro kodola resursiem tiek organizēta, nosakot noteikumus.
Avots: opennet.lv
