Seu primeiro sistema no QEMU

Um sistema NoWayOS é um conjunto de domínios de proteção, as partes de um dispositivo, inicializados juntos sobre o seL4. Todo sistema inicializa primeiro no QEMU, dentro do contêiner de desenvolvimento, e verifica a própria saída. Esta página inicializa o menor deles, e depois alguns que mostram mais.

Inicialize o hello

make qemu-test SYSTEM=hello

Isso compila o sistema hello, verifica as suas concessões, inicializa o seL4 em modo headless no QEMU e observa o que ele imprime. O teste passa quando todas as linhas que o sistema precisa imprimir aparecem, em ordem, e nada proibido aparece.

Para inicializá-lo você mesmo e acompanhar, rode make qemu SYSTEM=hello. Saia do QEMU com Ctrl-A e depois x.

Os três arquivos que definem um sistema

Cada sistema é formado por três arquivos em systems/, ao lado do código Rust em pds/.

hello.system é a descrição de sistema do Microkit: cada domínio de proteção, região de memória, canal e interrupção que o sistema tem. O hello tem um domínio de proteção e mais nada:

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

hello.grants lista tudo o que o sistema concede, um fato por linha. O build falha se a descrição conceder algo que não esteja listado aqui, ou se o arquivo listar algo que ela não concede, então uma mudança no que um sistema pode fazer fica sempre visível na revisão:

system demo
role hello app

pd hello priority=1 budget=1000 period=1000

hello.expect lista as linhas que o sistema precisa imprimir, em ordem, e, depois de um !, textos que reprovam o teste na hora, onde quer que apareçam:

NOWAYOS: rust pd starting
NOWAYOS: hello from rust

!MON|ERROR
!seL4(CPU
!panicked

O mesmo arquivo expect verifica o sistema num Raspberry Pi 5, a partir do log serial da placa.

O próprio domínio de proteção

pds/hello/src/main.rs é o programa inteiro. Ele segue a forma mínima do exemplo de Microkit do rust-sel4: init roda uma vez no início, e o handler receberia notificações se o sistema lhe desse algum 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;
}

Não há heap (qualquer alocação falharia na linkedição), nem unsafe, nem dispositivo. Imprimir só funciona porque este é um build de depuração: um kernel de release não tem console de depuração.

Veja o seL4 parar uma parte

make qemu-test SYSTEM=isolation-test

Dois domínios de proteção de sondagem tentam, cada um, algo que não lhes foi concedido: um lê memória que não está mapeada para ele, o outro escreve numa página que só pode ler. O seL4 para cada um com uma falha, e um terceiro domínio, só de espectador, continua rodando intacto. A última linha do teste diz isso:

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

Mais sistemas para experimentar

Rode qualquer um deles com make qemu-test SYSTEM=NAME, ou todos os sistemas com make qemu-test-all.

Clique pela interface de usuário

make qemu SYSTEM=ui-interactive VNC=1

A tela do QEMU é publicada via VNC em localhost:5900 na sua máquina, com uma senha impressa só para aquela execução. No macOS, abra vnc://localhost:5900 (no Finder: Ir, Conectar ao Servidor) e clique pelas telas da demo.

O que o build deixa ao lado de cada imagem

Em build/BOARD/SYSTEM/ (para estes, build/qemu_virt_aarch64/hello/ e assim por diante), ao lado de loader.img:

• sel4-config.txt: a configuração do seL4 da imagem, e se ela está dentro das provas do seL4. Um build de depuração diz claramente que não está. Veja Segurança.
• sbom.cdx.json: uma lista de materiais de software CycloneDX para a imagem: o kernel, o carregador, cada domínio de proteção e os crates dentro dele, cada um com o seu hash.
• Os arquivos de licença do que a imagem contém, como as licenças da fonte e dos ícones.