Formele verificatie van de veiligheid van de seL4-microkernel is uitgevoerd voor de AArch64-architectuur
Het werk aan de wiskundige formele verificatie van de betrouwbaarheid en veiligheid van de microkernel seL4 op systemen met de AArch64-instructiesetarchitectuur is afgerond. De verificatie komt neer op een wiskundig bewijs van de correctheid van seL4, wat getuigt van volledige naleving van de specificaties die in de formele taal zijn opgesteld. Het bewijs van betrouwbaarheid maakt het mogelijk om seL4 te gebruiken in kritieke systemen gebaseerd op ARM64-processoren, die een verhoogd beveiligingsniveau vereisen en […]
