💻 ciência da computação

State-inferer: LLM-Driven State Machine Extraction and Formal Verification for Secure Protocol Implementations

Este artigo introduz o State-inferer, um framework de caixa-branca que integra fatiamento de programa, grandes modelos de linguagem e verificação de modelos formais para extrair e verificar com precisão máquinas de estado de protocolos a partir de código-fonte, alcançando uma precisão de nível de transição superior e revelando quatro vulnerabilidades de segurança anteriormente desconhecidas em implementações de TLS, IKEv2 e SSH.

Autores originais: MengCheng Ju, Xi Chen, XieLi Zhang, Mingliang Zhu, Guanping Zhang, Dongliang Zhao, ChunXiang Gu

Publicado 2026-11-09

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: MengCheng Ju, Xi Chen, XieLi Zhang, Mingliang Zhu, Guanping Zhang, Dongliang Zhao, ChunXiang Gu

Artigo original sob licença CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

A segurança do mundo digital depende fortemente das regras invisíveis que governam como os computadores conversam entre si. Essas regras, conhecidas como protocolos de rede, são projetadas para garantir que os dados viajem com segurança de um remetente a um receptor, verificando identidades e mantendo segredos. Em seu cerne, esses protocolos funcionam como um roteiro rigoroso: um computador deve estar em uma condição específica, receber uma mensagem específica e, então, mover-se para uma nova condição antes de poder prosseguir. Se um computador pular uma etapa ou aceitar uma mensagem enquanto estiver na condição errada, todo o sistema pode ser comprometido, permitindo que invasores contornem verificações de segurança ou roubem informações confidenciais. Por décadas, especialistas em segurança tentaram verificar se o código real executado nos servidores segue esse roteiro perfeitamente. No entanto, o código é frequentemente desordenado, repleto de variáveis ocultas e lógica complexa que ferramentas de teste padrão têm dificuldade em mapear. Quando o comportamento real de um programa diverge de seu design escrito, falhas perigosas podem se esconder à vista de todos, esperando para serem exploradas.

Uma equipe de pesquisadores da Universidade de Engenharia de Informação da PLA desenvolveu um novo método para resolver este problema, criando uma ferramenta chamada State-inferer, que atua como um tradutor entre o código de computador complexo e as regras lógicas que ele deveria seguir. Em vez de tentar ler todo o código-fonte de uma só vez ou adivinhar como um programa se comporta enviando mensagens aleatórias, esta ferramenta decompõe o código em partes minúsculas e gerenciáveis. Ela utiliza uma técnica chamada fatiamento de programa (program slicing) para rastrear exatamente como um pedaço específico de dados muda conforme se move pelo software, isolando a lógica precisa que faz um computador mudar de estado para outro. Este processo é como rastrear um único fio através de um novelo de lã emaranhado para ver exatamente onde ele leva, ignorando o resto da bagunça. Ao focar nesses fios específicos, o sistema pode reconstruir a sequência exata de eventos que um programa segue, incluindo as condições internas ocultas que as ferramentas padrão costumam perder.

Os pesquisadores então alimentaram essas sequências reconstruídas em um grande modelo de linguagem, um tipo de inteligência artificial treinada para compreender e raciocinar sobre código. Diferente de tentativas anteriores que simplesmente pediam à IA para ler grandes blocos de texto, este sistema forneceu à IA um fragmento de código pequeno e focado para cada uma das transições do protocolo. Isso permitiu que a IA visse o contexto completo de uma mudança de estado sem ficar sobrecarregada por informações irrelevantes. A IA então construiu um mapa completo do comportamento do programa, anotando não apenas quais mensagens dispararam uma mudança, mas também as variáveis internas que precisavam ser verdadeiras para que essa mudança ocorresse. Finalmente, os pesquisadores usaram um mecanismo de verificação formal para checar este mapa contra as regras de segurança oficiais. Este mecanismo atua como um auditor rigoroso, testando sistematicamente cada caminho possível que o programa pode seguir para ver se ele algum dia viola as regras, como enviar dados antes que uma conexão segura seja totalmente estabelecida.

