As palavras, em bom português.

systems/NAME.grants: tudo o que um sistema concede, um fato por linha: prioridades, orçamentos, memória, dispositivos, interrupções e canais. O build falha se a descrição do sistema e o arquivo de concessões discordarem.

systems/NAME.expect: as linhas que um sistema precisa imprimir, em ordem, e o texto que reprova o teste se aparecer em qualquer lugar. O mesmo arquivo verifica um sistema no QEMU e no Raspberry Pi 5.

Um dispositivo provando a um serviço remoto, por criptografia, qual software ele iniciou. Ela mostra o que foi carregado na inicialização, não tudo o que aconteceu desde então. Planejada para o NoWayOS em hardware de produção; ainda não construída.

Uma fonte desenhada com antecedência, em tempo de build, em imagens dos seus caracteres, para que um dispositivo desenhe texto sem nunca interpretar um arquivo de fonte.

Tudo aquilo de cuja correção uma propriedade de segurança depende. Num sistema NoWayOS: o kernel seL4, o carregador e o monitor do Microkit, e os domínios de proteção dos quais essa propriedade depende.

Um erro como ler além do fim de um buffer ou usar memória depois de ela ter sido liberada. A Microsoft e o Google relataram, cada um, que cerca de 70% dos seus bugs de segurança graves são desse tipo; o código Rust seguro (safe) os exclui.

No Microkit, uma conexão declarada entre dois domínios de proteção, para notificações (sinais sem dados, entre eles as interrupções) e chamadas de procedimento protegidas.

No seL4, 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 só pode tocar no que as suas capacidades nomeiam.

A imagem de contêiner com versões fixadas que contém todo o conjunto de ferramentas do NoWayOS: os toolchains de Rust, o SDK do Microkit, o QEMU e as ferramentas de verificação. Todo alvo do make roda nela, então a sua máquina só precisa de Podman e make (e de Python 3.11 para controlar um Raspberry Pi 5).

A regra de que uma mensagem é copiada para fora da memória compartilhada antes de ser validada, para que o remetente não consiga alterá-la entre a verificação e o uso. Ela impede um double-fetch.

Um formato padrão aberto para listas de materiais de software. O NoWayOS gera uma para cada workspace e cada imagem de sistema. Veja SBOM.

O adaptador USB-serial do Raspberry Pi. No conector de depuração do Raspberry Pi 5, ele transporta o log de boot e carrega imagens de teste.

O arquivo XML do Microkit que declara cada domínio de proteção, região de memória, canal e interrupção de um sistema. Ela é o projeto de segurança do sistema, e uma mudança nela é revisada como tal.

Uma parte isolada de um sistema Microkit: um programa com memória própria, que detém apenas as capacidades que lhe são explicitamente concedidas. Os compartimentos estanques do NoWayOS.

Um bug em que o código verifica dados na memória compartilhada e depois os lê de novo, permitindo que o outro lado os altere no meio do caminho. Evitado por copiar, depois verificar.

Uma biblioteca de gráficos 2D em Rust para dispositivos sem pilha gráfica de sistema operacional. A interface de usuário do NoWayOS desenha com ela.

Para onde um dispositivo NoWayOS vai quando as falhas não param: só o supervisor, o watchdog e, quando possível, a tela continuam rodando, até uma inicialização a frio.

O que o seL4 informa quando um domínio de proteção faz algo que o kernel não permite, ou entra em pânico. A parte fica parada até que o seu tratador de falhas aja.

Testar um parser com milhões de entradas geradas até que uma delas o derrube ou quebre uma verificação. Todo parser de entrada externa do NoWayOS tem um alvo de fuzzing.

A família de processadores Arm industriais da NXP, e o hardware de produção pretendido do NoWayOS. Ainda não suportada.

Uma inicialização a partir do equipamento desligado, ao contrário de um reset. Só uma inicialização a frio traz um dispositivo NoWayOS de volta do seu estado de falha segura.

Um dispositivo que se recusa a iniciar software não assinado pelo seu fabricante. Planejada para o NoWayOS em hardware de produção; ainda não construída.

Um verificador de modelos para Rust que prova propriedades para toda entrada até um limite. O NoWayOS o usa para provar que os seus decodificadores de mensagens nunca entram em pânico, nunca estouram e nunca leem fora dos limites.

A configuração do seL4 com orçamentos e períodos de escalonamento, que o Microkit compila. Suas provas para AArch64 estão em andamento, então hoje nenhuma imagem do NoWayOS está dentro das provas concluídas do seL4.

Um registro de tamanho fixo com layout explícito, passado entre domínios de proteção por memória compartilhada e verificado no recebimento. Veja copiar, depois verificar.

