Het werk aan de wiskundige formele verificatie van de betrouwbaarheid en veiligheid van de seL4-microkernel op systemen met de AArch64-instructieset is voltooid. De verificatie is terug te brengen tot een wiskundig bewijs van de correctheid van de werking van seL4, wat getuigt van volledige conformiteit met de op een formele manier vastgestelde specificaties. Het bewijs van de betrouwbaarheid maakt het mogelijk seL4 te gebruiken in kritische systemen gebaseerd op ARM64-processors, die een hoger niveau van veiligheid vereisen en garant staan voor de afwezigheid van storingen.
Oorspronkelijk was de seL4-microkernel geverifieerd voor 32-bits ARM-processors en later voor 64-bits x86 en RISC-V-processors. De verificatie garandeert dat in het geval van een storing in een deel van het systeem, deze storing zich niet zal verspreiden naar de overige delen van het systeem en zijn kritische delen. In de context van veiligheid bevestigt de verificatie dat de kernel een passend niveau van isolatie voor applicaties biedt, zodat zij geen toegang krijgen tot informatie zonder autorisatie en garandeert dat in het geval van compromittering van secundaire applicaties, een aanval zich niet verspreidt naar kritieke applicaties.
De architectuur van de seL4-microkernel is opmerkelijk vanwege het verplaatsen van delen voor de beheersing van kernelbronnen naar de gebruikersruimte en het toepassen van dezelfde toegangscontrolemechanismen voor deze bronnen als voor gebruikersbronnen. De microkernel biedt geen kant-en-klare hoge abstracties voor het beheer van bestanden, processen, netwerkverbindingen, enzovoort; in plaats daarvan biedt het slechts minimale mechanismen voor het beheer van de toegang tot fysieke adressen, onderbrekingen en CPU-bronnen. Hoge abstracties en stuurprogramma's voor interactie met hardware worden apart boven op de microkernel geĆÆmplementeerd in de vorm van taken die op gebruikersniveau worden uitgevoerd. De toegang van deze taken tot de resources van de microkernel wordt georganiseerd door het definiĆ«ren van regels.
Bron: opennet.ru
