O microkernel seL4 foi verificado matematicamente para a arquitetura RISC-V
A organização RISC-V Foundation anunciou a verificação do funcionamento do microkernel seL4 em sistemas com a arquitetura do conjunto de comandos RISC-V. A verificação consiste em uma prova matemática da confiabilidade do funcionamento do seL4, que comprova total conformidade com as especificações dadas em linguagem formal. A prova de confiabilidade permite o uso do seL4 em sistemas críticos baseados em processadores RISC-V RV64, que exigem um nível elevado de confiabilidade e garantem a ausência de […]
