Le micro-noyau seL4 a été mathématiquement vérifié pour l'architecture RISC-V.
L'organisation RISC-V Foundation a annoncé la vérification du micro-noyau seL4 fonctionnant sur des systèmes avec architecture de jeu d'instructions RISC-V. La vérification se résume à une preuve mathématique de la fiabilité du fonctionnement de seL4, témoignant d'une conformité totale aux spécifications établies dans un langage formel. La preuve de fiabilité permet d'utiliser seL4 dans des systèmes critique basés sur des processeurs RISC-V RV64, nécessitant un niveau de fiabilité accru et garantissant l'absence […]
