Werk aan die formele wiskundige verifikasie van die betroubaarheid en sekuriteit van die seL4-mikrokern op stelsels met die AArch64-instruksiestel-argitektuur is voltooi. Verifikasie bestaan uit 'n wiskundige bewys van die korrektheid van seL4-werking, wat volle voldoening aan die spesifikasies wat in die formele taal gedefinieer is, demonstreer. Hierdie bewys van betroubaarheid maak die gebruik van seL4 moontlik in missie-kritieke stelsels gebaseer op ARM64-verwerkers wat 'n hoë vlak van sekuriteit vereis en die afwesigheid van mislukkings waarborg.
Die seL4-mikrokern is aanvanklik geverifieer vir 32-bis ARM-verwerkers, en later vir 64-bis x86- en RISC-V-verwerkers. Verifikasie verseker dat indien 'n fout in een deel van die stelsel voorkom, dit nie na die res van die stelsel en sy kritieke komponente sal versprei nie. In die konteks van sekuriteit bevestig verifikasie dat die kern die toepaslike vlak van toepassingsisolasie bied, verhoed dat hulle toegang tot inligting sonder magtiging verkry, en verseker dat indien sekondêre toepassings gekompromitteer word, die aanval nie na kritieke toepassings sal versprei nie.
Die seL4 mikrokern-argitektuur is opvallend vir bewegende dele vir die bestuur van kernhulpbronne in gebruikersruimte en die gebruik van dieselfde toegangsbeheernutsmiddels vir sulke hulpbronne as vir gebruikershulpbronne. Die mikrokern verskaf nie klaargemaakte hoëvlak-abstraksies vir die bestuur van lêers, prosesse, netwerkverbindings en dies meer nie, maar bied slegs minimale meganismes vir die beheer van toegang tot fisiese adresruimte, onderbrekings en verwerkerhulpbronne. Hoëvlak-abstraksies en drywers vir interaksie met hardeware word afsonderlik bo-op die mikrokern geïmplementeer in die vorm van gebruikersvlaktake. Toegang van sulke take tot die hulpbronne beskikbaar vir die mikrokern word georganiseer deur die definisie van reëls.
Bron: opennet.ru
