O que aconteceu: provas do seL4 no AArch64

Em 21 de agosto de 2026, a Proofcraft anunciou a conclusão da prova formal de confidencialidade do seL4 no AArch64. A novidade completa, para essa arquitetura, o conjunto de propriedades de segurança descrito no anúncio: correção funcional, integridade e confidencialidade. O resultado é uma evidência matemática, verificada por ferramentas formais, de que o kernel aplica a propriedade de confidencialidade dentro do modelo e das premissas declaradas pelo projeto.

O AArch64 é a arquitetura Arm de 64 bits. A notícia não descreve um ataque, um vazamento ou uma falha corrigida por atualização. Também não apresenta um CVE, uma pontuação CVSS ou uma prova de que todos os componentes de um sistema baseado em seL4 estejam automaticamente seguros. O valor do anúncio está em ampliar a confiança no núcleo de isolamento que fica entre aplicações e recursos do sistema.

Para profissionais de segurança, a distinção é essencial. Uma prova formal não é um selo genérico para qualquer produto que use o kernel. Ela é uma demonstração sobre uma implementação, uma arquitetura, uma configuração e um conjunto de hipóteses. A pergunta correta passa a ser: o sistema que será colocado em produção corresponde ao escopo verificado?

Como funciona a confidencialidade formal

Confidencialidade, nesse contexto, significa impedir que uma aplicação obtenha informação de outra aplicação sem autorização. O kernel controla recursos de memória, capacidades e transições entre níveis de execução. A prova relaciona o comportamento do código implementado a uma especificação abstrata e verifica que os fluxos permitidos respeitam as regras de isolamento expressas nessa especificação.

A ideia é diferente de procurar padrões conhecidos de erro em um teste ou em uma ferramenta de análise estática. Testes executam alguns caminhos com entradas escolhidas. A verificação formal tenta demonstrar que uma propriedade é válida para todos os estados e transições abrangidos pelo modelo. Isso exige especificações precisas, invariantes, modelos de hardware e ferramentas capazes de checar as provas.

O projeto seL4 separa propriedades. A correção funcional trata da conformidade do código com a especificação. A integridade trata, em termos práticos, de impedir modificações não autorizadas em dados. A confidencialidade trata de impedir leituras ou inferências não autorizadas dentro dos canais representados pelo modelo. Essa separação ajuda a evitar a conclusão incorreta de que uma propriedade substitui as demais.

O resultado também depende do modo como o sistema é construído. A equipe precisa usar a plataforma e a configuração compatíveis com a prova, respeitar as exigências do build e validar os componentes que ficam fora do kernel. Um sistema pode ter um núcleo formalmente verificado e ainda conter drivers, boot code, serviços ou políticas com problemas.

Quem foi afetado e para que serve

Não há indicação, na fonte do anúncio, de vítimas ou de organizações afetadas por um incidente. O público diretamente interessado é formado por equipes que projetam sistemas embarcados, dispositivos de alta criticidade, componentes de defesa em profundidade e plataformas que precisam separar aplicações com diferentes níveis de confiança.

Em uma arquitetura isolada, uma aplicação não deveria conseguir transformar um erro local em comprometimento de outra aplicação crítica. A Proofcraft descreve o objetivo como impedir que ataques contra aplicações não críticas se propaguem para aplicações críticas. Isso é relevante em cenários nos quais um componente de rede, uma interface de usuário ou um serviço de atualização tem uma superfície de ataque maior do que o componente que protege chaves, comandos ou dados sensíveis.

O benefício é arquitetural. Em vez de confiar apenas em processos, permissões e revisão de código em cada serviço, a equipe pode colocar uma barreira de menor nível entre domínios. Ainda assim, a prova não decide quais aplicações devem compartilhar dados, não configura políticas de autorização sozinha e não garante que uma aplicação não vaze um segredo por um canal que esteja fora do modelo.

Para quem avalia uma adoção, a notícia serve como ponto de partida para uma análise de assurance. É necessário mapear a placa, o processador, o boot, o hypervisor quando existir, os drivers, os dispositivos com DMA, o compilador, a configuração do kernel e a política de comunicação entre componentes. Cada item deve ser comparado com a documentação de verificação, e não apenas com o nome da arquitetura.

Como identificar e acompanhar a evidência

Como não se trata de um incidente com indicadores de comprometimento, a detecção aqui significa conferir o estado da verificação e a correspondência da implementação. O primeiro passo é registrar a plataforma exata usada pelo produto. AArch64 identifica uma família de arquitetura, mas não descreve sozinha a placa, o firmware, os dispositivos, a configuração do kernel ou o caminho de boot.