Quando testado em sete implementações de código aberto de diferentes protocolos de segurança importantes, incluindo TLS, IKEv2 e SSH, o novo método provou ser notavelmente preciso. Ele identificou corretamente o comportamento do código com uma precisão de 95,2 por cento, superando significativamente as melhores ferramentas existentes, que alcançavam apenas cerca de 78,9 por cento. A diferença não foi apenas uma questão de erros menores; a nova ferramenta capturou com sucesso lógicas internas complexas que outros métodos perderam completamente, como transições impulsionadas por temporizadores internos ou verificações de recursos, em vez de mensagens externas. De fato, os pesquisadores descobriram que os métodos mais antigos frequentemente falhavam em ver quase metade das transições críticas porque dependiam de uma visão simplificada do programa que ignorava esses detalhes internos. Ao capturar o quadro completo, a nova ferramenta foi capaz de descobrir quatro vulnerabilidades anteriormente desconhecidas no software. Estas falhas, que nunca haviam sido descobertas antes, eram sérias o suficiente para receberem identificadores de segurança oficiais e serem reportadas aos mantenedores do software para correção.

Uma das descobertas mais significativas foi que as falhas não eram apenas possibilidades teóricas, mas fraquezas reais e exploráveis. Em um caso, a ferramenta descobriu que um servidor poderia ser enganado para aceitar uma mensagem de segurança crítica antes de ter terminado a troca de chaves necessária, efetivamente contornando a autenticação. Em outro caso, uma verificação ausente permitiu que um servidor processasse um fluxo interminável de mensagens, potencialmente esgotando seus recursos. Essas descobertas destacam uma lacuna crítica na forma como o software é analisado atualmente: olhar apenas para a entrada e a saída não é suficiente para entender como um programa realmente funciona. Os pesquisadores demonstraram que, ao combinar a análise de código precisa com o poder de raciocínio da inteligência artificial, é possível construir um modelo completo e preciso da lógica interna de um programa. Esta abordagem não requer que o software seja modificado ou que os pesquisadores rastreiem manualmente cada linha de código, tornando-a uma forma escalável de auditar os sistemas complexos que protegem nossa infraestrutura digital.

O estudo também abordou as limitações de abordagens anteriores que dependiam da recuperação de código baseada em similaridade de texto. Esses métodos frequentemente falhavam porque não conseguiam conectar os pontos entre diferentes funções que trabalhavam juntas para alterar o estado de um programa. O novo sistema, por outro via inversa, segue o fluxo real de dados e controle, garantindo que o contexto fornecido à inteligência artificial seja completo e conectado. Isso permitiu que o sistema gerasse verificações de segurança que foram adaptadas especificamente para as variáveis e a lógica de cada implementação única, em vez de aplicar um modelo genérico que poderia perder o alvo. O resultado é uma estrutura que pode se adaptar às peculiaridades de diferentes estilos de codificação e ainda assim produzir um modelo confiável do comportamento do sistema.

Em última análise, este trabalho representa uma mudança na forma como abordamos a segurança do software. Ele se afasta da ideia de que devemos ou inspecionar manualmente cada linha de código ou confiar em testes de caixa preta que podem ver apenas a superfície. Em vez disso, oferece uma maneira de olhar dentro da máquina, entendendo exatamente como ela pensa e reage. Os pesquisadores descobriram que, ao tratar o código como um conjunto de etapas lógicas que podem ser fatiadas, analisadas e verificadas, eles podiam encontrar erros que estavam escondidos há anos. Embora a ferramenta tenha sido testada em projetos de código aberto, o método sugere um caminho a seguir para proteger a vasta gama de sistemas proprietários que operam a internet. A capacidade de extrair e verificar automaticamente as máquinas de estado de protocolos complexos significa que a segurança pode ser verificada de forma mais minuciosa e rápida do que nunca, potencialmente prevenindo os tipos de brechas que assolam o mundo digital há décadas. As descobertas confirmam que a lacuna entre o que um protocolo deveria fazer e o que ele realmente faz é onde reside o perigo, e que fechar essa lacuna exige um olhar mais profundo e preciso sobre o próprio código.

Resumo Técnico: State-inferer

Declaração do Problema

