Užbaigtas formalus matematinis seL4 mikrobranduolio patikimumo ir saugumo sistemose su AArch64 instrukcijų rinkinio architektūra patikrinimas. Patikrinimą sudaro matematinis seL4 veikimo teisingumo įrodymas, kuris parodo visišką atitiktį formalioje kalboje apibrėžtoms specifikacijoms. Šis patikimumo įrodymas leidžia naudoti seL4 kritinėse sistemose, pagrįstose ARM64 procesoriais, kurioms reikalingas aukštas saugumo lygis ir garantuojamas gedimų nebuvimas.
Iš pradžių „seL4“ mikrobranduolys buvo patikrintas 32 bitų ARM procesoriams, o vėliau – 64 bitų x86 ir RISC-V procesoriams. Patikrinimas užtikrina, kad gedimui įvykus vienoje sistemos dalyje, jis neišplis į likusią sistemos dalį ir jos svarbiausius komponentus. Saugumo kontekste patikrinimas patvirtina, kad branduolys užtikrina tinkamą programų izoliacijos lygį, neleidžia joms pasiekti informacijos be leidimo ir užtikrina, kad jei antrinės programos būtų pažeistos, ataka neišplistų į svarbiausias programas.
SeL4 mikrobranduolio architektūra pasižymi tuo, kad juda dalys, skirtos branduolio ištekliams valdyti į vartotojo erdvę, ir tokiems ištekliams naudoja tuos pačius prieigos kontrolės įrankius kaip ir vartotojo ištekliams. Mikrobranduolys nesuteikia paruoštų aukšto lygio abstrakcijų failams, procesams, tinklo ryšiams ir panašiai valdyti, o tik minimalius mechanizmus, skirtus kontroliuoti prieigą prie fizinės adresų erdvės, pertraukimų ir procesoriaus išteklių. Aukšto lygio abstrakcijos ir sąveikos su aparatine įranga tvarkyklės yra įdiegtos atskirai ant mikrobranduolių, vartotojo lygio užduočių pavidalu. Tokių užduočių prieiga prie mikrobranduoliui prieinamų išteklių organizuojama apibrėžiant taisykles.
Šaltinis: opennet.ru
