O seL4 completa provas formais de segurança em ARM 64 bits

A Proofcraft anunciou em 21 de agosto de 2026 que as provas de segurança do microkernel seL4 estão completas na arquitetura AArch64, a variante de 64 bits do ARM. Com isso, existe agora uma prova matemática formal de que o kernel impede que uma aplicação rodando sobre o seL4 obtenha informação sem autorização, propriedade conhecida como confidencialidade.

Esse era o último bloco que faltava. As provas de correção funcional e de integridade (que o kernel impede que uma aplicação modifique dados sem autorização) já haviam sido concluídas para AArch64. Fechar a confidencialidade completa o stack inteiro de provas de segurança para a arquitetura ARM de 64 bits. O trabalho contou com apoio continuado do NCSC, a agência britânica de cibersegurança↳Segurança171 conteúdosCibersegurança no Brasil: 6 passos para sair da estagnaçãoDevSecOps · jul 2025O papel do CISO para transformar a cibersegurança em uma alavanca de reputação para as empresasDevSecOps · mar 2024Itaipu Parquetec e Exército Brasileiro realizam exercício de cibersegurança em BrasíliaDev (Back & Front) · set 2025Ver tudo em DevSecOps →.

O que significa "prova formal" aqui

O seL4 não é um kernel comum. Ele é o primeiro kernel de sistema operacional de uso geral cuja implementação em código foi matematicamente verificada, usando o assistente de provas Isabelle/HOL. Em vez de confiar em testes, fuzzing e revisão de código para reduzir a chance de bugs, a verificação formal demonstra, com rigor matemático, que o código faz exatamente o que a especificação diz, sob um conjunto explícito de premissas.

No caso da segurança, isso se traduz em uma garantia de isolamento: um ataque que compromete uma aplicação não crítica não consegue se propagar para uma aplicação crítica rodando na mesma máquina. Segundo a Proofcraft, é exatamente esse isolamento que o stack de provas agora garante em AArch64, dentro das premissas listadas pela equipe. Vale a ressalva: a prova vale sob essas premissas (por exemplo, sobre o comportamento do hardware e do compilador), não é uma garantia absoluta contra qualquer ataque físico ou de canal lateral fora do modelo.

Por que AArch64 é o alvo relevante

O seL4 nasceu com verificação na arquitetura ARMv7 (32 bits) e vinha expandindo a cobertura. Um dos marcos recentes, divulgado nos cinco anos da Proofcraft, foi que as provas do seL4 passaram a cobrir 100% das plataformas ARM em que o kernel roda, permitindo que o usuário escolha livremente a plataforma ARM sabendo que está sobre uma base verificada. Esse esforço faz parte do programa PROVERS da DARPA.

AArch64 é a arquitetura por trás de praticamente tudo que é embarcado moderno: SoCs de celular, gateways de IoT, unidades de controle automotivas, dispositivos de borda. Ter o stack de segurança completo em 64 bits ARM significa que quem projeta esses sistemas passa a ter uma opção de kernel com garantia formal de isolamento na arquitetura que já usa na prática, sem precisar recair no ARMv7 mais antigo.

Os avanços que vieram junto

Os meses anteriores mostram um roadmap ativo além da confidencialidade:

• MCS verificado em RISC-V (junho de 2026): a configuração de mixed-criticality systems (MCS), a maior funcionalidade nova do seL4, teve a correção funcional provada pela primeira vez, mirando RISC-V. MCS é indispensável para aplicações de tempo real com criticidade mista, como casos de uso automotivos, e a prova está sendo portada para ARM 64 bits também como parte do programa PROVERS da DARPA.
• Escalonador de domínios dinâmico (junho de 2026): antes, a prova de fluxo de informação exigia um escalonamento totalmente estático, compilado dentro do kernel, o que obrigava o desenvolvedor a fixar de antemão o tempo de cada domínio por toda a vida do sistema. A nova API permite escalonamentos semi-estáticos: um sistema com proteção de fluxo de informação pode ter uma fase de boot com fatias de tempo maiores (para VMs subirem sem estourar o tempo alocado) e uma fase operacional com fatias menores para maior responsividade↳Design responsivo4 conteúdosDicas de Front-End para usabilidade, acessibilidade, performance e responsividadeProduto & UX · fev 2025Tipos de layouts e suas diferençasProduto & UX · jan 2025Dica de ouro: Saiba como fazer uma navbar responsivaDev (Back & Front) · jun 2025Ver tudo em Produto & UX →. Isso já está implementado, verificado e disponível no seL4 15.0.0, e facilita o uso de ferramentas em estilo SDK como o Microkit.
• Multikernel estático: a Proofcraft vem estendendo as provas para uma configuração multikernel, em que cada núcleo de CPU roda uma instância separada do seL4, permitindo ganho de performance com múltiplos cores sem abrir mão das garantias no nível do kernel.

O que muda para quem constrói no Brasil

Para o dev brasileiro que trabalha com embarcados, IoT ou infraestrutura crítica, o recado prático é que existe um kernel com garantia matemática de isolamento pronto para a arquitetura ARM 64 bits que domina o mercado de hardware. Em setores como automotivo, dispositivos médicos, defesa e sistemas industriais, onde uma falha de isolamento pode ter consequências físicas, essa base muda o argumento de segurança: em vez de "testamos bastante", passa a ser possível dizer "há uma prova de que aplicações não críticas não comprometem as críticas".

O seL4 é open source e mantido pela seL4 Foundation, então não há barreira de licença para experimentar. Para adotar de verdade, porém, é preciso arquitetar o sistema em cima do modelo de capabilities do kernel e das ferramentas do ecossistema (como o Microkit), o que exige investimento de aprendizado. As garantias formais também valem apenas dentro das premissas declaradas, um ponto que qualquer equipe precisa entender antes de usar a prova como argumento de conformidade.

O que ainda está em aberto

Alguns esforços seguem em andamento e vale acompanhar: a portabilidade do MCS de RISC-V para ARM 64 bits, a evolução da configuração multikernel e a maturação das APIs de escalonamento dinâmico. A Proofcraft mantém três grandes projetos em paralelo financiados por DARPA, pela Cyberagentur alemã e pelo NCSC britânico. O seL4 summit 2026 acontece em Vancouver, de 1 a 3 de setembro, e costuma ser onde os próximos passos do roadmap aparecem.

Fonte: Hacker News