A segurança das implementações de protocolos de rede depende da correção das máquinas de estados finitos (FSMs) realizadas pelo código. No entanto, as implementações do mundo real frequentemente se desviam de suas especificações RFC devido a requisitos mal interpretados ou lógica específica de fornecedores, levando a vulnerabilidades de máquina de estados, como a evasão de autenticação. Recuperar a FSM real a partir do código-fonte é desafiador devido a três limitações primárias nas abordagens existentes:

Desalinhamento Semântico (C1): Os métodos existentes frequentemente constroem máquinas de estados orientadas por mensagens que abstraem detalhes internos de implementação. Os estados reais dos protocolos dependem de variáveis internas (ex: flags, contadores) e condições de fluxo de controle que, quando ignorados, resultam em modelos grosseiros que não conseguem expressar comportamentos de nível de implementação necessários para a verificação.
Restrições de Contexto (C2): Bases de código de protocolos são grandes demais para as janelas de contexto dos Grandes Modelos de Linguagem (LLMs) atuais. Abordagens de Geração Aumentada de Recuperação (RAG) tipicamente dependem de similaridade textual, o que falha em recuperar as cadeias de chamadas completas entre funções e arquivos necessárias para entender uma transição de estado como uma unidade unificada. Isso leva a precondições ausentes e análise de alcançabilidade incorreta.
Especialização de Propriedades (C3): As propriedades de segurança de RFCs são declaradas em um nível semântico sem referência a variáveis de implementação específicas. Traduzir essas propriedades genéricas em fórmulas de Lógica Temporal Linear (LTL) para verificação de modelos requer o mapeamento de conceitos abstratos para variáveis de código específicas, um passo que as ferramentas existentes deixam para a intervenção manual do analista.

Metodologia: State-inferer

O State-inferer é um framework de caixa branca projetado para extrair e verificar máquinas de estado de protocolos combinando o fatiamento de programas (program slicing), LLMs e verificação de modelos. Sua arquitetura consiste em três componentes principais:

1. Extrator de Código Relacionado (RCE)

Para abordar a restrição de contexto (C2) e evitar alucinações causadas por código irrelevante, o RCE não utiliza recuperação baseada em similaridade. Em vez disso, ele emprega fatiamento de programa (program slicing) no Grafo de Dependência de Sistema (SDG).

Identificação de Variáveis de Estado: Um LLM é instruído a identificar variáveis de estado chave e seus valores de enumeração a partir de arquivos de cabeçalho e fontes principais.
Fatiamento com Limite de Profundidade: Partindo de atribuições às variáveis de estado, o sistema realiza buscas para frente e para trás no SDG limitadas pela profundidade de fluxo de dados ( $k_d$ ) e fluxo de controle ( $k_c$ ). Isso extrai um fragmento de código compacto ("gadget") para cada transição de estado que abrange fronteiras de funções, mas exclui código de baixo nível não relacionado. Isso garante que o LLM receba a cadeia de chamadas completa e as precondições para uma transição.

2. Construtor de Modelo

Este componente transforma os fragmentos de código fatiados em um Sistema de Transição de Estados (STS) formal, $M = (V, S, s_0, \delta, A)$ .

Espaço de Estados ( $S$ ) e Estado Inicial ( $s_0$ ): O LLM extrai o espaço de estados discretos a partir de tipos de enumeração e infere as constantes do estado inicial com base em rotinas de inicialização.
Função de Transição ( $\delta$ ) e Variáveis ( $V$ ): Para cada gadget de código, o LLM identifica os estados de origem e destino, extrai condições de fluxo de controle e as traduz em expressões booleanas formais. Ele também coleta as variáveis internas envolvidas.
Conjunto de Ações ( $A$ ): As transições são rotuladas com ações externas (ex: recebimento de mensagem) e ações internas (ex: expiração de timer, derivação de chave).
Saída: O resultado é um STS onde as transições carregam guardas explícitas sobre variáveis internas, abordando o desalinhamento semântico (C1).

3. Gerador de Propriedades de Segurança

Para resolver o problema da especialização de propriedades (C3), este módulo converte meta-propriedades de RFC em fórmulas LTL específicas de implementação.

O LLM recebe o STS extraído e uma propriedade de segurança de RFC como entrada.
Ele mapeia conceitos de segurança abstratos para as variáveis de estado e predicados de transição da implementação específica.
Ele gera a fórmula LTL correspondente adaptada ao código-fonte.

