De formele wiskundige verificatie van de betrouwbaarheid en veiligheid van de seL4-microkernel op systemen met de AArch64-instructiesetarchitectuur is afgerond. De verificatie bestaat uit een wiskundig bewijs van de correctheid van de werking van seL4, waaruit blijkt dat volledig wordt voldaan aan de specificaties die in de formele taal zijn gedefinieerd. Dit betrouwbaarheidsbewijs maakt het gebruik van seL4 mogelijk in bedrijfskritische systemen gebaseerd op ARM64-processoren die een hoog beveiligingsniveau vereisen en de afwezigheid van storingen garanderen.
De seL4-microkernel werd aanvankelijk geverifieerd voor 32-bits ARM-processors en later voor 64-bits x86- en RISC-V-processors. Verificatie garandeert dat een storing in een deel van het systeem zich niet verspreidt naar de rest van het systeem en de kritieke componenten. In de context van beveiliging bevestigt verificatie dat de kernel de juiste mate van applicatie-isolatie biedt, voorkomt dat applicaties zonder toestemming toegang krijgen tot informatie en ervoor zorgt dat een aanval die secundaire applicaties compromittert, zich niet verspreidt naar kritieke applicaties.
De architectuur van de seL4-microkernel onderscheidt zich door het verwijderen van onderdelen voor het beheer van kernelbronnen naar de gebruikersruimte en door het gebruik van dezelfde toegangscontrole voor dergelijke bronnen als voor gebruikersbronnen. De microkernel biedt geen kant-en-klare abstracties op hoog niveau voor het beheer van bestanden, processen, netwerkverbindingen, enz., maar slechts minimale mechanismen voor het beheer van de toegang tot de fysieke adresruimte, interrupts en processorbronnen. Abstracties op hoog niveau en drivers voor interactie met de hardware worden afzonderlijk op de microkernel geïmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van dergelijke taken tot de bronnen die beschikbaar zijn voor de microkernel wordt georganiseerd door het definiëren van regels.
Bron: opennet.ru
