Segurança

Ele cuida da própria vida.

Um dispositivo NoWayOS deixa de fora o que a sua tarefa não exige e isola o que sobra em compartimentos. Esta página mostra em que isso se apoia, o que está provado, o que ainda não está e o que cabe a você acertar.

O que fica de fora

Uma imagem do NoWayOS contém a sua aplicação, os drivers que essa aplicação usa e o microkernel seL4. Não há motor de navegador, sistema de janelas, shell, gerenciador de pacotes nem conta de usuário: nada disso jamais foi embutido, então nada disso está lá para ser explorado, corrigido ou mal configurado. O NoWayOS é projetado para reduzir software e serviços desnecessários: se a tarefa não precisa, não está na imagem.

Esse é o significado do nome: não há como explorar o que nunca foi embutido. É uma afirmação sobre o que está ausente, não uma promessa de que nada pode dar errado. O que está embutido ainda pode ter bugs; as afirmações são que há muito menos disso, e que um bug fica no seu compartimento.

Travar um sistema de propósito geral é ser seguro por configuração: os recursos trancados continuam presentes, e um único bug pode contornar todas as configurações. O NoWayOS busca ser seguro por construção: os recursos nunca estiveram lá.

Como uma falha é contida

Cada parte roda no seu próprio domínio de proteção, com a sua própria memória, e detém apenas as capacidades que a descrição do sistema concede. O seL4 as impõe.
Cada concessão está listada no arquivo de concessões do sistema, e o build falha se a descrição conceder algo que o arquivo não lista, ou vice-versa. Ampliar uma concessão é revisado como uma mudança de segurança.
As mensagens entre as partes são registros de tamanho fixo, copiados para fora da memória compartilhada antes de serem verificados, então um remetente não consegue alterar um registro depois que ele foi aprovado.
Toda entrada é hostil até ser verificada. Todo parser de entrada externa passa por fuzzing e é construído para nunca entrar em pânico, e as aplicações recebem eventos de tecla, ponteiro e toque, nunca protocolos de dispositivo.
Um supervisor para uma parte que falha e reinicia o sistema do zero. Falhas repetidas colocam o dispositivo num estado de falha segura até uma inicialização a frio.

O que as provas do seL4 cobrem, e o que não cobrem

O seL4 é um microkernel de cerca de 10.000 linhas, com provas de correção e segurança verificadas por máquina. As provas são uma conquista rara, e valem para configurações específicas em plataformas específicas. Esta é a posição exata:

O NoWayOS roda sobre o microkernel seL4, que tem provas de correção e segurança verificadas por máquina para configurações específicas no nosso hardware; o NoWayOS usa a configuração de criticidade mista do seL4, cujas provas estão em andamento.

Plataforma: a configuração verificada do seL4 para AArch64 lista o Raspberry Pi 5 e os i.MX8M Mini, Plus e Quad da NXP.
Escalonamento: o Microkit compila o kernel de criticidade mista (MCS) do seL4, cujas provas para AArch64 estão em andamento. Por isso, hoje nenhuma imagem do NoWayOS está dentro das provas concluídas do seL4.
Núcleos: as provas valem para kernels de núcleo único. Uma imagem que usa vários núcleos fica fora delas, e diz isso.
Acima do kernel: as ferramentas do Microkit e os domínios de proteção e drivers do NoWayOS não são cobertos pelas provas do seL4. A garantia deles vem do Rust, do isolamento, da revisão, dos testes e das próprias provas limitadas do NoWayOS.

Cada imagem registra a sua configuração num sel4-config.txt ao lado dela. Veja o que o registro de um build de desenvolvimento do sistema hello diz sobre si mesmo:

system: hello
board: qemu_virt_aarch64
configuration: debug
sdk: Microkit 2.3.1
status: development build: a debug kernel, with printing and debug interfaces, outside seL4's proofs
status: outside seL4's completed proofs: a mixed-criticality (MCS) kernel, whose AArch64 proofs are in progress
status: outside seL4's proofs: a platform that is not on seL4's AArch64 verified list

Mesmo uma imagem cujo kernel correspondesse a todas as opções da configuração verificada não seria chamada de “verificada” aqui. O registro informa os fatos, e os fatos bastam.

As evidências, e o comando de cada uma

Cada afirmação desta página vem com a sua evidência, e cada evidência vem de um comando que qualquer pessoa pode executar no contêiner de desenvolvimento. make ci executa todos em ordem, e make ci CI_SCOPE=full executa todas as provas e todos os alvos de fuzzing; Verificações e evidências explica cada um.

