Construído a partir da tarefa.

Da aplicação à imagem

Um dispositivo NoWayOS é construído, não configurado. Quatro passos levam o seu código a um dispositivo que cumpre a sua única tarefa, e cada passo deixa algo que você pode verificar.

Compartimentos estanques

Cada parte de um sistema NoWayOS (a tela, a entrada, a rede, a sua aplicação) roda num domínio de proteção próprio sobre o microkernel seL4. Um domínio de proteção tem a sua própria memória e detém apenas as capacidades que a descrição do sistema lhe concede: uma capacidade funciona como um cartão de acesso para uma única porta. O seL4 as impõe, então uma parte só alcança o que recebeu, e tudo é projetado para que um bug numa parte fique nessa parte.

• Um supervisor recebe as falhas das outras partes, para a parte que falhou e reinicia o sistema do zero. Quando as falhas não param de chegar, o dispositivo entra num estado de falha segura, e só uma inicialização a frio o traz de volta.
• Um domínio de proteção watchdog alimenta o watchdog de hardware só enquanto todas as outras partes respondem ao seu sinal de vida.
• Papéis limitam o que cada parte pode receber: o build recusa uma concessão que o papel de uma parte nunca deve ter, como um dispositivo para uma parte que só deveria desenhar.

Mensagens tipadas, copiadas antes de ser verificadas

Os domínios de proteção se comunicam por registros de tamanho fixo e versionados, com layout explícito, passados em anéis de produtor único sobre memória compartilhada. Cada registro é copiado para fora da memória compartilhada antes de ser verificado, então o remetente não consegue alterá-lo entre a verificação e o uso.

Todo parser de entrada externa passa por fuzzing e é construído para nunca entrar em pânico, e todo decodificador de mensagens tem provas limitadas, feitas com o verificador de modelos Kani.

Uma tela nativa, e nenhum navegador

A interface de usuário é um pequeno núcleo declarativo: layout, foco e hit-testing em memória limitada, desenhados com a biblioteca Rust embedded-graphics, redesenhando só o que mudou. O texto vem de atlas de glifos desenhados com antecedência, em tempo de build, então o dispositivo nunca interpreta um arquivo de fonte. As aplicações recebem eventos de tecla, ponteiro e toque, nunca USB ou qualquer outro protocolo de dispositivo.

Os designers podem continuar trabalhando em React. O Screen Compiler converte em Rust, em tempo de build, as telas escritas dentro do subconjunto que ele suporta, e recusa qualquer coisa fora desse subconjunto em vez de aproximá-la.

O que vem dentro

Hardware

O NoWayOS é desenvolvido em máquinas Apple silicon (arm64). Em x86-64, os pacotes da imagem de desenvolvimento também são fixados e revisados, mas a imagem ainda não foi compilada e testada de ponta a ponta nessa arquitetura.

Construído sobre

O NoWayOS se apoia no trabalho de outras pessoas, e diz isso: seL4, Microkit, rust-sel4, as filas de rede do seL4 Device Driver Framework, smoltcp, rustls, RustCrypto e embedded-graphics.