Atmosphere: kernels verificados práticos com Rust e Verus

Os kernels formalmente verificados continuam raros porque prová-los era caro. Os autores lembram que o seL4 exigiu 11 pessoas-ano para as provas, mais 9 para frameworks e ferramentas de apoio, e que verificadores push-button como o Hyperkernel compraram automação restringindo a interface do kernel (todo caminho precisa ser finito, então a chamada de abertura de arquivo obriga o usuário a escolher o número do descritor). Enquanto isso, a viabilidade de verificar código de sistema rico em funcionalidades e cheio de ponteiros ainda é, nas palavras dos autores, um debate em aberto.

Este artigo do SOSP 2025 (Seul), da University of Utah (Vikram Narayanan hoje consta na Palo Alto Networks, e o trabalho foi feito em Utah), pergunta se o Verus, um verificador de Rust baseado em SMT, consegue verificar um microkernel completo a um custo modesto. O Atmosphere é a resposta: processos, threads, memória dinâmica, IPC baseado em endpoints, espaços de endereçamento virtuais, suporte a IOMMU e containers, tudo em Rust, com drivers e pilhas de rede rodando no userspace.

Termos-chave: refinamento significa que a implementação corresponde a uma especificação abstrata de alto nível do kernel. Boa formação (well-formedness) significa que os invariantes de cada estrutura de dados valem depois de cada chamada de sistema. Uma permissão rastreada (tracked) é um token fantasma linear que o Verus exige antes de um ponteiro bruto poder ser usado. Um container é um grupo de processos com uma cota de memória e um conjunto de cores de CPU garantidos. Não interferência significa que as chamadas de sistema de um container não conseguem alterar o estado observável de outro.

Vale conhecer antes: propriedade e empréstimo (ownership e borrowing) em Rust, pré e pós-condições, e como um solver SMT trata fórmulas quantificadas. O RustBelt é a explicação formal de por que a disciplina de ownership do Rust merece confiança, e o artigo o cita, junto com o Viper e o Prusti, como trabalho anterior sobre raciocínio baseado em permissões.

• Um microkernel verificado feito em grande parte de peças comuns de kernel. Ele roda em hardware multi-CPU sob um único big lock global, com interrupções desabilitadas dentro do kernel. Os autores relatam 6K linhas de código executável e 20,1K linhas de código de prova: 14,3K de especificações (2,9K delas a especificação de mais alto nível da interface de chamadas de sistema) e 5,8K de dicas e provas.
• Design centrado em ponteiros. As estruturas do kernel usam ponteiros brutos, não lineares, como faria um C inseguro, incluindo ponteiros reversos dos filhos para os pais, armazenamento interno de listas e árvores e remoção em tempo constante de listas encadeadas. O Verus confere cada operação com ponteiros por meio do tipo de ponteiro com permissão PPtr<T> e da permissão fantasma PointsTo<T>.
• Armazenamento plano de permissões. As permissões de todos os nós de uma estrutura recursiva ficam em um único mapa no topo do subsistema, por exemplo, o gerenciador de processos guarda mapas de todos os containers, processos, threads e endpoints. Propriedades de uma árvore ilimitada podem então ser enunciadas sem recursão. O invariante de caminho dos containers, normalmente uma definição recursiva entre pai e filho, vira uma única afirmação sobre todos os nós, e um conjunto fantasma subtree por container dá acesso direto a todos os descendentes.
• Separação entre provas estruturais e não estruturais. Os invariantes estruturais (a árvore não tem ciclos, os ponteiros reversos estão certos) ficam em funções de especificação fechadas (closed), que não custam nada fora do seu módulo. Uma chamada de sistema como new_container declara apenas como o estado muda, e uma função de prova separada mostra que a mudança preserva o invariante estrutural.
• Gerenciamento manual de memória. O Atmosphere não depende do borrow checker nem dos smart pointers do Rust para o tempo de vida dos objetos do kernel. Os objetos recebem páginas de 4KB, 2MB ou 1GB de um alocador cujo estado é exposto às especificações, e cada objeto tem um page_closure(). Os autores provam a disjunção local e juntam os closures de baixo para cima, o que dá segurança de memória e ausência de vazamentos sem uma prova global par a par.
• Containers e não interferência. Os containers formam uma árvore, e a única forma de revogar os recursos de um container é terminá-lo, uma perda deliberada de revogação de granularidade fina que simplifica o raciocínio sobre o código do usuário. Para dois containers não confiáveis A e B e um container compartilhado verificado V, os autores provam isolamento de memória e de endpoints sob chamadas de sistema arbitrárias, e depois derivam a não interferência de três condições de unwinding: consistência de saída, consistência de passo e respeito local.

