Verificações e evidências

O que o make ci executa e o que cada verificação mostra, as regras básicas que todo crate segue, como ler o registro do seL4 e a lista de materiais de uma imagem, e como a bateria de verificações continua rápida.

O NoWayOS faz poucas afirmações, e sustenta cada uma delas com uma verificação que você pode executar. Esta página explica o que cada verificação mostra, e o que ela não mostra.

Um comando para tudo

make ci

make ci é a bateria completa, executada em ordem: a varredura de segredos, lints, testes, documentação, a demo, o build no_std, as verificações de licenças e de alertas de segurança, os atlas de glifos, as listas de materiais, fuzzing e as provas Kani, depois as verificações de sistema e as inicializações no QEMU. Uma mudança só passa se todas as etapas passarem.

O que cada verificação mostra

Comando	O que ele mostra
`make test`	Testes unitários, de propriedade, de documentação e de imagem de referência: o código faz o que os seus testes dizem, e cada tela é desenhada exatamente como foi aprovada
`make lint`	rustfmt e clippy, com avisos tratados como erros
`make nostd`	Todo crate de dispositivo compila para bare metal (`aarch64-unknown-none`), sem biblioteca padrão
`make deny`	A linha de base que todo workspace precisa manter, depois o cargo-deny: licenças, origens, crates banidos e alertas conhecidos
`make secrets`	A árvore e cada commit, varridos offline em busca de chaves e credenciais
`make fuzz`	Todos os alvos de fuzzing, compilados com libFuzzer e executados contra entradas geradas, por `FUZZ_SECONDS` (10 s) cada
`make kani`	As provas limitadas do Kani: que cada decodificador de registros nunca entra em pânico, nunca estoura e nunca lê fora dos limites para qualquer entrada até o registro mais longo, com testes de mutação que mostram que cada prova pode falhar
`make unsafe-audit`	Código `unsafe` só aparece onde a lista aprovada permite
`make pds-miri`	O Miri executa os testes dos crates autorizados a usar `unsafe`, procurando comportamento indefinido
`make sbom`	Uma lista de materiais CycloneDX para cada workspace
`make image-sbom SYSTEM=NAME`	Uma imagem e a sua lista de materiais: kernel, carregador, monitor e cada domínio de proteção, com os crates de cada um e os seus hashes
`make sel4-config-check`	A posição de verificação do seL4 que está registrada é a do SDK do Microkit fixado
`make qemu-test-all`	Todo sistema inicializa no QEMU, em cada configuração que lista, e imprime o que o seu arquivo expect diz

Provas limitadas são provas até um tamanho de entrada declarado, não para toda entrada que possa existir. O fuzzing encontra travamentos; ele não consegue mostrar que não há nenhum. Os testes mostram os casos que testam. Cada um vale pelo que de fato mostra.

As regras básicas que todo crate segue

Estas são lints e verificações em todo workspace, não recomendações:

Nada de unsafe, exceto numa lista curta e aprovada de crates e arquivos que acessam o hardware ou a memória diretamente. Acrescentar algo à lista exige uma justificativa declarada e revisão.
Nada de pânico com entrada externa: nada de unwrap, expect ou panic! em código de biblioteca, nada de indexação ou aritmética sem verificação, e toda exceção a uma lint traz a sua justificativa.
Crates de dispositivo são no_std e não alocam nada. Builds de release mantêm as verificações de overflow, e um pânico para a parte em vez de seguir em frente.
Parsers recusam entradas grandes demais antes de copiá-las, retornam erros tipados e têm testes de propriedade e um alvo de fuzzing.
Nenhum segredo em lugar nenhum, nem mesmo chaves de desenvolvimento. Chaves de teste são criadas quando um teste roda, e nunca armazenadas.

Como ler os registros de uma imagem

Toda imagem é gravada em build/BOARD/SYSTEM/ com dois registros ao lado.

sel4-config.txt nomeia a imagem, o seu hash, a placa, o SDK do Microkit e o kernel, depois diz onde a imagem se situa em relação às provas do seL4, com uma linha status: por motivo, e lista cada opção do kernel que decide isso ao lado do valor da configuração verificada. Um kernel de depuração é um build de desenvolvimento. Um kernel multinúcleo ou de criticidade mista, ou uma placa fora da lista do seL4, fica fora das provas do seL4. Um kernel que corresponda a todas as opções ainda assim nunca é chamado de “verificado”: o registro dá os fatos e para por aí.

sbom.cdx.json é a lista de materiais de software CycloneDX da imagem: do que ela é feita, até cada crate de cada domínio de proteção, cada um com o seu sha256.

Como a bateria continua rápida

O conjunto completo de provas e de fuzzing leva muito tempo, então o make ci do dia a dia executa Kani, fuzzing e Miri só onde uma mudança chega. Ele acompanha a mudança por todos os crates que dependem dela, e pula qualquer verificação cujas entradas não mudaram desde a última vez que ela passou. make ci CI_SCOPE=full executa todas elas, sem nada em cache; make kani, make fuzz e make pds-miri sempre rodam completos.

O Kani é a etapa mais faminta: cada job de prova recebe cerca de 10 GB de memória, e KANI_JOBS define quantos rodam ao mesmo tempo. Se o make kani ficar sem memória, dê mais memória à máquina virtual do Podman, ou defina KANI_JOBS=1.