seL4: o kernel que a matemática provou livre de bugs — não apenas testado

Por

Em algum momento de 2016, uma equipe de hackers profissionais recebeu autorização quase total para invadir os sistemas de um helicóptero autônomo Boeing, o Little Bird, com acesso de rede mais generoso do que qualquer adversário real teria. O objetivo era simples de enunciar e brutal de executar: assumir o controle de voo da aeronave. Eles tinham seis semanas. O helicóptero chegou a voar, com pilotos reais a bordo por segurança, enquanto a equipe atacante tentava tudo o que sabia. Na parte do sistema protegida pelo software em questão, não conseguiram entrar.

Isso não seria particularmente notável se estivéssemos falando de um software “bem testado”. Praticamente todo sistema crítico do mundo passa por testes extensos antes de operar — aviação, usinas nucleares, sistemas bancários. E, mesmo assim, bugs continuam aparecendo, porque testar significa apenas verificar um conjunto finito de situações e torcer para que as que não foram verificadas não escondam um problema. O software por trás da defesa do Little Bird era diferente: sua correção não havia sido apenas testada, mas demonstrada por prova matemática, verificada mecanicamente por um programa de computador que checou cada passo do raciocínio, célula por célula, como se fosse um assistente de matemática incansável e implacável.

O nome desse software é seL4. É um microkernel — um núcleo de sistema operacional propositalmente minúsculo, com pouco mais de dez mil linhas de código — e é, até onde a comunidade de ciência da computação sabe, o primeiro kernel de uso geral do mundo cuja implementação em C foi provada matematicamente correta em relação a uma especificação formal do seu comportamento. Este artigo apura o que essa afirmação significa de verdade, de onde ela vem e onde termina.

Provar versus testar: a diferença que muda tudo

Testar um programa é rodá-lo com entradas específicas e conferir se o resultado é o esperado. É útil e necessário, mas é, por definição, incompleto: um programa pode passar em milhares de testes e ainda conter um erro que só se manifesta com uma combinação de condições que ninguém pensou em experimentar. A famosa observação do cientista da computação Edsger Dijkstra resume o problema: testes podem mostrar a presença de erros, nunca a sua ausência.

Provar matematicamente a correção de um programa é outra categoria de garantia. Em vez de escolher casos e observar o comportamento, o processo formaliza tanto o código quanto uma especificação do que ele deveria fazer — usando lógica matemática — e então constrói, passo a passo, uma demonstração de que o código satisfaz a especificação para absolutamente todas as entradas possíveis dentro daquele modelo. Não é uma amostra: é a totalidade do espaço de comportamento coberto pela especificação.

A parte “mecanicamente verificada” é o que separa isso de uma prova em um quadro-negro. No caso do seL4, a prova inteira foi escrita e checada dentro do Isabelle/HOL, um assistente de prova amplamente usado na pesquisa acadêmica em verificação formal. Cada linha de raciocínio foi validada por máquina, não apenas revisada por um humano que pode errar ou se cansar — o que reduz drasticamente, embora não elimine por completo, a chance de que a “prova” esconda uma falha de lógica despercebida.

Dez mil linhas de código, duzentas mil linhas de prova

O trabalho que tornou o seL4 famoso na comunidade acadêmica foi publicado no artigo “seL4: Formal Verification of an OS Kernel”, de Gerwin Klein e colegas, apresentado no 22º ACM Symposium on Operating Systems Principles (SOSP), em Big Sky, Montana, em outubro de 2009. O projeto havia começado em 2004, liderado por Gernot Heiser, Kevin Elphinstone e o próprio Klein, então na NICTA, instituição de pesquisa australiana. Em 29 de julho de 2009, a equipe eliminou o último “sorry” — o marcador que o Isabelle/HOL usa para uma etapa da prova ainda não demonstrada — fechando a primeira prova de correção funcional, verificada mecanicamente, de um kernel de sistema operacional completo e de uso geral.

Os números, segundo o whitepaper oficial mantido pela seL4 Foundation, dão a medida do esforço: o kernel em si tem cerca de 8.700 linhas de código C mais 600 linhas de assembly — da ordem de dez mil linhas ao todo, fração minúscula perto dos cerca de vinte milhões de linhas do núcleo do Linux. A prova de correção funcional publicada em 2009 somava cerca de 200 mil linhas de script formal no Isabelle/HOL — muito mais texto de prova do que de código-fonte, o que é típico nesse tipo de verificação. Depois de 2009, a base de provas continuou crescendo, incorporando demonstrações adicionais de integridade e confidencialidade, e hoje ultrapassa largamente aquele número original.

É importante frisar o que a prova de 2009 cobre: ela garante que a implementação em C do kernel corresponde a uma especificação abstrata do seu comportamento — o que inclui, entre outras coisas, que o kernel nunca trava e nunca executa uma operação classificada como insegura dentro daquele modelo. Trabalhos posteriores da mesma equipe estenderam a cadeia de provas para incluir propriedades de integridade e confidencialidade de informação, e para conectar a especificação abstrata ao código binário efetivamente executado pelo processador, fechando lacunas entre “o que foi provado” e “o que realmente roda no hardware”.

