La seguridad del kernel, a prueba

Investigadores australianos afirman que pueden probar, matemáticamente, que el código que han desarrollado, diseñado para controlar la seguridad de los sistemas, está libre de la mayoría de tipos de error. Se trata de la primera máquina de comprobación de errores para el kernel de un sistema operativo de propósito general. Al kernel se le llama microkernel seL4.

Aunque comprobar de forma rigurosa la calidad de un código es caro, el desarrollo de este tipo de pruebas tiene un efecto secundario, que es el de mejorar el software en general. La mayoría de las clases de ataque, como los que explotan vulnerabilidades de desbordamiento de buffer, no tendrían éxito con el microkernel seL4.