Um kernel mantido o menor possível, com drivers, rede e tela rodando fora dele, cada um no seu próprio compartimento. O seL4 é um deles.

O framework da seL4 Foundation para sistemas seL4 estáticos, construídos a partir de domínios de proteção declarados numa descrição do sistema.

Um interpretador para Rust que detecta comportamento indefinido. O NoWayOS o executa sobre os poucos crates autorizados a usar código unsafe.

Uma prova de que uma propriedade vale para toda entrada até um tamanho declarado. O NoWayOS prova assim os seus decodificadores de mensagens, com o Kani.

Um emulador de máquinas de código aberto. Todo sistema NoWayOS inicializa nele, e verifica a própria saída, antes de tocar em hardware.

A placa de baixo custo que o NoWayOS usa como hardware de referência.

Uma linguagem de programação cujo código seguro (safe) exclui os bugs de segurança de memória. O código do próprio NoWayOS é Rust de ponta a ponta.

O suporte a Rust da seL4 Foundation, incluindo o crate para escrever domínios de proteção do Microkit.

Uma biblioteca TLS escrita em Rust. O cliente TLS 1.3 do NoWayOS é construído sobre ela, com RustCrypto.

Uma lista de materiais de software (software bill of materials): a relação de cada componente e versão que compõe um software. O NoWayOS gera uma em CycloneDX para cada workspace e cada imagem de sistema.

A ferramenta de build do NoWayOS que converte telas React, escritas em TSX dentro de um subconjunto suportado, em Rust para a interface de usuário do NoWayOS. Ela recusa tudo o que estiver fora do subconjunto em vez de fazer uma aproximação.

O seL4 Device Driver Framework: um projeto de referência para drivers no Microkit, que usa filas em memória compartilhada. As filas de rede do NoWayOS seguem esse modelo.

Tornar um dispositivo de propósito geral mais seguro mudando as suas configurações. Os recursos continuam lá, e um único bug pode contornar todas as configurações.

Construir um dispositivo que não consegue fazer as coisas arriscadas porque elas nunca foram embutidas nele. A abordagem do NoWayOS.

Um microkernel de cerca de 10.000 linhas, mantido pela seL4 Foundation, com provas de correção e segurança verificadas por máquina para configurações específicas. O NoWayOS roda sobre ele.

O registro gravado ao lado de cada imagem do NoWayOS: a sua configuração do seL4, e se essa configuração está dentro das provas concluídas do seL4.

Um sistema operacional feito para a única tarefa de um dispositivo, em vez de ser feito para rodar qualquer coisa e depois travado numa só. Três características o definem: ele é feito para uma só tarefa (a sua imagem contém a aplicação, os drivers que ela usa e o kernel, e nada mais); é isolado por dentro (cada parte num compartimento próprio, alcançando só o que lhe foi concedido); e abre o jogo (as evidências do que há dentro vêm com ele). Não é modo quiosque, que trava um sistema seguro por configuração num único app. O NoWayOS é um Single Purpose OS: um computador sem mais nada para fazer.

Uma pilha TCP/IP em Rust que não aloca memória durante a execução. A pilha de rede do NoWayOS é construída sobre ela.

Tudo o que um atacante poderia tentar usar contra um dispositivo: o seu código, serviços, interfaces e entradas. Menos código e menos recursos deixam menos superfície.

O domínio de proteção que recebe as falhas das outras partes, as relata e reinicia o sistema do zero.

A data e a hora do dia, de uma fonte autenticada. O NoWayOS o mantém separado do tempo monotônico, como um tipo diferente.

Tempo contado a partir da inicialização, que nunca é ajustado e nunca volta para trás. Todo timeout do NoWayOS o usa, e ele nunca se mistura com o tempo de relógio de parede.

Um sistema que tenta alcançar o que não lhe foi concedido, o que o seL4 precisa barrar. Uma variante com uma concessão ampliada de propósito precisa falhar, o que mostra que o teste é capaz de falhar.

Código Rust cuja segurança de memória o compilador não consegue verificar. Proibido em todo crate do NoWayOS, exceto numa lista curta e revisada que as verificações impõem.

Prova matemática, verificada por computador, de que um software atende à sua especificação. O seL4 tem essa prova para configurações específicas. O código do próprio NoWayOS se apoia, em vez disso, em Rust, isolamento, testes e provas limitadas.

Um temporizador de hardware que reinicia a placa a menos que o software o alimente. O domínio de proteção watchdog do NoWayOS só o alimenta enquanto todas as outras partes respondem ao seu sinal de vida.