O teste que a Darpa fez com um helicóptero de verdade

A pesquisa em torno do seL4 chamou a atenção da Darpa, a agência de pesquisa avançada de defesa dos Estados Unidos, que entre 2012 e 2017 financiou o programa HACMS (High-Assurance Cyber Military Systems, algo como “sistemas militares cibernéticos de alta confiança”). O objetivo era demonstrar que métodos formais — a mesma família de técnicas usada para provar o seL4 — poderiam eliminar categorias inteiras de vulnerabilidades exploráveis em sistemas embarcados, sem sacrificar desempenho. Vale registrar isso como fato histórico neutro: a origem do financiamento é militar e o caso de teste mais visível envolveu uma aeronave militar não tripulada, o que não constitui, em si, endosso nem crítica ao uso militar da tecnologia — apenas explica de onde vieram os recursos e o cenário de teste mais divulgado.

Segundo relato da Quanta Magazine, publicado em setembro de 2016, e confirmado pela página oficial da Darpa sobre o caso, o teste mais dramático do programa usou um helicóptero autônomo Boeing Little Bird. Antes da aplicação das técnicas formais, uma equipe de invasores conseguiu acesso completo aos sistemas de computador do helicóptero rapidamente. Depois que o software foi reestruturado em partições protegidas por componentes com garantias formais — a mesma abordagem testada antes em um quadricóptero —, o cenário mudou: durante seis semanas, com acesso de rede mais amplo do que um adversário real teria e acesso concedido de antemão à partição da câmera, a equipe de invasores não conseguiu escapar dela para comprometer os sistemas de voo. O teste incluiu um voo real, com pilotos a bordo por precaução, e, segundo Kathleen Fisher, gerente do programa na Darpa, os pilotos não notaram diferença de desempenho em relação ao sistema original. A página histórica do próprio projeto seL4 identifica esse software como um dos componentes de alta confiança usados no endurecimento cibernético do Little Bird dentro do HACMS, ao lado de outros veículos autônomos testados no mesmo programa, como caminhões e robôs terrestres.

Onde o seL4 realmente funciona hoje — e onde as lendas urbanas erram

É comum encontrar, em textos sobre o assunto, a afirmação de que o seL4 protege diretamente o “enclave seguro” dos iPhones e os modems celulares da Qualcomm. A apuração para este artigo encontrou uma nuance que vale corrigir: segundo o próprio whitepaper da seL4 Foundation e um texto do pesquisador Gernot Heiser, o que roda nesses dispositivos é um kernel anterior da mesma família L4 — o “L4-embedded” no caso do enclave seguro da Apple, e o OKL4 no caso dos modems da Qualcomm —, desenvolvido pelo mesmo grupo de pesquisa antes da conclusão da prova do seL4 em 2009, mas que não é o seL4 propriamente dito nem carrega sua prova de correção. A documentação de segurança da própria Apple confirma apenas que o processador do enclave seguro roda “uma versão customizada do microkernel L4”, sem citar o seL4 nominalmente.

Os usos documentados do seL4 verificado propriamente dito são outros, e mais recentes. A montadora chinesa NIO afirma produzir em série o veículo elétrico ONVO L60 rodando o SkyOS-M, sistema operacional construído sobre o seL4. A DornerWorks oferece ferramentas para sistemas de defesa e aeroespaciais baseados no kernel; a MEP o usa em comunicação de voz para controle de tráfego aéreo e marítimo; a Kry10 construiu sobre ele um sistema operacional para dispositivos conectados de missão crítica; e a HENSOLDT Cyber desenvolve, com base no seL4, sistemas seguros em RISC-V para defesa, aviônica e uso automotivo. O próprio programa HACMS, discutido acima, segue sendo o caso mais citado e mais rigorosamente documentado publicamente.

O que a prova não garante

Nenhuma dessas conquistas transforma o seL4 em garantia de que qualquer sistema construído sobre ele está livre de falhas. A prova matemática cobre o kernel — o núcleo mínimo que gerencia memória, processos e comunicação entre partes isoladas do sistema — dentro de um modelo formal específico, que inclui premissas sobre o compilador e, em parte, sobre o hardware subjacente. Ela não se estende automaticamente a aplicações que rodam sobre o kernel, a drivers de dispositivo, nem a erros de configuração cometidos por quem integra o seL4 em um produto final. Um sistema pode usar um kernel formalmente correto e ainda ser vulnerável por uma falha em uma aplicação vizinha, ou por uma decisão equivocada em como as partições foram divididas — como o próprio teste do Little Bird ilustra: a equipe de invasores obteve acesso à partição da câmera precisamente porque essa partição não fazia parte do que estava sendo protegido pela prova.

É esse ponto, mais do que qualquer número de linhas de código, que resume o valor real do seL4: ele não elimina a necessidade de engenharia de segurança cuidadosa em todo o resto do sistema, mas remove uma categoria inteira e historicamente enorme de risco — bugs de implementação no próprio núcleo do sistema operacional — ao trocar “confiamos que testamos o suficiente” por “provamos matematicamente que está correto dentro deste modelo”.

Fontes citadas neste artigo:

Deixe um comentário