AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation

Problema
A verificação formal é crítica para garantir a segurança de protocolos criptográficos, mas continua sendo uma barreira significativa para os praticantes. Embora ferramentas como Tamarin e ProVerif tenham automatizado grande parte do processo de verificação, o hiato entre modelos simbólicos de alto nível e implementações concretas de protocolos persiste. Preencher esse hiato tradicionalmente exige perícia substancial em métodos formais para modelar manualmente implementações ou para interpretar resultados de verificação para bases de código específicas. Além disso, abordagens existentes que extraem modelos de linguagens de propósito geral frequentemente impõem restrições restritivas (como proibir loops ou recursão) para manter a tratabilidade, deixando partes da máquina de estados do protocolo sujeitas a suposições manuais. Essa limitação é problemática, pois vulnerabilidades históricas (ex: SKIP) originaram-se de máquinas de estados implementadas incorretamente. Adicionalmente, a transferência de resultados de verificação para implementações concretas carece de uma conexão sonora e automatizada, exigindo conhecimento especializado para garantir que uma propriedade provada em um modelo simbólico realmente se sustente no código em execução.

Metodologia
Os autores apresentam o AutoTam, uma abordagem inovadora de "primeiro a linguagem" (language-first) que integra implementação de protocolo, geração de modelo simbólico e execução simbólica dinâmica. O núcleo da metodologia é uma linguagem de domínio específico (DSL) projetada especificamente para protocolos criptográficos.

1. Linguagem AutoTam: A linguagem é projetada para alinhar-se ao nível de abstração de propriedades de segurança de alto nível, permanecendo executável. Ela modela protocolos como máquinas de estados finitos onde os papéis consistem em estados (divididos em partes de saída e entrada) e transições. A linguagem restringe o fluxo de controle ao nível da máquina de estados do protocolo para garantir a decidibilidade durante a tradução, evitando problemas de alcançabilidade indecidíveis. Ela suporta máquinas de estados arbitrárias, incluindo ciclos necessários para fases de transporte, mas limita escolhas intra-procedurais para fazerem parte da lógica da máquina de estados.
2. Interpretador e Execução: O AutoTam inclui um interpretador que executa descrições de protocolos diretamente. Isso permite o teste de interoperabilidade com implementações existentes (ex: WireGuard). O interpretador utiliza uma tabela de consulta para funções predefinidas (E/S de rede, operações criptográficas como ChaCha20-Poly1305, Ed25519 e Blake2s) implementadas via biblioteca formalmente verificada HACL.
3. Tradução Sonora para Tamarin: Os autores desenvolveram um procedimento de tradução que converte descrições de protocolos AutoTam em modelos Tamarin. A tradução mapeia transições estendidas (combinando a entrada do estado de origem, a lógica de transição e a saída do estado de destino) em regras de reescrita únicas do Tamarin. Os autores fornecem uma prova formal de sonidade (soundness), demonstrando que qualquer propriedade de traço provada no modelo Tamarin gerado se mantém na execução concreta da implementação AutoTam sob o modelo Dolev-Yao. Isso garante que os resultados de verificação sejam diretamente aplicáveis à implementação.
4. Integração de Execução Simbólica: Para abordar segurança de memória e erros de nível de implementação, o AutoTam integra-se ao motor de execução simbólica dinâmica KLEE. O interpretador é compilado para bytecode LLVM, e as funções criptográficas são substituídas por abstrações simbólicas. Isso permite a exploração sistemática de caminhos de execução sob entradas de rede arbitrárias, descartando erros de memória como estouros de buffer (buffer overflows).

Principas Contribuições

• Linguagem AutoTam: Uma linguagem de domínio específico totalmente executável para protocolos criptográficos que codifica naturalmente máquinas de estados, análise de mensagens e operações criptográficas.
• Extração de Modelo Sonora: Um procedimento para extrair modelos Tamarin de implementações executáveis, acompanhado de uma prova formal de sonoridade em relação a propriedades de traço. Isso garante que propriedades de traço universais verificadas no modelo se traduzam de volta para a implementação.
• Execução Simbólica Integrada: Um fluxo de trabalho totalmente integrado usando KLEE para analisar implementações AutoTam quanto à segurança de memória, fornecendo testes de cobertura completos contra entradas de rede arbitrárias.
• Estudos de Caso: A implementação e verificação de dois protocolos:
  • Um protocolo de troca de chaves Diffie-Hellman assinado.
  • O protocolo de VPN WireGuard.
    Os autores demonstram que sua implementação WireGuard é interoperável com as implementações existentes do kernel Linux e Go e atinge desempenho aceitável.

Resultados

• Eficiência de Verificação: A ferramenta gerou modelos Tamarin para ambos os estudos de caso em menos de 1 segundo. O protocolo Diffie-Hellman foi verificado para todas as propriedades de segurança (sigilo, autenticação) em menos de 5 segundos.
• Verificação do WireGuard: A verificação do modelo WireGuard exigiu a adição manual de um "lema de fontes" (sources lemma) para guiar o provador, um requisito comum para protocolos complexos no Tamarin. Apesar disso, o modelo gerado foi verificado com sucesso para propriedades de handshake (sigilo fraco e acordo injetivo) em aproximadamente 360 segundos.
• Fidelidade do Modelo: O modelo WireGuard gerado capturou mais detalhes do que vários modelos escritos por especialistas, incluindo a modelagem explícita de etapas de HKDF e validação/descriptografia de AEAD, que são frequentemente abstraídas em outros trabalhos.
• Segurança de Memória: A análise de execução simbólica explorou com sucesso milhares de caminhos de execução para ambos os protocolos (ex: 4.120 caminhos para o responder do WireGuard) e não encontrou erros de memória, descartando efetivamente estouros de buffer e bugs de implementação similares.
• Desempenho: A implementação baseada no interpretador AutoTam do WireGuard alcançou throughput comparável à implementação oficial WireGuard em Go ao rodar em hardware idêntico, apesar de carecer de otimizações de baixo nível específicas.

Significância
O artigo afirma que o AutoTam oferece um caminho simplificado para o desenvolvimento de protocolos seguros ao minimizar a necessidade de perícia em verificação formal durante a fase de implementação. Ao vincular a linguagem de implementação diretamente ao modelo simbólico, a abordagem garante que escrever a implementação do protocolo em AutoTam resulte, em grande parte, em um modelo "pronto para verificação" gratuitamente. A propriedade de sonoridade é central para essa afirmação, pois ela faz a ponte entre a verificação abstrata e a execução concreta, permitindo que desenvolvedores confiem em provas formais para a segurança da implementação. Além disso, a integração da execução simbólica fornece uma camada dupla de garantia: verificação formal da lógica do protocolo e detecção automatizada de erros de implementação de memória. Os autores posicionam isso como um passo significativo para melhorar a adoção de métodos formais na indústria, reduzindo a barreira de expertise e garantindo que o modelo verificado reflita fielmente o código em execução.