Seguridad

Solo se ocupa de lo suyo.

Un dispositivo NoWayOS deja fuera lo que su tarea no necesita y sella lo que queda en compartimentos. Esta página explica en qué se basa, qué está demostrado, qué no lo está todavía y qué le corresponde a usted hacer bien.

Lo que se deja fuera

Una imagen de NoWayOS contiene su aplicación, los controladores que esa aplicación usa y el micronúcleo seL4. No hay motor de navegador, ni sistema de ventanas, ni shell, ni gestor de paquetes, ni cuentas de usuario: nada de eso se incorporó nunca, así que no hay nada de eso que explotar, parchear o configurar mal. NoWayOS está diseñado para reducir el software y los servicios innecesarios: si la tarea no lo necesita, no está en la imagen.

Ese es el significado del nombre: no hay manera de explotar lo que nunca se incorporó. Es una afirmación sobre lo que está ausente, no una promesa de que nada pueda salir mal. Lo que sí está incorporado puede tener errores; lo que afirmamos es que hay mucho menos, y que un error se queda en su compartimento.

Bloquear un sistema de propósito general es seguro por configuración: las funciones bloqueadas siguen presentes, y un solo error puede saltarse todos los ajustes. NoWayOS aspira a ser seguro por construcción: esas funciones nunca estuvieron ahí.

Cómo se contiene un fallo

Cada parte se ejecuta en su propio dominio de protección, con su propia memoria, y solo posee las capacidades que le concede su descripción de sistema. seL4 las hace cumplir.
Cada concesión figura en el archivo de concesiones del sistema, y la compilación falla si la descripción concede algo que el archivo no enumera, o al revés. Ampliar una concesión se revisa como un cambio de seguridad.
Los mensajes entre partes son registros de tamaño fijo, copiados fuera de la memoria compartida antes de comprobarse, así que un emisor no puede cambiar un registro después de que haya pasado la comprobación.
La entrada es hostil hasta que se comprueba. Cada analizador de entrada externa pasa por fuzzing y está construido para no entrar nunca en pánico, y las aplicaciones ven eventos de teclado, de puntero y táctiles, nunca protocolos de dispositivo.
Un supervisor detiene una parte que falla y reinicia el sistema en limpio. Los fallos repetidos llevan el dispositivo a un estado de fallo seguro hasta un arranque en frío.

Qué cubren las demostraciones de seL4, y qué no

seL4 es un micronúcleo de unas 10 000 líneas, con demostraciones de corrección y seguridad comprobadas por máquina. Esas demostraciones son un logro poco común, y son válidas para configuraciones específicas en plataformas específicas. Esta es la posición exacta:

NoWayOS se ejecuta sobre el micronúcleo seL4, que cuenta con demostraciones de corrección y seguridad comprobadas por máquina para configuraciones específicas en nuestro hardware; NoWayOS usa la configuración de criticidad mixta de seL4, cuyas demostraciones están en curso.

Plataforma: la configuración verificada de seL4 para AArch64 incluye la Raspberry Pi 5 y los i.MX8M Mini, Plus y Quad de NXP.
Planificación: Microkit compila el núcleo de criticidad mixta (MCS) de seL4, cuyas demostraciones para AArch64 están en curso. Por eso, hoy ninguna imagen de NoWayOS está dentro de las demostraciones completadas de seL4.
Núcleos de CPU: las demostraciones son para el núcleo de seL4 en configuración monoprocesador (un solo núcleo de CPU). Una imagen que usa varios núcleos de CPU queda fuera de ellas, y lo dice.
Por encima del núcleo: las herramientas de Microkit y los dominios de protección y controladores de NoWayOS no están cubiertos por las demostraciones de seL4. Su garantía procede de Rust, del aislamiento, de la revisión, de las pruebas y de las demostraciones acotadas propias de NoWayOS.

Cada imagen registra su configuración en un sel4-config.txt junto a ella. Esto es lo que dice de sí mismo el registro de una compilación de desarrollo del sistema hello:

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

Ni siquiera una imagen cuyo núcleo coincidiera con todas las opciones de la configuración verificada se llamaría aquí “verificada”. El registro expone los hechos, y los hechos bastan.

Las evidencias, y el comando de cada una

Cada afirmación de esta página viene con sus evidencias, y cada evidencia sale de un comando que cualquiera puede ejecutar en el contenedor de desarrollo. make ci los ejecuta en orden, y make ci CI_SCOPE=full ejecuta todas las demostraciones y todos los objetivos de fuzzing; Comprobaciones y evidencias explica cada uno.