Em seguida, a equipe deve consultar o status oficial das provas do seL4 e manter no processo de build a versão, o commit, as opções e os artefatos que foram analisados. O objetivo é tornar possível responder, meses depois, qual código foi compilado, com quais parâmetros e qual conjunto de provas se aplica a ele. Logs de CI devem registrar falhas de compilação, mudanças de configuração e diferenças entre a configuração testada e a configuração liberada.

Também é importante acompanhar os componentes fora do kernel. Uma revisão deve identificar drivers que acessam memória, código de inicialização, módulos em assembly, mecanismos de virtualização, tabelas de memória e caminhos de comunicação. Se um componente depende de DMA, o time precisa documentar quem pode escrever na memória e como essa capacidade é limitada ou verificada.

Uma checagem útil é manter uma matriz de escopo: propriedade verificada, arquitetura, configuração, versão, componentes assumidos e evidência disponível. Se uma célula ficar sem fonte ou sem artefato reproduzível, ela deve ser tratada como risco de assurance, mesmo que o sistema continue funcionando normalmente.

Como se proteger e reduzir o risco

A primeira medida é não tratar o anúncio como substituto para atualização, hardening ou monitoramento. Use uma versão e uma configuração suportadas pelo projeto, valide a documentação de verificação e preserve a cadeia de build. Mudanças aparentemente pequenas em opções, inicialização, drivers e mapa de memória podem retirar o sistema do escopo da prova.

Revise o boot. A página oficial de premissas informa que a prova considera o kernel depois de ele ser carregado corretamente na memória e colocado em um estado inicial consistente. Portanto, firmware, carregador, medição de integridade e sequência de inicialização precisam de controles próprios. A confiança no kernel não corrige uma imagem adulterada antes de sua entrada em execução.

Revise DMA e dispositivos. A prova assume que a CPU e a MMU são os únicos dispositivos com acesso direto à memória, ou que dispositivos DMA não se comportem de modo adverso. Drivers de dispositivos com essa capacidade exigem atenção especial e podem precisar de verificação formal ou de um componente verificado que valide os acessos.

Por fim, trate canais laterais, hardware e disponibilidade como camadas separadas. O projeto explica que a prova de confidencialidade cobre os canais visíveis no modelo, mas não cobre canais de tempo. Controle acesso físico, escolha políticas de isolamento, reduza a superfície dos serviços e monitore eventos de boot, falhas de integridade e alterações de configuração.

Comparação com testes e marcos anteriores

Testes continuam necessários, mas respondem a uma pergunta diferente. Eles ajudam a encontrar defeitos em exemplos concretos, verificar integração, medir desempenho e observar o comportamento em hardware real. A prova formal busca estabelecer propriedades para o conjunto de estados representado pelo modelo. Nenhuma das duas abordagens, sozinha, cobre todos os riscos de um produto completo.

O histórico apresentado pela Proofcraft ajuda a entender o avanço. Em 2024, a organização anunciou a prova de correção funcional do seL4 no AArch64. Em 2025, anunciou a prova de integridade nessa arquitetura. Em 2026, anunciou a prova de confidencialidade. São marcos relacionados, mas não são sinônimos. A conclusão de uma propriedade não transforma automaticamente as outras em garantias universais.

A comparação também pode ser feita com um kernel sem prova equivalente. Nesse caso, a equipe ainda pode obter um nível alto de segurança com revisão, testes, análise estática, isolamento, atualização e resposta a incidentes. A diferença é a quantidade e a natureza das evidências disponíveis sobre o núcleo. O seL4 acrescenta uma demonstração formal ao conjunto de controles, com o custo de respeitar premissas e manter a configuração dentro do escopo.

O anúncio, portanto, não deve ser usado em marketing como proteção absoluta. Ele é mais útil em uma decisão técnica que documenta quais riscos a prova reduz, quais riscos permanecem e quais componentes precisam de uma avaliação independente.

Análise técnica do anúncio

Não há CVE, CVSS ou PoC associados ao anúncio da conclusão da prova de confidencialidade. Ele também não relata exploração ativa. Classificá-lo como vulnerabilidade seria incorreto. A análise técnica deve se concentrar no significado da propriedade, no limite do modelo e na diferença entre o kernel verificado e o sistema final.

A documentação oficial do seL4 lista premissas importantes. O código em assembly é assumido como correto. O hardware é assumido como funcionando de acordo com a especificação e sem adulteração. O gerenciamento de cache, cache colouring e TLB é tratado com premissas sobre a camada de máquina. O boot code não está todo dentro do mesmo escopo, pois a prova parte de um kernel carregado corretamente.