4. Verificação

O STS extraído e as propriedades LTL são traduzidos para a linguagem SMV e verificados usando nuXmv. Se uma propriedade for violada, o nuXmv gera um rastro de contraexemplo, que é revisado manualmente para identificar vulnerabilidades.

Contribuições Principais

Construção de Contexto Baseada em Fatiamento: Um método para recuperar transições de estado de protocolo realizando buscas para frente e para trás limitadas por profundidade no SDG. Isso extrai um fragmento de código compacto por transição, garantindo que o LLM veja a lógica completa entre funções em vez de apenas trechos isolados.
Sistema de Transição de Estados com Guardas: Um pipeline que constrói um STS de nível de implementação onde as transições carregam guardas sobre variáveis internas, permitindo a modelagem de comportamentos que dependem de configurações internas em vez de apenas mensagens externas.
Especialização de Propriedade Consciente do Modelo: Uma abordagem automatizada para especializar propriedades de RFC em fórmulas LTL sobre o modelo extraído, preenchendo a lacuna entre a semântica da especificação e as variáveis da implementação.
Avaliação Empírica: Uma avaliação abrangente em sete implementações de código aberto de TLS, IKEv2 e SSH, demonstrando alta precisão na recuperação de transições e na descoberta de vulnerabilidades anteriormente desconhecidas.

Resultados

O framework foi avaliado em sete implementações (OpenSSL, WolfSSL, TLSE, strongSwan, Libreswan, OpenSSH, tinySSH) contra um modelo de referência construído por especialistas do domínio.

Precisão: O State-inferer alcançou um F-score macro-médio estrito ao nível de transição de 95,2%. Isso superou significativamente o baseline mais forte, ProtocolGPT (46,2%), e agentes de codificação de propósito geral (Codex: 78,9%, Claude Code: 77,1%).
Poder de Representação: Diferente das representações estilo Mealy usadas pelos baselines, o STS do State-inferer pôde expressar todas as transições de referência. Métodos baseline perderam aproximadamente 22% das transições devido a limitações de representação (ex: incapacidade de distinguir estados baseados em guardas internas ou eventos internos).
Descoberta de Vulnerabilidades: O State-inferer descobriu quatro vulnerabilidades anteriormente desconhecidas em implementações não modificadas:
1. WolfSSL (CVE-2026-2645): Uma evasão de autenticação em TLS 1.2 onde uma mensagem CertificateVerify pode ser processada antes da conclusão da troca de chaves.
2. TLSE (CNVD-2026-27960): Uma confusão de versão de protocolo causada por extensões de compartilhamento de chave vazias em TLS 1.3.
3. TLSE (CNVD-2026-27959): Processamento ilimitado de mensagens ChangeCipherSpec devido a uma variável de estado ausente.
4. TLSE (CNVD-2026-27957): Dessincronização entre o tratamento de alertas TLS e o estado da camada de transporte, permitindo a transmissão de dados após uma notificação de fechamento.
  Todos os achados foram divulgados de forma responsável e receberam identificadores CVE ou CNVD.

Significância e Alegações

O artigo afirma que o State-inferer aborda as limitações fundamentais dos métodos atuais de extração de máquinas de estado ao integrar análise estática (fatiamento) com as capacidades de raciocínio de LLMs. Ao construir o contexto por meio de fatiamento de dependência em vez de recuperação textual, o framework garante que o LLM receba a lógica necessária entre funções para inferir com precisão as guardas de transição e a alcançabilidade. Além disso, ao automatizar a especialização de propriedades de RFC em fórmulas LTL, ele permite a verificação formal de propriedades de segurança específicas de implementação sem mapeamento manual.

Os autores afirmam que sua abordagem fornece uma representação mais fiel do comportamento de nível de implementação em comparação com o aprendizado de caixa-preta ou modelagem baseada em especificação, permitindo diretamente a descoberta de vulnerabilidades que dependem de configurações de estado interno. O alto F-score e a descoberta bem-sucedida de vulnerabilidades do mundo real demonstram a eficácia prática da combinação de fatiamento de programa, LLMs e verificação de modelos para a análise segura de protocolos.