Comprobaciones y evidencias

Qué ejecuta make ci y qué muestra cada comprobación, las reglas básicas que cumple cada crate, cómo leer el registro de seL4 y la lista de materiales de una imagen, y cómo se mantiene rápido el control.

NoWayOS hace pocas afirmaciones, y respalda cada una con una comprobación que usted puede ejecutar. Esta página explica qué muestra cada comprobación, y qué no.

Un solo comando para todo

make ci

make ci es el control completo, ejecutado en orden: el análisis de secretos, los lints, las pruebas, la documentación, la demo, la compilación no_std, las comprobaciones de licencias y de avisos de seguridad, los atlas de glifos, las listas de materiales, el fuzzing y las demostraciones de Kani, y después las comprobaciones de sistema y los arranques en QEMU. Un cambio solo se supera si se supera cada paso.

Qué muestra cada comprobación

Comando	Lo que muestra
`make test`	Pruebas unitarias, de propiedades, de documentación y de imágenes de referencia: el código hace lo que dicen sus pruebas, y cada pantalla se dibuja exactamente como se aprobó
`make lint`	rustfmt y clippy, con las advertencias tratadas como errores
`make nostd`	Cada crate de dispositivo se compila para bare metal (`aarch64-unknown-none`), sin biblioteca estándar
`make deny`	La base que debe mantener cada espacio de trabajo y, después, cargo-deny: licencias, orígenes, crates prohibidos y avisos de seguridad conocidos
`make secrets`	El árbol y cada commit, analizados sin conexión en busca de claves y credenciales
`make fuzz`	Cada objetivo de fuzzing, compilado con libFuzzer y ejecutado contra entradas generadas durante `FUZZ_SECONDS` (10 s) cada uno
`make kani`	Las demostraciones acotadas de Kani: que cada decodificador de registros nunca entra en pánico, se desborda ni lee fuera de límites para ninguna entrada hasta el registro más largo, con pruebas de mutación que muestran que cada demostración puede fallar
`make unsafe-audit`	El código `unsafe` solo aparece donde lo permite la lista aprobada
`make pds-miri`	Miri ejecuta las pruebas de los crates a los que se permite `unsafe`, en busca de comportamiento indefinido
`make sbom`	Una lista de materiales CycloneDX para cada espacio de trabajo
`make image-sbom SYSTEM=NAME`	Una imagen y su lista de materiales: núcleo, cargador, monitor y cada dominio de protección, con los crates de cada uno y sus hashes
`make sel4-config-check`	La posición de verificación de seL4 que consta en el registro es la del SDK de Microkit fijado
`make qemu-test-all`	Cada sistema arranca en QEMU, en cada configuración que enumera, e imprime lo que dice su archivo de salida esperada

Las demostraciones acotadas son demostraciones hasta un tamaño de entrada indicado, no para todas las entradas posibles. El fuzzing encuentra fallos; no puede demostrar que no los haya. Las pruebas muestran los casos que prueban. Cada una vale la pena por lo que sí muestra.

Las reglas básicas que cumple cada crate

Son lints y comprobaciones en cada espacio de trabajo, no recomendaciones:

Nada de unsafe, salvo en una lista breve y aprobada de crates y archivos que acceden directamente al hardware o a la memoria. Añadir algo a la lista requiere un motivo explícito y una revisión.
Nada de pánicos ante entradas externas: nada de unwrap, expect ni panic! en el código de biblioteca, nada de indexación ni aritmética sin comprobar, y cada excepción a un lint da su motivo.
Los crates de dispositivo son no_std y no reservan memoria. Las compilaciones de versión final conservan las comprobaciones de desbordamiento, y un pánico detiene la parte en lugar de seguir adelante.
Los analizadores rechazan la entrada sobredimensionada antes de copiarla, devuelven errores tipados y tienen pruebas de propiedades y un objetivo de fuzzing.
Ningún secreto en ninguna parte, ni siquiera claves de desarrollo. Las claves de prueba se generan cuando se ejecuta una prueba, y nunca se almacenan.

Cómo leer los registros de una imagen

Cada imagen se escribe en build/BOARD/SYSTEM/ con dos registros a su lado.

sel4-config.txt nombra la imagen, su hash, la placa, el SDK de Microkit y el núcleo, y después indica dónde se sitúa la imagen respecto a las demostraciones de seL4, con una línea status: por motivo, y enumera cada opción del núcleo que lo determina junto al valor de la configuración verificada. Un núcleo de depuración es una compilación de desarrollo. Un núcleo multiprocesador o de criticidad mixta, o una placa que no está en la lista de seL4, queda fuera de las demostraciones de seL4. Un núcleo que coincide con todas las opciones tampoco se llama nunca “verificado”: el registro da los hechos y ahí lo deja.

sbom.cdx.json es la lista de materiales de software CycloneDX de la imagen: de qué está hecha, hasta cada crate de cada dominio de protección, cada uno con su sha256.

Cómo se mantiene rápido el control

El conjunto completo de demostraciones y fuzzing lleva mucho tiempo, así que el make ci de cada día ejecuta Kani, el fuzzing y Miri solo donde llega un cambio. Sigue el cambio a través de cada crate que depende de él y omite cualquier comprobación cuyas entradas no hayan cambiado desde la última vez que se superó. make ci CI_SCOPE=full las ejecuta todas, sin nada en caché; make kani, make fuzz y make pds-miri siempre se ejecutan completos.

Kani es el paso más voraz: cada trabajo de demostración recibe unos 10 GB de memoria, y KANI_JOBS fija cuántos se ejecutan a la vez. Si make kani se queda sin memoria, asigne más a la máquina virtual de Podman, o establezca KANI_JOBS=1.