A documentação também explica que a memória virtual é verificada, mas há uma parte do modelo que depende de condições justificadas e ainda pode conter erro humano. Para a confidencialidade, os canais laterais dependem do que o modelo de hardware captura; canais de tempo não estão cobertos. A página informa ainda que, em arquiteturas com verificação em nível de binário, compilador e linker não precisam ser confiados da mesma forma, desde que as configurações corretas sejam usadas.

Esses limites não invalidam a prova. Eles tornam a evidência utilizável. Uma equipe consegue apontar exatamente quais partes ainda exigem revisão, teste, controle físico ou outra técnica formal. Em segurança, explicitar a fronteira de uma garantia é mais útil do que prometer uma cobertura que a evidência não sustenta.

Impacto e consequências para projetos críticos

O principal impacto é a redução do risco de uma falha em uma aplicação atravessar o limite de isolamento e atingir outra aplicação. Esse ganho pode apoiar arquiteturas com componentes de confiança diferente, desde que os fluxos de informação tenham sido definidos corretamente e que os componentes externos atendam às premissas.

Há também uma consequência de processo. A organização que adota um kernel formalmente verificado precisa tratar configuração e proveniência como parte da segurança. A lista de materiais do software, o commit usado, os artefatos de build e as alterações em drivers deixam de ser detalhes operacionais. Eles passam a ser evidência para uma afirmação de segurança.

No aspecto reputacional e regulatório, uma prova pode melhorar a qualidade da documentação de assurance, mas não substitui certificação, análise de risco, requisitos de privacidade ou controles específicos do setor. A prova não elimina a necessidade de registrar incidentes, aplicar correções, proteger dados pessoais ou demonstrar que o produto completo atende à legislação aplicável.

O impacto operacional pode incluir treinamento, pipelines mais rigorosos e uma seleção menor de configurações. Esse custo é esperado. A decisão deve comparar o custo de manter as premissas com o custo potencial de uma falha de isolamento em um componente crítico. Para serviços comuns, controles tradicionais podem ser mais adequados. Para sistemas com fronteiras fortes de confiança, a evidência adicional pode justificar o investimento.

Dicas práticas e boas práticas

Antes de adotar o seL4 no AArch64, transforme a notícia em perguntas verificáveis. Qual é a placa exata? Qual é a versão do kernel? Qual configuração foi provada? O boot está dentro do escopo ou é tratado separadamente? Há dispositivos DMA? O firmware é medido e atualizado com controle de integridade? Os serviços usam apenas os canais de comunicação previstos?

Mantenha uma política de mudanças. Toda alteração de arquitetura, compilador, opções de build, mapa de memória, driver ou componente privilegiado deve gerar uma revisão de escopo. Não aceite a frase arquitetura compatível como única evidência. Exija a referência para a prova aplicável, o artefato do build e a justificativa para cada premissa.

Use defesa em profundidade. Separe segredos em domínios mínimos, reduza interfaces, limite privilégios, valide entradas nos componentes de serviço, monitore falhas e mantenha uma estratégia de recuperação. Controle o acesso físico ao dispositivo e proteja o processo de atualização. Se o produto processa dados pessoais, aplique minimização, retenção e registro de acesso independentemente da proteção do kernel.

Uma checklist curta para auditoria é: confirmar a versão e a plataforma; registrar a configuração; consultar as provas oficiais; revisar boot e assembly; avaliar DMA; avaliar canais laterais; testar serviços e integração; registrar exceções; e repetir a análise quando houver mudança relevante.

Conclusão: o que fazer agora

A conclusão das provas de segurança do seL4 no AArch64 é uma notícia importante para quem trabalha com isolamento de sistemas. Ela indica que a propriedade de confidencialidade foi formalmente estabelecida para o escopo anunciado, depois dos marcos de correção funcional e integridade. Isso fortalece a base técnica para sistemas que precisam impedir fluxos não autorizados entre aplicações.

O próximo passo não é instalar um componente e declarar o risco resolvido. É comparar o sistema real com a prova. Documente arquitetura, versão, configuração, boot, hardware, drivers, DMA e canais de comunicação. Valide o build, preserve a evidência e trate cada premissa fora do escopo com um controle específico.

Para acompanhar a evolução, consulte o anúncio da Proofcraft e as páginas oficiais de provas e premissas do seL4. Em uma avaliação de segurança, a pergunta mais valiosa continua sendo simples: qual afirmação está provada, sob quais condições, e como demonstramos que o produto em produção ainda satisfaz essas condições?