Cómo encaja un sistema

Cada dispositivo NoWayOS es un sistema: un conjunto fijo de partes, declarado antes de construirse, cada una aislada de las demás por seL4. No se añade nada en tiempo de ejecución. Esta página explica las piezas y cómo se conectan.

Dominios de protección

Un dominio de protección es una parte de un sistema: un programa con su propia memoria, que solo posee las capacidades que se le conceden. En seL4, una capacidad es 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 no puede tocar nada que sus capacidades no designen, y seL4 lo hace cumplir.

Un sistema típico tiene un dominio de protección para cada asunto: un controlador de pantalla, la ruta de entrada, la pila de red, la interfaz de usuario, la aplicación, un temporizador, un supervisor y un watchdog. Cada uno es un pequeño programa en Rust, no_std, que no reserva memoria después de arrancar.

La descripción del sistema

La descripción de sistema de Microkit (systems/NAME.system, un archivo XML) declara el sistema completo: cada dominio de protección con su prioridad, su presupuesto y su pila; cada región de memoria y quién la mapea; cada canal; cada interrupción.

• Las descripciones nombran dispositivos, nunca direcciones: phys_addr="@NAME". Las direcciones salen del archivo de la placa en platforms/, cada una con su fuente, así que la misma descripción se compila para QEMU y para la Raspberry Pi 5.
• Los canales conectan dos dominios de protección, para notificaciones (señales sin datos, entre ellas las interrupciones) y llamadas a procedimientos protegidos (llamadas síncronas a una parte de mayor prioridad).

La descripción es el diseño de seguridad del sistema, así que un cambio en ella se revisa como un cambio de seguridad.

El archivo de concesiones

Junto a cada descripción, systems/NAME.grants enumera todo lo que concede el sistema, un hecho por línea: prioridades, presupuestos, memoria, dispositivos, interrupciones y canales. La compilación falla si ambos no coinciden, en cualquiera de los dos sentidos.

Cada dominio de protección tiene además un rol (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock o test), y la compilación rechaza una concesión que su rol nunca debe tener. A una interfaz de usuario no se le puede entregar un dispositivo de red por error, y un instrumento de prueba no puede colarse en un producto.

Mensajes tipados

Los dominios de protección se comunican mediante mensajes tipados: registros de tamaño fijo y versionados, con una disposición explícita, que circulan por anillos de un solo productor y un solo consumidor sobre memoria compartida.

• Copiar y después comprobar. El receptor copia cada registro fuera de la memoria compartida antes de validarlo, así que el emisor no puede cambiarlo entre la comprobación y su uso (el error conocido como doble lectura o double-fetch).
• Los decodificadores no pueden entrar en pánico. Cada decodificador devuelve un error tipado ante cualquier cosa mal formada, y tiene demostraciones acotadas de Kani y un objetivo de fuzzing.
• Cada lado tiene su propia vista. El productor y el consumidor ven el anillo a través de vistas de memoria separadas, y los índices compartidos usan ordenación acquire y release.

Entrada

Las aplicaciones ven eventos de entrada canónicos (teclas, movimientos del puntero y toques), comprobados contra la pantalla y con límite de frecuencia. Nunca ven USB ni ningún otro protocolo de dispositivo; la ruta de entrada los analiza en dominios de protección propios y trata cada byte como hostil.

Los fallos, el supervisor y el estado de fallo seguro

Cuando un dominio de protección hace algo que seL4 no permite, o entra en pánico, seL4 lo detiene y notifica un fallo a su padre.

• El supervisor es el padre de las demás partes. Recibe cada fallo, lo notifica y reinicia la placa para que el sistema vuelva a arrancar en limpio. Está construido y probado en sistemas de prueba de QEMU.
• El estado de fallo seguro es adonde va un dispositivo cuando los fallos se repiten: por defecto, al cuarto reinicio desde un arranque en frío, o al segundo fallo en una parte sensible para la seguridad, como el almacenamiento o las actualizaciones. Solo siguen funcionando el supervisor, el watchdog y, cuando es posible, la pantalla, y solo un arranque en frío, desde el equipo apagado, devuelve el dispositivo a la normalidad.
• El dominio de protección watchdog atiende al watchdog de hardware solo mientras todas las demás partes responden a su señal de vida. Si una deja de responder, el hardware reinicia la placa.

Memoria y tiempo

• La memoria se fija al construir la imagen. El código del dispositivo no reserva memoria: cada búfer y cada cola tienen un tamaño fijo, de nowayos-bounded. La única excepción, el cliente TLS, trabaja en una zona de memoria fija propia.
• Dos tipos de tiempo que nunca se mezclan. El tiempo monótono cuenta desde el arranque y nunca retrocede; todos los plazos de espera lo usan. La hora de reloj, la fecha y la hora del día, procede de una fuente autenticada. Son tipos de Rust distintos, así que no se puede pasar uno donde se espera el otro.

Construir sus propios sistemas

Los sistemas y dominios de protección de su producto viven en un repositorio propio, junto a nowayos, nunca dentro de él. El Makefile de ese repositorio define SYSTEM_REPO := $(CURDIR) e incluye los fragmentos de make de NoWayOS:

SYSTEM_REPO := $(CURDIR)
include ../nowayos/tools/make/container.mk
include ../nowayos/tools/make/system.mk

Así, make image, make qemu-test, make qemu-test-all y las comprobaciones funcionan sobre sus systems/ y pds/, con el contenedor de desarrollo, los archivos de placa, las reglas de concesión y las comprobaciones de NoWayOS. Las variables están documentadas al principio de tools/make/system.mk. El Showcase se construye exactamente así.