O kernel é modelado como uma máquina de estados sobre um estado abstrato. Dois teoremas são provados: o refinamento da especificação abstrata e a boa formação de uma hierarquia de invariantes depois de cada transição. Especificações e provas são código fantasma, apagado em tempo de compilação, então a verificação não adiciona custo em tempo de execução.

A avaliação pergunta se o desenvolvimento verificado é prático e se o kernel abre mão de desempenho. O tempo de verificação é medido em um servidor c220g5 do CloudLab (dois Xeon Silver 4114 de 10 cores, 192 GB) e em um laptop com i9-13900HX. Os testes de rede usam máquinas c220g2 com NICs de 10Gb, os de NVMe usam máquinas d430, todas com Ubuntu 20.04 e kernel 5.4.0, com hyper-threading, turbo boost, estados de ociosidade e escalonamento de frequência desabilitados. As comparações são a page table verificada em Verus do NrOS, o Mimalloc e o VeriSMo para esforço de prova, o seL4 para chamadas de sistema sob KVM, e Linux, DPDK, SPDK, fio e Nginx para drivers e aplicações. Os autores escreveram um driver de rede Ixgbe e um driver NVMe, além de Maglev, um key-value store e um pequeno servidor web por cima deles.

Estes são os resultados relatados pelos autores.

• Esforço de prova. O Atmosphere tem razão entre prova e código de 3,32:1 (a Tabela 2 lista 20.098 linhas de prova para 6.048 de código), contra 20:1 do seL4 e 14,9:1 do CertiKOS. O VeriSMo é menor, com 2:1, o que os autores atribuem a uma semântica mais simples e a um timeout de verificação relaxado que troca velocidade por menos linhas de prova.
• Tempo de verificação. No servidor c220g5, a verificação completa leva 3m29s com uma thread e 1m7s com oito, contra 12m11s do VeriSMo e 1m40s do Mimalloc com oito threads. No laptop leva menos de 20 segundos com 32 threads e 47 segundos com uma.
• O design plano compensa em uma comparação direta. Para page tables comparáveis, a do Atmosphere tem razão de 4,3:1 contra 13,3:1 do NrOS (o texto diz 4,4:1) e verifica em 33 segundos com uma thread contra 1m52s. O NrOS precisa de cerca de 200 linhas de prova para desenrolar suas especificações recursivas em uma função, enquanto o Atmosphere precisa de cerca de 30 linhas para mostrar que as demais entradas não mudam.
• Esforço de desenvolvimento. Três versões sucessivas levaram cerca de 2 pessoas-ano no total, com aproximadamente 14 meses no código verificado: 2 meses para uma pessoa, 8 meses para duas e 4 meses para uma que reaproveitou metade do código anterior.
• IPC e chamadas de memória. Sob KVM, call e reply levam cerca de 1.058 ciclos contra 1.026 do seL4, e mapear uma página leva cerca de 1.984 contra 2.650, embora os autores observem que as chamadas não são estritamente equivalentes.
• Driver de rede. Com lotes de 32 pacotes, tanto o Atmosphere quanto o DPDK atingem a taxa de linha de 14,2 Mpps do 10GbE, enquanto o Linux chega a 0,89 Mpps. Com a aplicação em um processo separado no mesmo core, o Atmosphere atinge 2,3 Mpps por core com uma troca de contexto por pacote e 11,1 Mpps com lotes de 32.
• Driver NVMe. Ele se comporta como o SPDK em leituras sequenciais e atinge o máximo do dispositivo. Em escritas com lote de 32, chega a 232K IOPS, um overhead de 10% sobre um máximo do dispositivo próximo de 256K IOPS, do qual o Linux com fio fica a até 3%. Em leituras, o fio atinge 13K e 141K IOPS por core com lotes de 1 e 32.
• Aplicações. O Maglev atinge 1,0 Mpps por core com sockets do Linux e 9,72 Mpps por core com DPDK. No Atmosphere ele atinge 13,3 Mpps com o driver em outro core, 8,8 Mpps em um core com lotes de 32 e 1,66 Mpps com lotes de 1. O servidor web atende 99,4K requisições por segundo ligado ao driver, contra 70,9K do Nginx no Linux.

