Glosario

Las palabras, en lenguaje claro.

NoWayOS toma palabras prestadas de los sistemas operativos, de la seguridad y de Rust, y usa algunas en un sentido concreto. Aquí está cada una, en una o dos líneas.

Los términos están en orden alfabético. Un término en cursiva dentro de una definición tiene su propia entrada.

Archivo de concesiones: systems/NAME.grants: todo lo que concede un sistema, un hecho por línea: prioridades, presupuestos, memoria, dispositivos, interrupciones y canales. La compilación falla si la descripción del sistema y el archivo de concesiones no coinciden.
Archivo de salida esperada: systems/NAME.expect: las líneas que un sistema debe imprimir, en orden, y el texto que hace fallar la prueba si aparece en cualquier parte. El mismo archivo comprueba un sistema en QEMU y en la Raspberry Pi 5.
Arranque en frío: Un arranque desde el equipo apagado, a diferencia de un reinicio. Solo un arranque en frío saca a un dispositivo NoWayOS de su estado de fallo seguro.
Arranque seguro: Un dispositivo que se niega a iniciar software que no esté firmado por su fabricante. Previsto para NoWayOS en hardware de producción; todavía no construido.
Atestación: Un dispositivo que demuestra a un servicio remoto, criptográficamente, qué software inició. Muestra lo que se cargó en el arranque, no todo lo que ha ocurrido desde entonces. Prevista para NoWayOS en hardware de producción; todavía no construida.
Atlas de glifos: Una fuente dibujada de antemano, en tiempo de compilación, en imágenes de sus caracteres, para que un dispositivo dibuje texto sin analizar nunca un archivo de fuente.
Base de cómputo de confianza (TCB): Todo aquello de cuya corrección depende una propiedad de seguridad. En un sistema NoWayOS: el núcleo seL4, el cargador y el monitor de Microkit, y los dominios de protección en los que se apoya esa propiedad.
Canal: En Microkit, una conexión declarada entre dos dominios de protección, para notificaciones (señales sin datos, entre ellas las interrupciones) y llamadas a procedimientos protegidos.
Capacidad: En seL4, un testigo infalsificable que designa un objeto del núcleo y los derechos que se tienen sobre él, como una tarjeta de acceso para una sola puerta. Un dominio de protección solo puede tocar lo que designan sus capacidades.
Contenedor de desarrollo: La imagen de contenedor, con versiones fijadas, que contiene toda la cadena de herramientas de NoWayOS: las cadenas de herramientas de Rust, el SDK de Microkit, QEMU y las herramientas de comprobación. Cada objetivo de make se ejecuta en ella, así que su máquina solo necesita Podman y make (y Python 3.11 para controlar una Raspberry Pi 5).
Copiar y después comprobar: La regla según la cual un mensaje se copia fuera de la memoria compartida antes de validarse, para que el emisor no pueda cambiarlo entre la comprobación y su uso. Evita una doble lectura.
CycloneDX: Un formato estándar abierto para listas de materiales de software. NoWayOS genera una para cada espacio de trabajo y cada imagen de sistema. Véase SBOM.
Debug Probe: El adaptador de USB a serie de Raspberry Pi. En el conector de depuración de la Raspberry Pi 5 transporta el registro de arranque y carga imágenes de prueba.
Demostración acotada: Una demostración de que una propiedad se cumple para toda entrada hasta un tamaño indicado. NoWayOS demuestra así sus decodificadores de mensajes, con Kani.
Descripción del sistema: El archivo XML de Microkit que declara cada dominio de protección, región de memoria, canal e interrupción de un sistema. Es el diseño de seguridad del sistema, y un cambio en él se revisa como tal.
Doble lectura (double-fetch): Un error en el que el código comprueba datos en memoria compartida y luego vuelve a leerlos, lo que permite que la otra parte los cambie entre medias. Se evita con copiar y después comprobar.
Dominio de protección (PD): Una parte aislada de un sistema Microkit: un programa con su propia memoria, que solo posee las capacidades que se le conceden explícitamente. Los compartimentos sellados de NoWayOS.
embedded-graphics: Una biblioteca de gráficos 2D en Rust para dispositivos sin la pila gráfica de un sistema operativo. La interfaz de usuario de NoWayOS dibuja con ella.
Error de seguridad de memoria: Un fallo de programación como leer más allá del final de un búfer o usar memoria después de liberarla. Microsoft y Google han informado, cada uno, de que alrededor del 70 % de sus errores de seguridad graves son de este tipo; el Rust seguro los descarta.
Estado de fallo seguro: Adonde va un dispositivo NoWayOS cuando los fallos se repiten: solo siguen funcionando el supervisor, el watchdog y, cuando es posible, la pantalla, hasta un arranque en frío.
Fallo: Lo que notifica seL4 cuando un dominio de protección hace algo que el núcleo no permite, o entra en pánico. La parte permanece detenida hasta que actúa su gestor de fallos.
Fuzzing: Probar un analizador con millones de entradas generadas hasta que una lo hace fallar o rompe una comprobación. Cada analizador de entrada externa de NoWayOS tiene un objetivo de fuzzing.
Hora de reloj: La fecha y la hora del día, procedentes de una fuente autenticada. NoWayOS la mantiene separada del tiempo monótono, como un tipo distinto.
i.MX8: La familia de procesadores Arm industriales de NXP, y el hardware de producción previsto para NoWayOS. Aún no está soportada.
Kani: Un verificador de modelos para Rust que demuestra propiedades para toda entrada hasta un límite. NoWayOS lo usa para demostrar que sus decodificadores de mensajes nunca entran en pánico, se desbordan ni leen fuera de límites.
Mensaje tipado: Un registro de tamaño fijo con una disposición explícita, que se pasa entre dominios de protección a través de memoria compartida y se comprueba al recibirlo. Véase copiar y después comprobar.
Microkit: El framework de la seL4 Foundation para sistemas seL4 estáticos construidos a partir de dominios de protección declarados en una descripción del sistema.
Micronúcleo (microkernel): Un núcleo reducido al mínimo posible, con los controladores, la red y la pantalla funcionando fuera de él, cada uno en su propio compartimento. seL4 es uno.
Miri: Un intérprete para Rust que detecta comportamiento indefinido. NoWayOS lo ejecuta sobre los pocos crates a los que se permite código unsafe.
Núcleo de criticidad mixta (MCS): La configuración de seL4 con presupuestos y periodos de planificación, que es la que compila Microkit. Sus demostraciones para AArch64 están en curso, así que hoy ninguna imagen de NoWayOS está dentro de las demostraciones completadas de seL4.
Prueba de aislamiento: Un sistema que intenta alcanzar lo que no se le ha concedido, y que seL4 debe impedir. Una variante con una concesión ampliada a propósito debe fallar, lo que demuestra que la prueba es capaz de fallar.
QEMU: Un emulador de máquinas de código abierto. Cada sistema NoWayOS arranca en él, y comprueba su propia salida, antes de tocar hardware.
Raspberry Pi 5: La placa de bajo coste que NoWayOS usa como hardware de referencia.
Rust: Un lenguaje de programación cuyo código seguro descarta los errores de seguridad de memoria. El código propio de NoWayOS es Rust de principio a fin.
rust-sel4: El soporte de Rust de la seL4 Foundation, que incluye el crate para escribir dominios de protección de Microkit.
rustls: Una biblioteca TLS escrita en Rust. El cliente TLS 1.3 de NoWayOS está construido sobre ella, junto con RustCrypto.
SBOM: Una lista de materiales de software (software bill of materials): una relación de cada componente y versión de un software. NoWayOS genera una en CycloneDX para cada espacio de trabajo y cada imagen de sistema.
Screen Compiler: La herramienta de compilación de NoWayOS que convierte pantallas de React, escritas en TSX dentro de un subconjunto admitido, en Rust para la interfaz de usuario de NoWayOS. Rechaza todo lo que queda fuera del subconjunto en lugar de aproximarlo.
sDDF: El seL4 Device Driver Framework: un diseño de referencia para controladores sobre Microkit, con colas en memoria compartida. Las colas de red de NoWayOS lo siguen.
Seguro por configuración: Hacer más seguro un dispositivo de propósito general cambiando sus ajustes. Las funciones siguen ahí, y un solo error puede saltarse todos los ajustes.
Seguro por construcción: Hacer un dispositivo que no puede hacer las cosas arriesgadas porque nunca se incorporaron. El enfoque de NoWayOS.
seL4: Un micronúcleo de unas 10 000 líneas, mantenido por la seL4 Foundation, con demostraciones de corrección y seguridad comprobadas por máquina para configuraciones específicas. NoWayOS se ejecuta sobre él.
sel4-config.txt: El registro que se escribe junto a cada imagen de NoWayOS: su configuración de seL4, y si esa configuración está dentro de las demostraciones completadas de seL4.
Single Purpose OS: Un sistema operativo construido para la única tarea de un dispositivo, en lugar de construirse para ejecutar cualquier cosa y luego restringirse a una sola. Tres rasgos lo definen: está hecho para una sola tarea (su imagen contiene la aplicación, los controladores que usa y el núcleo, y nada más); está sellado por dentro (cada parte en su propio compartimento, alcanzando solo lo que se le ha concedido); y se deja comprobar (las evidencias de lo que contiene vienen con él). No es un modo quiosco, que restringe un sistema seguro por configuración a una sola aplicación. NoWayOS es un Single Purpose OS: una máquina sin nada más que hacer.
smoltcp: Una pila TCP/IP en Rust que no reserva memoria mientras funciona. La pila de red de NoWayOS está construida sobre ella.
Superficie de ataque: Todo lo que un atacante podría intentar usar contra un dispositivo: su código, sus servicios, sus interfaces y sus entradas. Menos código y menos funciones dejan menos superficie.
Supervisor: El dominio de protección que recibe los fallos de las demás partes, los notifica y reinicia el sistema en limpio.
Tiempo monótono: Tiempo contado desde el arranque, que nunca se ajusta y nunca retrocede. Todos los plazos de espera de NoWayOS lo usan, y nunca se mezcla con la hora de reloj.
unsafe: Código Rust cuya seguridad de memoria el compilador no puede comprobar. Prohibido en todos los crates de NoWayOS salvo en una lista breve y revisada que las comprobaciones hacen cumplir.
Verificación formal: Demostración matemática, comprobada por máquina, de que un software cumple su especificación. seL4 la tiene para configuraciones específicas. El código propio de NoWayOS se apoya en cambio en Rust, el aislamiento, las pruebas y las demostraciones acotadas.
Watchdog: Un temporizador de hardware que reinicia la placa a menos que el software lo atienda. El dominio de protección watchdog de NoWayOS solo lo atiende mientras todas las demás partes responden a su señal de vida.