Verificação formal de segurança do microkernel seL4 para a arquitetura AArch64 finalizada
Concluído o trabalho de verificação formal matemática da confiabilidade e segurança do microkernel seL4 em sistemas com arquitetura de conjunto de instruções AArch64. A verificação consiste em uma prova matemática da correção do seL4, que indica conformidade total com as especificações definidas em linguagem formal. A prova de confiabilidade permite o uso do seL4 em sistemas críticos baseados em processadores ARM64, que exigem alto nível de segurança e […]
