13 de noviembre de 2026
Atacamos nuestra propia compilación en cada cambio
Una prueba de seguridad que no puede fallar no demuestra nada. Por eso las pruebas de NoWayOS vienen con versiones hechas para fallar, y sus controles viven donde una pull request no puede alcanzarlos.
Esta es una pregunta incómoda para cualquier prueba de seguridad: ¿ha fallado alguna vez? Una prueba que nunca ha fallado puede estar pasando porque el sistema es sólido, o porque la prueba no ve nada en absoluto. Desde fuera, las dos cosas se ven exactamente igual.
Por eso NoWayOS no se limita a probar su seguridad. La ataca, en cada cambio, y comprueba que los ataques se detienen.
Alargar la mano hacia lo ajeno
Cada parte de un sistema NoWayOS se ejecuta en su propio compartimento sobre seL4, y solo tiene lo que se le concedió. Las pruebas de aislamiento envían sondas a propósito a través de esas fronteras. Una lee una dirección que nunca se le dio. Otra escribe en una página que solo puede leer. Otra, que tiene exactamente lo que tiene la interfaz de usuario, intenta escribir en la página de control de la pantalla, que la interfaz solo puede leer. Otra más, que tiene exactamente lo que tiene el cliente de red, intenta escribir en la memoria del controlador de red.
seL4 debe detenerlas todas, y una parte ajena al asunto debe seguir funcionando, intacta.
Una prueba hecha para fallar
Luego viene el giro. Junto a la prueba de aislamiento de la interfaz de usuario hay una variante con una concesión ampliada a propósito: al sustituto de la interfaz se le da la página privada de la pantalla. La prueba de esa variante debe fallar. Si alguna vez pasara, la prueba de aislamiento estaría ciega, y la compilación lo diría.
La misma idea recorre el resto de las comprobaciones. Cada decodificador de mensajes entre partes tiene demostraciones acotadas, del verificador de modelos Kani, de que nunca entra en pánico, nunca se desborda y nunca lee fuera de los límites. Después, las comprobaciones por mutación rompen los decodificadores deliberadamente, para mostrar que las demostraciones lo notan. Cada analizador de entradas externas se somete a fuzzing con datos hostiles.
Todo ello forma parte de make ci, el control que debe superar cada cambio. Las pruebas de aislamiento se ejecutan siempre; una demostración o una sesión de fuzzing se repite cada vez que cambia el código que cubre.
Una prueba hecha para fallar
La pruebaLa sonda intenta alcanzar una página que nunca se le concedió. seL4 la detiene, y la prueba pasa.
La varianteUna concesión se amplía a propósito. La sonda pasa, así que esta prueba debe fallar. Si alguna vez pasara, la primera prueba estaría ciega.
Controles fuera de alcance
Un control solo es tan fuerte como la mano que puede cambiarlo. Por eso las comprobaciones que debe superar cada contribución a NoWayOS están definidas en Defence Agent, un repositorio público propio. Una pull request que toca un control se señala al mantenedor.
Defence Agent se prueba a sí mismo del mismo modo: veinte pull requests trucadas, cada una con algo oculto que a un revisor se le podría escapar. Hay texto oculto de derecha a izquierda en un comentario, una letra cambiada por su doble cirílica, una dependencia obtenida directamente de un repositorio git, un workflow que ejecutaría código no fiable. Todas deben detectarse, mientras que tres cambios reales anteriores deben pasar.
Evidencias, no adjetivos
Nada de esto hace que un dispositivo sea “inhackeable”. Nada lo hace, y nunca lo diremos. Lo que le da son evidencias: un registro de lo que se intentó, de lo que se detuvo, y el comando que lo muestra. Lea las evidencias de una imagen real, o los propios controles.