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.
Este aislamiento evita que los ataques a aplicaciones no críticas se propaguen a aplicaciones críticas y las comprometan.
- StilesCrisis
Próximamente: un ataque de canal lateral por temporización que invalida por completo este resultado
- i_am_a_peasant
Lean la letra pequeña: "no-MCS (sistemas de criticidad mixta), un núcleo"
- kvuj
¿Qué sistemas operativos usan seL4? Conozco los siguientes:
- GenodeOS
- LionsOS
- Un fabricante de coches chino lo usaba como hipervisor en sus coches, si no recuerdo mal
- ¿Qué más? ¿Conocéis algún despliegue privado?
- avadodin
Los mercados de sistemas embebidos y militares pueden seguir financiándolos en el futuro previsible, pero necesitan un seL4/Linux nativo si quieren afirmar honestamente que están mejorando la seguridad de los sistemas con su modelo de capacidades.
Las plataformas de virtualización con arranque seguro están a la orden del día hoy en día.