A afirmação	A evidência	Execute
Cada concessão está registrada.	O arquivo de concessões de cada sistema, conferido com a descrição do sistema a cada build.	`make qemu-test SYSTEM=hello`
Uma parte não consegue alcançar o que não lhe foi concedido.	Testes de isolamento cujas sondas fazem leituras e escritas não concedidas, que o seL4 precisa barrar, e uma variante com uma concessão ampliada de propósito, que precisa falhar.	`make qemu-test SYSTEM=isolation-test`
Os decodificadores de mensagens se sustentam para toda entrada até um limite.	Provas Kani de cada decodificador de registros de mensagem, com testes de mutação que mostram que as provas podem falhar.	`make kani`
Os parsers de entrada externa sobrevivem a entradas hostis.	Um alvo de fuzzing para cada parser de entrada não confiável. Um travamento, depois de corrigido, vira um teste de regressão.	`make fuzz`
Código unsafe só existe onde foi aprovado.	Uma lista de permissões dos poucos crates e arquivos que podem usá-lo, imposta pelo make ci, com o Miri executado sobre esses crates.	`make unsafe-audit`
Cada componente é conhecido.	Uma lista de materiais de software CycloneDX para cada workspace e cada imagem de sistema, cada componente com o seu hash.	`make image-sbom SYSTEM=hello`
Licenças e alertas de segurança são verificados.	cargo-deny sobre cada workspace: licenças, origens, crates banidos e alertas conhecidos.	`make deny`
Não há segredos no código.	A árvore e cada commit varridos, offline, em busca de chaves e credenciais.	`make secrets`
A configuração do seL4 de cada imagem está registrada.	Um sel4-config.txt ao lado de cada imagem, e uma verificação de que os valores de referência do registro correspondem ao SDK do Microkit fixado.	`make sel4-config-check`

Leia as evidências de uma imagem

Você não precisa compilar nada para ver como são as evidências. Aqui estão todas elas, de uma imagem real: ui-interactive, a interface de usuário clicável, compilada para o QEMU em 1º de novembro de 2026.

Sua lista de materiais de software (CycloneDX 1.5): 62 partes, do kernel seL4 e do carregador do Microkit até cada crate de cada domínio de proteção, cada uma com o seu SHA-256.
Seu registro de configuração do seL4: o kernel que ela roda, opção por opção, comparado com a configuração verificada do seL4, e, com todas as letras, onde ela fica fora das provas.
Sua descrição de sistema: cada domínio de proteção, região de memória, interrupção e canal, do jeito que o Microkit os constrói.
Seu arquivo de concessões: as mesmas concessões registradas, um fato por linha, que o build confere com a descrição.
A tela que ela desenha, comparada pixel a pixel com esta imagem aprovada sempre que o seu teste roda.

O que continua sendo seu

O NoWayOS é uma plataforma, não um produto certificado. Um dispositivo seguro também depende de como ele é implantado e operado, e essa parte cabe a quem o constrói e o opera.

Segurança física. Um aparelho plugado nele ou uma mão no cabo de energia ainda podem tirar um dispositivo de operação. Gabinetes, portas e alimentação fazem parte do projeto do produto construído sobre o NoWayOS.
O que cada sistema concede. O NoWayOS verifica se um sistema e o seu arquivo de concessões estão de acordo. Se essas concessões são as certas para a tarefa é uma decisão de projeto, e deve ser revisada como tal.
Redes e back-ends. Um dispositivo só se conecta aos destinos que o seu sistema permite. Proteger o que esses serviços fazem com o que recebem cabe a eles.
Chaves e atualizações. Atualizações assinadas com reversão segura estão projetadas, mas ainda não construídas. Quem guarda as chaves de assinatura, e como uma versão é aprovada, é uma decisão de operação.
Certificação. Produtos regulados que rodam sobre o NoWayOS têm a sua própria certificação. O NoWayOS é projetado para fornecer as evidências de que eles precisam; ele mesmo não é certificado.

Ainda não construído

Inicialização segura e atestação dependem de hardware de produção com uma raiz de confiança em hardware. Nenhuma das duas está construída.
Atualizações assinadas aplicadas no dispositivo. Os registros de atualização e as suas verificações existem; o caminho que aplica uma atualização num dispositivo ainda não.
O Raspberry Pi 5 é uma placa de desenvolvimento, não um dispositivo reforçado. Quem tem uma em mãos pode trocar o software dela, e o acesso à memória por dispositivos USB ainda não está confinado nela.

Palavras que você não vai encontrar aqui

Não chamamos o NoWayOS de “inhackeável”, “à prova de adulteração” ou “à prova de balas”, nem dizemos que ele tem “superfície de ataque zero”. Nada é assim, e você teria toda razão em parar de ler. As afirmações desta página são menores que isso, e cada uma vem com a sua evidência.

Como relatar uma vulnerabilidade

Por favor, relate uma vulnerabilidade de forma privada, pelo relato privado de vulnerabilidades do GitHub na aba Security do repositório ou por e-mail para security@nowayos.com, como descreve o SECURITY.md de cada repositório, e não numa issue pública. Como cada parte roda no seu próprio compartimento, tudo é projetado para que uma brecha fique onde está enquanto a correção é feita.