Su primer sistema en QEMU

Arranque seL4 en QEMU con un dominio de protección en Rust, lea los tres archivos que definen un sistema, vea cómo seL4 detiene una parte que va demasiado lejos y recorra la interfaz de usuario con el ratón.

Un sistema NoWayOS es un conjunto de dominios de protección, las partes de un dispositivo, que arrancan juntos sobre seL4. Cada sistema arranca primero en QEMU, dentro del contenedor de desarrollo, y comprueba su propia salida. Esta página arranca el más pequeño y después algunos que muestran más.

Arranque hello

make qemu-test SYSTEM=hello

Esto compila el sistema hello, comprueba sus concesiones, arranca seL4 sin pantalla en QEMU y vigila lo que imprime. La prueba se supera cuando ha aparecido, en orden, cada línea que el sistema debe imprimir, y no ha aparecido nada prohibido.

Para arrancarlo usted mismo y observarlo, ejecute make qemu SYSTEM=hello. Salga de QEMU con Ctrl-A y después x.

Los tres archivos que definen un sistema

Cada sistema son tres archivos en systems/, junto al código Rust de pds/.

hello.system es la descripción de sistema de Microkit: cada dominio de protección, región de memoria, canal e interrupción que tiene el sistema. hello tiene un dominio de protección y nada más:

<system>
 <protection_domain name="hello" priority="1" stack_size="0x10000">
 <program_image path="nowayos-hello.elf" />
 </protection_domain>
</system>

hello.grants enumera todo lo que concede el sistema, un hecho por línea. La compilación falla si la descripción concede algo que no figura aquí, o si aquí figura algo que no concede, así que un cambio en lo que un sistema puede hacer siempre es visible en la revisión:

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect enumera las líneas que el sistema debe imprimir, en orden, y, tras un !, el texto que hace fallar la prueba en el acto dondequiera que aparezca:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

El mismo archivo de salida esperada comprueba el sistema en una Raspberry Pi 5, a partir del registro serie de la placa.

El dominio de protección en sí

pds/hello/src/main.rs es el programa completo. Sigue la forma mínima del ejemplo de Microkit de rust-sel4: init se ejecuta una vez al inicio, y el gestor recibiría notificaciones si el sistema le diera algún canal.

#![no_std]
#![no_main]

use sel4_microkit::{Handler, Infallible, debug_println, protection_domain};

#[protection_domain]
fn init() -> HelloPd {
 debug_println!("NOWAYOS: rust pd starting");
 debug_println!("NOWAYOS: hello from rust");
 HelloPd
}

struct HelloPd;

impl Handler for HelloPd {
 type Error = Infallible;
}

No hay heap (cualquier reserva de memoria fallaría al enlazar), ni unsafe, ni dispositivo. La impresión solo funciona porque es una compilación de depuración: un núcleo de versión final no tiene consola de depuración.

Vea cómo seL4 detiene una parte

make qemu-test SYSTEM=isolation-test

Dos dominios de protección sonda intentan cada uno algo que no se les ha concedido: uno lee memoria que no tiene mapeada y el otro escribe en una página que solo puede leer. seL4 detiene a cada uno con un fallo, y un tercero que solo observa sigue funcionando intacto. La última línea de la prueba lo dice:

NOWAYOS: isolation-test: 2 of 2 forbidden accesses faulted and were contained; bystander still running

Más sistemas para probar

Sistema	Lo que muestra
`ipc-demo`	Dos dominios de protección intercambian registros tipados a través de un anillo compartido; un registro mal formado se rechaza
`timer-demo`	El dominio de protección del temporizador atiende a dos clientes y entrega sus plazos en orden de vencimiento
`supervisor-test`	El supervisor recibe un fallo y reinicia la placa, y el siguiente arranque encuentra su memoria limpia
`ui-demo`	La sesión guionizada de la interfaz de usuario, con un hash de cada fotograma comprobado

Ejecute cualquiera de ellos con make qemu-test SYSTEM=NAME, o todos los sistemas con make qemu-test-all.

Recorra la interfaz de usuario

make qemu SYSTEM=ui-interactive VNC=1

La pantalla de QEMU se publica por VNC en localhost:5900 de su máquina, con una contraseña que se imprime solo para esa ejecución. En macOS, abra vnc://localhost:5900 (en el Finder: Ir, Conectarse al servidor) y recorra las pantallas de la demo haciendo clic.

Lo que deja la compilación junto a cada imagen

En build/BOARD/SYSTEM/ (para estos, build/qemu_virt_aarch64/hello/ y así sucesivamente), al lado de loader.img:

sel4-config.txt: la configuración de seL4 de la imagen, y si está dentro de las demostraciones de seL4. Una compilación de depuración dice claramente que no lo está. Consulte Seguridad.
sbom.cdx.json: una lista de materiales de software CycloneDX para la imagen: el núcleo, el cargador, cada dominio de protección y los crates que contiene, cada uno con su hash.
Los archivos de licencia de lo que contiene la imagen, como las licencias de la fuente y de los iconos.