La afirmación	La evidencia	Ejecútelo
Cada concesión está por escrito.	El archivo de concesiones de cada sistema, cotejado con su descripción de sistema en cada compilación.	`make qemu-test SYSTEM=hello`
Una parte no puede alcanzar lo que no se le ha concedido.	Pruebas de aislamiento cuyas sondas hacen lecturas y escrituras no concedidas, que seL4 debe impedir, y una variante con una concesión ampliada a propósito, que debe fallar.	`make qemu-test SYSTEM=isolation-test`
Los decodificadores de mensajes aguantan cualquier entrada hasta un límite.	Demostraciones de Kani para cada decodificador de registros de mensajes, con pruebas de mutación que muestran que las demostraciones pueden fallar.	`make kani`
Los analizadores de entrada externa resisten la entrada hostil.	Un objetivo de fuzzing para cada analizador de entrada no confiable. Un fallo, una vez corregido, se convierte en una prueba de regresión.	`make fuzz`
El código unsafe solo está donde está aprobado.	Una lista de permitidos con los pocos crates y archivos que pueden usarlo, que make ci hace cumplir, con Miri ejecutado sobre esos crates.	`make unsafe-audit`
Se conoce cada componente.	Una lista de materiales de software CycloneDX para cada espacio de trabajo y cada imagen de sistema, cada componente con su hash.	`make image-sbom SYSTEM=hello`
Se comprueban las licencias y los avisos de seguridad.	cargo-deny sobre cada espacio de trabajo: licencias, orígenes, crates prohibidos y avisos de seguridad conocidos.	`make deny`
No hay secretos en el código.	El árbol y cada commit, analizados sin conexión en busca de claves y credenciales.	`make secrets`
La configuración de seL4 de cada imagen queda registrada.	Un sel4-config.txt junto a cada imagen, y una comprobación de que los valores de referencia del registro coinciden con el SDK de Microkit fijado.	`make sel4-config-check`

Lea las evidencias de una imagen

No necesita compilar nada para ver qué aspecto tienen las evidencias. Aquí están todas las de una imagen real: ui-interactive, la interfaz de usuario interactiva, compilada para QEMU el 1 de noviembre de 2026.

Su lista de materiales de software (CycloneDX 1.5): 62 componentes, desde el núcleo seL4 y el cargador de Microkit hasta cada crate de cada dominio de protección, cada uno con su SHA-256.
Su registro de configuración de seL4: el núcleo que ejecuta, opción por opción frente a la configuración verificada de seL4, y dónde queda claramente fuera de las demostraciones.
Su descripción de sistema: cada dominio de protección, región de memoria, interrupción y canal, tal como los construye Microkit.
Su archivo de concesiones: las mismas concesiones puestas por escrito, un hecho por línea, que la compilación coteja con la descripción.
La pantalla que dibuja, comparada píxel a píxel con esta imagen aprobada cada vez que se ejecuta su prueba.

Lo que le corresponde a usted

NoWayOS es una plataforma, no un producto certificado. Un dispositivo seguro también depende de cómo se despliega y se opera, y esa parte corresponde a quien lo construye y lo opera.

Seguridad física. Un dispositivo que se le conecte o una mano en el cable de alimentación aún pueden dejarlo fuera de servicio. Las carcasas, los puertos y la alimentación forman parte del diseño del producto construido sobre NoWayOS.
Lo que concede cada sistema. NoWayOS comprueba que un sistema y su archivo de concesiones coinciden. Si esas concesiones son las adecuadas para la tarea es una decisión de diseño, y debe revisarse como tal.
Redes y sistemas de back-end. Un dispositivo solo se conecta a los destinos que permite su sistema. Proteger lo que esos servicios hacen con lo que reciben les corresponde a ellos.
Claves y actualizaciones. Las actualizaciones firmadas que, si algo falla, vuelven atrás de forma segura están diseñadas, pero todavía no construidas. Quién custodia las claves de firma y cómo se aprueba una versión es una decisión de operación.
Certificación. Los productos regulados que funcionan sobre NoWayOS llevan su propia certificación. NoWayOS está diseñado para aportar las evidencias que necesitan; él mismo no está certificado.

Aún no construido

El arranque seguro y la atestación corresponden al hardware de producción con una raíz de confianza en hardware. Ninguno de los dos está construido.
Actualizaciones firmadas aplicadas en el dispositivo. Los registros de actualización y sus comprobaciones existen; la vía que aplica una actualización en un dispositivo, todavía no.
La Raspberry Pi 5 es una placa de desarrollo, no un dispositivo reforzado. Quien tenga una en la mano puede cambiar su software, y el acceso a memoria de los dispositivos USB todavía no está confinado en ella.

Palabras que no encontrará aquí

No decimos que NoWayOS sea “inhackeable”, “a prueba de manipulaciones” ni “a prueba de balas”, y no afirmamos que tenga “superficie de ataque cero”. Nada lo es, y haría bien en dejar de leer. Las afirmaciones de esta página son más modestas, y cada una viene con sus evidencias.

Informar de una vulnerabilidad

Informe de una vulnerabilidad en privado, mediante el sistema de notificación privada de vulnerabilidades de GitHub en la pestaña Security del repositorio o por correo electrónico a security@nowayos.com, como describe el SECURITY.md de cada repositorio, y no en una incidencia pública. Como cada parte se ejecuta en su propio compartimento, un fallo está diseñado para quedarse donde está mientras se prepara una corrección.