O artigo é aberto sobre vários limites. As provas cobrem apenas chamadas de sistema, não o código do usuário, e canais de temporização por caches compartilhados e outros recursos de hardware ficam fora do escopo. Chamadas longas (mapear ou enviar grandes regiões, terminar containers) seguram o big lock por muito tempo e podem vazar informação de temporização, um limite que os autores removeriam limitando o tamanho das regiões e tornando o kill iterativo, como faz o seL4. O container compartilhado V tem um processo e uma thread, e as provas para drivers compartilhados concorrentes ficam como trabalho futuro. A base de computação confiável é listada por inteiro: Verus, Z3, o compilador e a biblioteca core do Rust, especificações de tipos do core, cerca de 700 linhas de axiomas ausentes, cerca de 300 linhas de funções setter com 1.900 linhas de especificações (o Verus não tem referências mutáveis para permissões rastreadas), 172 linhas de assembly, aproximadamente 3.000 linhas de Rust confiável, o boot loader e o hardware.

Os pontos a seguir são uma leitura das evidências, não afirmações do artigo.

• Os números de esforço não batem. O resumo e a introdução dizem menos de 2,5 pessoas-ano, 1,5 delas em verificação, enquanto a Seção 6.3 diz cerca de 2 pessoas-ano com aproximadamente 14 meses no código verificado. As três etapas listadas somam cerca de 22 pessoas-mês. Uso o número da Seção 6.3.
• O número do laptop esconde a quantidade de threads. "Menos de 20 segundos em um laptop moderno" vale com 32 threads. Com uma thread são 47 segundos, e no servidor são 1m7s com oito. A afirmação de que isso é mais rápido que compilar o kernel não é sustentada por uma medição.
• As razões entre prova e código comparam coisas diferentes. Elas cruzam Isabelle, Coq, Dafny e Verus, um big lock contra a concorrência de granularidade fina do CertiKOS, e escopos distintos. A discussão do VeriSMo mostra que a razão pode ser trocada por tempo de verificação, então é um guia aproximado.
• O design plano é testado em um único subsistema. A page table do NrOS é a única comparação direta. A árvore de containers, onde o artigo defende que a planicidade mais importa, não tem uma variante hierárquica para comparar, e nenhuma ablação isola cada escolha de design.
• As bases de desempenho diferem em funcionalidades. O seL4 oferece capabilities e revogação de granularidade fina que o Atmosphere omite, então 1.058 contra 1.026 ciclos compara tarefas diferentes. As diferenças para Linux, Nginx e Maglev mostram sobretudo o kernel bypass, que o DPDK também oferece, e o resultado de 13,3 Mpps usa dois cores enquanto o número do DPDK é por core. O kernel é testado com um ou dois cores, então a contenção no big lock não é medida. Os resultados do key-value store estão só em um gráfico, sem números declarados.
• A especificação de mais alto nível carrega a confiança. O refinamento vale contra 2,9K linhas de especificação das chamadas de sistema, e o texto não diz como elas foram conferidas contra o comportamento pretendido. O artigo não relata bugs encontrados pela verificação, embora diga que os testes exigiram bem menos esforço, sem números.
• A base confiável fica no caminho do isolamento. Cerca de 3.000 linhas de Rust confiável ficam ao lado de 6K linhas de código verificado, e 465 linhas que configuram a IOMMU estão entre elas, embora as page tables da IOMMU façam parte do subsistema de memória verificado. O isolamento de dispositivos depende das duas partes.
• A não interferência é mostrada para uma única configuração. Os autores argumentam que outros arranjos são parecidos ou mais simples, mas demonstram apenas A, B e V.

• Provas de serviços compartilhados concorrentes, como drivers intensivos em I/O, que os autores esperam ser viáveis porque os drivers modernos separam os planos de controle e de dados.
• Chamadas de sistema longas limitadas e iterativas, o que fecharia o vazamento de temporização e poderia abrir caminho para medir ou substituir o big lock.
• Reduzir a base confiável: verificar as cerca de 700 linhas de axiomas, substituir as funções setter conforme o Verus ganhar referências mutáveis para permissões rastreadas e cobrir o código de configuração da IOMMU e de interrupções.
• Um estudo controlado de permissões planas contra hierárquicas em uma estrutura maior, como a árvore de containers, com um registro dos bugs encontrados pela prova, para testar as afirmações de custo além de uma page table.