Mikrokärnan seL4 är matematiskt verifierad för RISC-V-arkitekturen.
Organisationen RISC-V Foundation meddelade om verifieringen av mikrooperativsystemet seL4 på system med RISC-V instruktioner. Verifieringen handlar om ett matematiskt bevis för pålitligheten hos seL4, vilket visar att den uppfyller de specificerade formella specifikationerna. Beviset för pålitlighet möjliggör användning av seL4 i kritiska system baserade på RISC-V RV64-processorer som kräver en högre nivå av tillförlitlighet och garanterar att inga […]
