seL4 completa las pruebas de seguridad en AArch64

SeL4 security proofs now complete on AArch64

Proofcraft ha completado la prueba formal de confidencialidad para el microkernel seL4 en AArch64, lo que culmina el conjunto de pruebas de seguridad para esta arquitectura. Con el apoyo continuo de NCSC, se demuestra matemáticamente que el kernel impide que las aplicaciones accedan a información sin autorización, garantizando el aislamiento entre aplicaciones críticas y no críticas. Este hito se suma a las pruebas de corrección funcional e integridad ya completadas, consolidando a seL4 como el kernel con mayor aseguramiento formal.