💻 computer science

CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes

Este artigo apresenta o CrypFormBench, um benchmark abrangente composto por 700 instâncias em 677 esquemas criptográficos e 7 linguagens de verificação formal, para avaliar e revelar as limitações atuais dos grandes modelos de linguagem na geração e correção de provas de segurança formais, ao mesmo tempo em que oferece estratégias práticas para melhorar seu desempenho.

Autores originais: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

Publicado 2026-06-25

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Zhaoxuan Li, Qionglu Zhang, Hengyuan Liu, Xiaoyan Gu, Xianhui Lu, Hongbo Liu, Bingzheng Wang, Haihui Fan, Ziming Zhao, Rui Zhang, Li Zhou

Artigo original sob licença CC BY 4.0 (http://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

O Panorama Geral: O Problema do "Tradutor"

Imagine que você é um mestre arquiteto que projeta cofres incrivelmente seguros (esquemas criptográficos). Você escreve seus projetos em inglês simples para que qualquer pessoa possa entender o plano. No entanto, para realmente construir e testar esses cofres em busca de vulnerabilidades, você precisa traduzir esses projetos em inglês para uma linguagem muito rigorosa, antiga e complexa que apenas robôs de segurança específicos e de alta tecnologia (ferramentas de verificação formal como Scyther ou Tamarin) conseguem entender.

Essa tradução é difícil. Requer um especialista humano que conheça tanto o design do cofre quanto a linguagem rigorosa do robô. Se você errar uma única vírgula ou usar a palavra errada, o robô rejeita o projeto ou, pior, constrói um cofre que parece seguro, mas possui uma porta dos fundos (backdoor) oculta.

A Pergunta: Os Modelos de Linguagem de Grande Escala (LLMs) — os chatbots de IA que usamos hoje — podem atuar como esses tradutores especialistas? Eles conseguem pegar uma descrição em inglês simples de um protocolo de segurança e escrever instantaneamente o código perfeito e livre de erros para os robôs de segurança?

A Resposta (segundo este artigo): Ainda não exatamente. Eles estão melhorando na leitura e na correção, mas ainda têm dificuldades para escrever do zero.

A Solução: CrypFormBench (A "Academia" para a IA)

Para descobrir exatamente o quão bons esses tradutores de IA são, os pesquisadores construíram um enorme campo de testes chamado CrypFormBench (ou C.F.B.).

Pense nisso como uma academia com 700 diferentes estações de treino.

O Equipamento: Eles reuniram 700 protocolos de segurança do mundo real (como os usados no seu telefone, banco ou na internet).
As Linguagens: Eles traduziram esses protocolos para 7 "linguagens de robô" diferentes (linguagens formais como SPDL, HLPSL, EasyCrypt, etc.).
Os Testes: Eles não apenas pediram para a IA escrever código. Eles testaram cinco habilidades específicas:
1. Interpretação: "Aqui está um código de robô; explique-o para mim em inglês." (Leitura)
2. Geração: "Aqui está uma descrição em inglês; escreva o código do robô." (Escrita do zero)
3. Preenchimento (Completion): "Aqui está um código de robô com lacunas; preencha os espaços em branco." (Corrigindo trabalho parcial)
4. Transformação: "Aqui está o código na Linguagem A; reescreva-o na Linguagem B." (Traduzindo entre robôs)
5. Correção: "Este código de robô tem um erro; corrija-o." (Depuração/Debugging)

Os Resultados: O Boletim da IA

Os pesquisadores testaram 9 dos modelos de IA mais inteligentes disponíveis (incluindo GPT-4o, Claude-3.5 e DeepSeek). Aqui está o que descobriram:

1. A Habilidade de "Saber Ler" (Interpretação e Preenchimento)

Analogia: Imagine um aluno que é ótimo em ler um livro didático e consegue preencher as palavras que faltam em uma frase porque o contexto já está lá.
Resultado: As IAs foram surpreendentemente boas nisso. Quando recebiam um trecho de código com algumas partes faltando, ou quando lhes era pedido para explicar o que uma parte do código faz, elas tiveram um desempenho muito bom. Elas entendiam a "gramática" das linguagens de segurança.

2. A Habilidade de "Saber Escrever" (Geração e Transformação)

Analogia: Agora imagine pedir a esse mesmo aluno para escrever um livro didático inteiro do zero, ou traduzir um livro do francês para o japonês sem um dicionário. Eles começam a alucinar, inventar regras ou esquecer a gramática rigorosa.
Resultado: Foi aqui que as IAs falharam.
- Geração: Quando solicitadas a escrever um protocolo de segurança completo a partir de uma descrição em inglês simples, a maioria das IAs produziu códigos que os robôs sequer consegam executar. Era como escrever uma frase com sintaxe quebrada.
- Transformação: Quando solicitadas a traduzir um código de uma linguagem de robô para outra, as IAs frequentemente se confundiam. Elas misturavam as regras das duas linguagens, criando um código "Frankenstein" que não funcionava em nenhuma delas.
- A Pontuação: Mesmo a melhor IA (Claude-3.5) obteve apenas 48,7 de 100. Isso significa que menos da metade de suas tentativas eram realmente utilizáveis pelas ferramentas de segurança.

3. A Habilidade de "Corrigir" (Correção)

Analogia: Se você der ao aluno uma frase com um erro de digitação óbvio (ex: "receiv" em vez de "receber"), ele pode corrigir facilmente. Mas se a frase estiver gramaticalmente correta, porém logicamente errada (ex: "O cofre está aberto para todos, mas é seguro"), eles têm dificuldade em encontrar o erro de lógica.
Resultado: As IAs foram boas em corrigir erros simples de sintaxe (erros de digitação). No entanto, elas tiveram dificuldades com erros "semânticos" — corrigindo a própria lógica do protocolo de segurança.

Por que isso é tão difícil?

O artigo explica que essas "linguagens de robô" não são como Python ou Java. Elas são extremamente rigorosas.

A Regra do "Um Erro": Na programação normal, se você esquece um ponto e vírgula, o computador pode apenas reclamar. Nessas linguagens de segurança, uma palavra faltando pode mudar todo o significado da prova de segurança, fazendo um cofre seguro parecer inseguro, ou vice-versa.
O Problema do "Contexto": Esses protocolos geralmente dependem de longas cadeias de eventos (ex: "Se Alice envia uma mensagem no passo 1, Bob deve responder no passo 2, mas apenas se ele não tiver visto uma mensagem do passo 0"). As IAs costam perder o rastro dessas longas cadeias.

O Que Podemos Fazer? (As "Rodinhas de Treino")

O artigo sugere que, embora não possamos confiar nas IAs para fazer todo o trabalho sozinhas ainda, podemos usá-las como assistentes se dermos a elas a ajuda certa:

Few-Shot Prompting: Em vez de apenas dizer "Escreva isso", mostre à IA três exemplos de como escrever aquilo primeiro. Isso funciona como uma "cola".
Pass@K: Peça para a IA tentar escrever o código 5 vezes e, então, escolha a melhor versão. Isso aumenta as chances de obter uma versão funcional.
Human-in-the-Loop (Humano no Ciclo): Use a IA para redigir o código, mas tenha um especialista humano para verificá-lo antes que o robô de segurança o execute.

A Conclusão Final

O artigo conclui que os Modelos de Linguagem de Grande Escala são atualmente excelentes assistentes de pesquisa para entender e corrigir códigos de segurança, mas ainda não são arquitetos confiáveis para construir novos protocolos de segurança do zero.

Elas podem ajudar você a ler o manual e corrigir seus erros de digitação, mas você ainda precisa de um especialista humano para garantir que o cofre seja realmente seguro antes de entregar as chaves. O benchmark (CrypFormBench) está agora disponível para que outros pesquisadores testem novos modelos de IA contra esses mesmos padrões rigorosos.

Resumo Técnico: CrypFormBench

1. Definição do Problema

A análise formal manual de esquemas criptográficos é laboriosa, exigindo profunda expertise tanto em criptografia quanto em linguagens de especificação formal. Embora ferramentas automatizadas como Scyther, Tamarin, CryptoVerif e EasyCrypt existam, elas ainda dependem de especialistas para abstrair a lógica do esquema em linguagens formais especializadas e propensas a erros (ex: HLPSL, SPDL, $\pi$ -cálculo aplicado). Modelos de Linguagem de Grande Escala (LLMs) oferecem uma solução potencial para automatizar a derivação de especificações formais a partir de linguagem natural. No entanto, sua eficácia neste domínio permanece inexplorada devido à ausência de metodologias de avaliação padronizadas.

Benchmarks existentes são insuficientes porque frequentemente:

Suportam apenas segurança simbólica, negligenciando a segurança computacional.
Cobrem escalas limitadas (ex: ~18 protocolos) e excluem diversos modelos de ameaça ou primitivas avançadas (ex: Conhecimento Zero, Pós-Quântica).
Carecem de um framework unificado para avaliar LLMs através de múltiplas linguagens de verificadores formais e tipos de tarefas (geração, transformação, correção).

2. Metodologia: CrypFormBench (C.F.B)

Os autores introduzem o CrypFormBench, um benchmark abrangente projetado para avaliar as capacidades de LLMs na análise criptográfica formal. A metodologia envolve três componentes principais:

A. Construção do Dataset

Escala e Diversidade: O dataset compreende 700 instâncias curadas derivadas de 4.549 projetos de código aberto e datasets de ferramentas. Estas instâncias cobrem 677 esquemas criptográficos distintos (variando de autenticação clássica a designs modernos de MPC, ZK e pós-quânticos) e 160 propriedades de segurança.
Cobertura de Linguagem: Abrange 7 linguagens de verificadores formais predominantes associadas a ferramentas incluindo Scyther (SPDL), Tamarin (SPTHY), AVISPA (HLPSL), ProVerif (PV/HORN), Maude-NPA (MAUDE), CryptoVerif (CV/OCV) e EasyCrypt (EC).
Modelos Adversários: O dataset inclui diversos pressupostos de adversários, desde modelos passivos/ativos Dolev-Yao até modelos estendidos (CK, eCK) e ameaças de domínio específico (ex: tentativa de adivinhação de senha em IoT).
Controle de Qualidade: Um pipeline rigoroso foi empregado envolvendo deduplicação, verificações de executabilidade e verificação manual. As instâncias foram rotuladas como "seguras" (sem ataques conhecidos) ou "inseguras" (ataques conhecidos), com os outputs das ferramentas alinhados contra rótulos canônicos da literatura criptográfica.

B. Definição de Tarefa

O benchmark avalia cinco capacidades essenciais de LLM para especificações formais utilizáveis por ferramentas:

Interpretação: Gerar comentários de nível de notação e resumos globais de esquemas a partir de código formal.
Geração: Criar código formal completo a partir de descrições de lógica em linguagem natural.
Completamento: Preencher fragmentos ausentes de especificações formais parcialmente mascaradas.
Transformação: Traduzir especificações de esquemas de uma linguagem formal para outra preservando a semântica.
Correção: Reparar códigos que falham na compilação (erros de sintaxe) ou produzem resultados de verificação incorretos (erros semânticos).

C. Pipeline de Avaliação

Verificação Automatizada: Um pipeline de ponta a ponta integra múltiplas ferramentas, versões e comandos de execução para verificar os outputs dos LLMs. Ele lida com comportamentos de chamada variáveis (ex: múltiplos backends para AVISPA) e incompatibilidades de versão.
Framework de Pontuação: O desempenho é medido via um sistema de pontuação ponderada equilibrando:
- Executabilidade (Analisabilidade): Se o código compila e executa.
- Corretude Funcional: Se as propriedades de segurança verificadas coincidem com a verdade fundamental (SAFE/UNSAFE), medido por Acurácia ( $ACC_A$ ) e F1 ( $F1_A$ ).
- Similaridade: Similaridade de código para tarefas de completamento e similaridade semântica (via embeddings) para tarefas de interpretação.
- Eficiência: Tempo de execução e tamanho do arquivo.

3. Resultados Principais

Os autores avaliaram 9 LLMs de última geração (incluindo GPT-4o, Claude-3.5-Sonnet-Coder, DeepSeek-Coder e LLaMA4-Instruct).

Desempenho Geral: O desempenho é geralmente limitado. O modelo de maior desempenho, Claude-3.5-Sonnet-Coder, alcançou uma pontuação geral de 48,7 de 100.
Insights Específicos por Tarefa:
- Pontos Fortes: Os modelos performam bem em Interpretação e Completamento, aproveitando sua consciência de código. Por exemplo, DeepSeek-Coder e GPT-4o mostram alta precisão ao interpretar código existente.
- Pontos Fracos: Modelos lutam significativamente com Geração, Transformação e Correção.
  - Geração: Mesmo os melhores modelos alcançam baixas razões de analisabilidade (ex: ~15% para Claude-3.5) e lutam com sintaxe/semântica estrita em linguagens complexas como EasyCrypt e Maude.
  - Transformação: Esta é a tarefa mais difícil. Interferências entre linguagens e incompatibilidades semânticas levam a uma analisabilidade muito baixa (frequentemente <10%), com modelos frequentemente copiando fragmentos da fonte que são incompatíveis com os idiomatismos da linguagem alvo.
  - Correção: Embora modelos possam corrigir erros de sintaxe localizados (guiados pelo compilador), eles lutam com reparos semânticos (ex: corrigir falsos relatórios de propriedades de segurança).
Variabilidade de Linguagem: O desempenho varia drasticamente por linguagem. Modelos geralmente performam melhor em ProVerif (PV) devido à sua similaridade com a sintaxe de programação mainstream, enquanto lutam com ferramentas baseadas em reescrita como Maude-NPA.
Estratégias de Otimização:
- Prompting Few-Shot: Melhora significativamente a analisabilidade para geração (de 6,6% para 24,9% com 3-shot) e a corretude para correção.
- Pass@K: Aumentar o número de tentativas de geração ( $K$ ) melhora a probabilidade de obter um output analisável, particularmente para tarefas difíceis, embora não garanta a corretude semântica.
- Fine-Tuning: O fine-tuning leve de LoRA no Qwen2.5-Coder-3B melhorou as capacidades de completamento e correção, mas teve impacto mínimo em geração ou transformação.

4. Significância e Alegações

O artigo afirma fornecer o primeiro benchmark abrangente que cobre conjuntamente segurança simbólica e computacional para avaliar LLMs na análise de esquemas criptográficos.

Visão Fundamentada: Os autores afirmam que, embora os LLMs sejam assistentes promissores para interpretação e correção localizada, eles ainda não são confiáveis para a automação de ponta a ponta da geração de esquemas formais ou transformação entre linguagens.
Identificação de Gargalos: A barreira primária não é apenas o raciocínio semântico, mas a executabilidade — a capacidade de produzir código que satisfaça a sintaxe formal estrita e as restrições específicas da ferramenta sem disparar timeouts ou erros de parsing.
Orientação Prática: O estudo oferece direções concretas para melhorar a análise assistida por LLM, incluindo o uso de prompting few-shot, amostragem Pass@K e fine-tuning leve para mitigar o gargalo da executabilidade.
Reprodutibilidade: O benchmark e o dataset são liberados para permitir a avaliação sistemática, padronizada e reproduzível de modelos futuros neste domínio.

Os autores concluem que os LLMs atuais servem como fortes ferramentas de "rascunho", mas requerem validação humana ou fluxos de trabalho de reparo guiados por ferramentas para serem praticamente úteis para a análise criptográfica formal.