Resumo Técnico: Análise Quiral de Smart Contracts

1. Definição do Problema

As vulnerabilidades de smart contracts frequentemente derivam não de instruções inseguras isoladas, mas de inconsistências relacionais entre caminhos de negócio que são semanticamente pareados, mas sintaticamente distintos. Exemplos comuns incluem discrepâncias entre:

• Pontos de entrada únicos vs. em lote (batch).
• Fluxos diretos vs. baseados em adaptadores.
• Caminhos de cotação (preview) vs. execução.
• Operações inversas (ex: compra vs. venda, cunhagem vs. queima).

Analisadores estáticos existentes são excelentes na detecção de padrões sintáticos locais, dependências de estilo taint e vulnerabilidades de função única (ex: reentrância, chamadas não verificadas). No entanto, eles carecem de um "oráculo" para bugs relacionais: não conseguem determinar se dois caminhos correspondentes preservam os mesmos guardas, transições de estado, fluxos de valor ou comportamentos de falha. Esses bugs frequentemente exigem a comparação da lógica de um wrapper contra uma função principal, ou de um despachante de lote contra um caminho de operação única, para serem detectados.

2. Metodologia: Análise Quiral

O artigo introduz a análise quiral, um modelo relacional que trata caminhos de negócio semanticamente pareados como especificações implícitas uns para os outros. O termo "quiral" captura operações que são espelhadas, alternativas ou relacionadas ao ciclo de vida (ex: único/lote, wrapper/core) sem exigir identidade sintática.

2.1 O Modelo de Vulnerabilidade Quiral

Os autores formalizam uma relação quiral ($R_\chi$) como um análogo estático de uma relação metamórfica. Ela consiste em dois caminhos ($p, q$), um tipo de relação ($\tau$) e um conjunto de obrigações induzidas pela relação. Estas obrigações são aproximações de comportamentos esperados através de sete dimensões semânticas:

1. Guarda (Guard): Modificadores, precondições e verificações de elegibilidade.
2. Ator (Actor): Identidades de chamadores, signatários, pagadores e destinatários de reembolso.
3. Estado (State): Conjuntos de leitura/escrita, flags, contadores e deltas de estado.
4. Valor (Value): Unidades, taxas, recompensas, transferências e manipulação de reembolsos.
5. Ordem (Order): Sequências de check-effect-interaction e tempo de liquidação.
6. Falha (Failure): Comportamento de reversão (revert), semântica de sucesso parcial e emissão de eventos.
7. Externo (External): Uso de oráculos, callbacks e dependências entre contratos.

Uma vulnerabilidade quiral é definida como uma violação de tal obrigação que resulta em um impacto de segurança ou de protocolo viável (ex: perda de fundos, mudança de estado não autorizada ou erros de contabilidade).

2.2 O Pipeline ChiralDetector

Os autores implementam este modelo no ChiralDetector, um pipeline de quatro estágios projetado para equilibrar recall com precisidade enquanto gerencia os custos de Large Language Models (LLMs):

1. Extração de Caminho e Sumarização:

   • Constrói um grafo de chamadas ao nível do projeto a partir do código-fonte Solidity.
   • Extrai "caminhos de negócio" (funções únicas, cadeias de entrada-até-a-folha e segmentos de bifurcação).
   • Gera um resumo de fatos semânticos ($\Phi(p)$) para cada caminho, capturando leituras/escritas de armazenamento, transferências de valor, modificadores e chamadas externas. Esta abstração é intencionalmente perdedora de informação (lossy), mas orientada à relação.

2. Redução de Pares Candidatos:

   • Evita comparações exaustivas $O(n^2)$ usando um classificador estático (ranker).
   • Pontua pares de caminhos com base em pegadas de armazenamento compartilhadas, chamadas externas sobrepostas, pistas de nomenclatura (ex: "claim" vs. "batchClaim") e similaridades de ator/fluxo de valor.
   • Prioriza pares que provavelmente formam uma relação quiral sem deletar sinais de alto recall que sejam incertos.

3. Filtragem Semântica e Detecção (Baseada em LLM):

   • Filtro Semântico: Determina se um par forma plausivelmente uma relação quiral e atribui um tipo de relação (ex: inversa, wrapper/core). É instruído a aceitar pares com comprimentos de caminho diferentes ou direções econômicas opostas.
   • Detector Consciente da Relação: Dado uma relação confirmada, o LLM identifica obrigações específicas violadas, fornece evidência de origem e formula uma tese de impacto. Os prompts são estruturados como "contratos" para forçar o raciocínio explícito em vez de conclusões vagas.

