Como um sistema se encaixa

Todo dispositivo NoWayOS é um sistema: um conjunto fixo de partes, declarado antes do build, cada uma isolada das outras pelo seL4. Nada é acrescentado em tempo de execução. Esta página explica as peças e como elas se conectam.

Domínios de proteção

Um domínio de proteção é uma parte de um sistema: um programa com memória própria, que detém apenas as capacidades que lhe são concedidas. No seL4, uma capacidade é um token infalsificável que nomeia um objeto do kernel e os direitos que se tem sobre ele, como um cartão de acesso para uma única porta. Um domínio de proteção não consegue tocar em nada que as suas capacidades não nomeiem, e o seL4 impõe isso.

Um sistema típico tem um domínio de proteção para cada responsabilidade: um driver de tela, o caminho de entrada, a pilha de rede, a interface de usuário, a aplicação, um temporizador, um supervisor e um watchdog. Cada um é um pequeno programa Rust, no_std, que não aloca nada depois de iniciar.

A descrição do sistema

A descrição de sistema do Microkit (systems/NAME.system, um arquivo XML) declara o sistema inteiro: cada domínio de proteção com a sua prioridade, orçamento e pilha; cada região de memória e quem a mapeia; cada canal; cada interrupção.

• As descrições nomeiam dispositivos, nunca endereços: phys_addr="@NAME". Os endereços vêm do arquivo da placa em platforms/, cada um com a sua fonte, então a mesma descrição compila para o QEMU e para o Raspberry Pi 5.
• Canais conectam dois domínios de proteção, para notificações (sinais sem dados, entre eles as interrupções) e chamadas de procedimento protegidas (chamadas síncronas para uma parte de prioridade mais alta).

A descrição é o projeto de segurança do sistema, então uma mudança nela é revisada como uma mudança de segurança.

O arquivo de concessões

Ao lado de cada descrição, systems/NAME.grants lista tudo o que o sistema concede, um fato por linha: prioridades, orçamentos, memória, dispositivos, interrupções e canais. O build falha se os dois discordarem, em qualquer direção.

Cada domínio de proteção também tem um papel (ui, input, broker, display, driver, network, security, storage, update, app, supervisor, watchdog, clock ou test), e o build recusa uma concessão que esse papel nunca deve ter. Uma interface de usuário não pode receber um dispositivo de rede por engano, e um instrumento de teste não consegue entrar escondido num produto.

Mensagens tipadas

Os domínios de proteção se comunicam por mensagens tipadas: registros de tamanho fixo e versionados, com layout explícito, passados em anéis de produtor único e consumidor único sobre memória compartilhada.

• Copiar, depois verificar. O receptor copia cada registro para fora da memória compartilhada antes de validá-lo, então o remetente não consegue alterá-lo entre a verificação e o uso (o bug chamado double-fetch).
• Os decodificadores não podem entrar em pânico. Cada decodificador retorna um erro tipado para qualquer coisa malformada, e tem provas limitadas com Kani e um alvo de fuzzing.
• Cada lado tem a sua própria visão. O produtor e o consumidor enxergam o anel por mapeamentos de memória separados, e os índices compartilhados usam ordenação acquire e release.

Entrada

As aplicações recebem eventos de entrada canônicos (teclas, movimentos de ponteiro e toques), verificados em relação à tela e com limite de taxa. Elas nunca veem USB ou qualquer outro protocolo de dispositivo; o caminho de entrada interpreta esses protocolos em domínios de proteção próprios, tratando cada byte como hostil.

Falhas, o supervisor e o estado de falha segura

Quando um domínio de proteção faz algo que o seL4 não permite, ou entra em pânico, o seL4 o para e informa uma falha ao seu pai.

• O supervisor é o pai das outras partes. Ele recebe cada falha, a relata e reinicia a placa para que o sistema recomece do zero. Ele é construído e testado em sistemas de teste no QEMU.
• O estado de falha segura é para onde um dispositivo vai quando as falhas não param: por padrão, no quarto reinício desde uma inicialização a frio, ou na segunda falha numa parte sensível para a segurança, como o armazenamento ou as atualizações. Só o supervisor, o watchdog e, quando possível, a tela continuam rodando, e só uma inicialização a frio, a partir do equipamento desligado, traz o dispositivo de volta.
• O domínio de proteção watchdog alimenta o watchdog de hardware só enquanto todas as outras partes respondem ao seu sinal de vida. Se uma delas parar de responder, o hardware reinicia a placa.

Memória e tempo

• A memória é fixada quando a imagem é compilada. O código do dispositivo não aloca nada: cada buffer e cada fila têm um tamanho definido, de nowayos-bounded. A única exceção, o cliente TLS, trabalha numa arena fixa própria.
• Dois tipos de tempo que nunca se misturam. O tempo monotônico conta a partir da inicialização e nunca volta para trás; todo timeout o usa. O tempo de relógio de parede, a data e a hora do dia, vem de uma fonte autenticada. São tipos Rust diferentes, então um não pode ser passado onde o outro é esperado.

Como criar os seus próprios sistemas

Os sistemas e os domínios de proteção do seu produto ficam num repositório próprio, ao lado de nowayos, nunca dentro dele. O Makefile desse repositório define SYSTEM_REPO := $(CURDIR) e inclui os fragmentos de make do NoWayOS:

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

Depois disso, make image, make qemu-test, make qemu-test-all e as verificações funcionam sobre os systems/ e pds/ dele, com o contêiner de desenvolvimento, os arquivos de placa, as regras de concessão e as verificações do NoWayOS. As variáveis estão documentadas no topo de tools/make/system.mk. O Showcase é construído exatamente assim.