4. Validação Estrita e Deduplicação:

   • Um validador estrito tenta falsificar as descobertas verificando se a relação é justificada, se existe evidência e se caminhos de código alternativos invalidam o impacto.
   • A deduplicação de causa raiz mescla múltiplos relatórios que compartilham o mesmo defeito subjacente e provável correção, distinguindo entre ruído de nível de par e problemas de nível de raiz.

3. Principais Contribuições

• Modelo de Análise Quiral: Um framework de vulnerabilidade relacional que trata caminhos de negócio correspondentes como especificações implícitas, indo além da análise de função única.
• Formalização: Definição de relações quirais como análogos metamórficos estáticos e a derivação de sete dimensões de obrigações específicas.
• Implementação do ChiralDetector: Um pipeline de protótipo integrando análise estática, classificação de pares estática, detecção semântica baseada em LLM, validação de falsificação estrita e deduplicação de causa raiz.
• Evidência Empírica: Uma avaliação preliminar no protocolo Phi demonstrando a detecção de inconsistências de lógica de negócio que são difíceis de expressar como regras de função única.

4. Resultados da Avaliação

Os autores avaliaram o ChiralDetector no protocolo Phi, um projeto Solidity contendo diversas formas de relação (claim/batch, adapter/factory, quote/execution).

• Métricas de Funil:

  • Começou com 3.217 pares candidatos classificados estaticamente.
  • Reduziu para 1.643 pares para detecção semântica.
  • Produziu 201 achados limpos/candidatos suspeitos.
  • Colapsou para 101 grupos de deduplicação local.
  • 44 grupos sobreviveram à validação estrita.
  • A deduplicação manual de causa raiz final resultou em 13 questões únicas eficazes.

• Achados Representativos:

  • M10: Reuso de prova de Merkle entre artes distintas (Violação de fluxo/guarda semelhante).
  • M13: Incompatibilidade de unidade de taxa (pontos base vs. wei) (Violação de valor/unidade).
  • M12: Auxiliares de rastreamento público corrompendo o estado do curador (Violação de estado/acesso).
  • M05/M02/M04: Lacunas de propagação de reembolso e assimetrias de guarda entre caminhos únicos e de lote (Violações de fluxo de valor de wrapper/core e single/batch).

• Análise de Custo:

  • A execução completa custou aproximadamente 212,70 CNY (excluindo tempo humano).
  • O custo dominante foi a inferência de LLM (filtragem semântica, detecção e validação), não a análise estática.
  • O validador estrito reduziu significativamente o ruído, rejeitando 57 dos 101 grupos de deduplicação local.

5. Significância e Alegações

O artigo afirma que a análise quiral expõe uma classe de bugs — inconsistências relacionais — que são naturalmente difíceis de expressar como regras de função única, mas que são críticas para a segurança do protocolo.

• Insight: Muitos bugs de lógica de negócio existem porque dois caminhos relacionados discordam sobre como lidar com um objeto de negócio compartilhado (ex: um destinatário de reembolso ou um cálculo de taxa), em vez de uma função ser localmente insegura.
• Uso Estruturado de LLM: O artigo argumenta que usar LLMs dentro de um pipeline estruturado (redução estática $\to$ filtragem semântica $\to$ validação estrita) é mais eficaz e econômico do que "auditoria de agente direta" (leitura irrestrita de código). O pipeline externaliza decisões intermediárias (pares, relações, obrigações), tornando a análise inspecionável e depurável.
• Modéstia: Os autores declaram explicitamente que a avaliação atual é um estudo de caso preliminar em um único protocolo. Eles não alegam ter estabelecido métricas de recall ou precisão geral ainda. Eles reconhecem limitações, incluindo a aproximação da semântica Solidity na extração de caminhos, o potencial de alucinações de LLM e a falta de geração automatizada de testemunhas (transações de prova de conceito executáveis).

O trabalho posiciona-se como um passo para tornar o raciocínio de lógica de negócio explícito e repetível na auditoria de smart contracts, oferecendo um vocabulário para descrever por que inconsistências específicas importam.