Resumo Técnico: Análise Quantitativa de Impacto de Correção Simbólica

Declaração do Problema

A verificação de equivalência tradicional classifica programas como equivalentes ou não equivalentes. Essa classificação binária é insuficiente para a análise de impacto de correção, onde a versão corrigida é esperada ser não equivalente ao código original (vulnerável) para remediar uma vulnerabilidade. Embora a não equivalência seja esperada, o desafio crítico reside em determinar sob quais condições os programas diferem e qual porcentagem do domínio de entrada é afetada.

As abordagens atuais frequentemente falham em distinguir entre uma correção "boa" que corrige uma vulnerabilidade enquanto preserva a funcionalidade para a maioria das entradas, e uma correção "ruim" que restringe excessivamente as entradas (por exemplo, ao codificar valores seguros ou rejeitar todas as entradas), introduzindo assim não equivalência em uma porção significativamente maior do domínio de entrada. Há uma falta de técnicas para quantificar formalmente essa divergência comportamental.

Metodologia

Os autores propõem a Análise Quantitativa de Equivalência Parcial, um framework que refina a não equivalência medindo a extensão da divergência comportamental através do domínio de entrada. A metodologia consiste em três componentes principais:

1. Formalização da Equivalência Parcial

O artigo define um programa $P$ como uma função total de um domínio de entrada $D_{IP}$ para um domínio de saída $D_{OP}$. Dados dois programas $P_1$ (original) e $P_2$ (corrigido) com o mesmo domínio de entrada:

• Conjunto de Equivalência ($D_{eq}$): O conjunto de entradas onde $P_1(\vec{I}) = P_2(\vec{I})$.
• Conjunto de Não Equivalência ($D_{neq}$): O conjunto de entradas onde $P_1(\vec{I}) \neq P_2(\vec{I})$.
• Superfície de Impacto da Correção: Definida como $D_{neq}$. O objetivo é calcular a condição de equivalência ($F_{eq}$) e a porcentagem do domínio de entrada onde $D_{eq}$ se mantém.

2. Análise Simbólica e Sumarização

A abordagem utiliza execução simbólica estendida para gerar resumos simbólicos ($S_P$) para ambos os programas. Um resumo simbólico é uma fórmula lógica que representa a relação entre entradas e saídas para todos os caminhos de execução.

• Algoritmo 1 (EqChecker): Classifica programas como Equivalentes ($T_{eq}$), Totalmente Não Equivalentes ($T_{neq}$) ou Parcialmente Equivalentes ($P_{eq}$) verificando a satisfatibilidade de $S_1 \Leftrightarrow S_2$ e $S_1 \land S_2$.

3. Técnicas Quantitativas (Heurísticas de Busca por Intervalo)

Para quantificar eficientemente o tamanho de $D_{eq}$ e $D_{neq}$ em domínios numéricos, os autores propõem uma heurística de busca baseada em intervalos. Isso evita a intratabilidade computacional de enumerar todas as entradas ou usar contagem de modelos dispendiosa para grandes domínios.

• Busca por Intervalo Relacional (Algoritmo 2): Divide recursivamente o domínio de entrada em subdomínios (metade dos intervalos) e verifica equivalência ou não equivalência total dentro desses subdomínios. Captura condições relacionais entre múltiplas variáveis, mas possui complexidade exponencial $O((2^N)^{LIMIT})$.
• Busca por Intervalo Iterativa (Algoritmo 3): Processa um parâmetro de entrada por vez para melhorar a escalabilidade, reduzindo a complexidade para $O(N \times 2^{LIMIT})$. No entanto, não consegue capturar restrições relacionais entre variáveis.
• Busca por Intervalo Iterativa com Prioridade (Algoritmo 5): Divide domínios com prioridade em direção ao zero (partições negativa, zero, positiva), baseado na intuição de que programas são mais prováveis de serem equivalentes para valores absolutos menores.
• Busca por Intervalo Combinada (Algoritmo 6): Integra as abordagens Iterativa e com Prioridade, selecionando o melhor limite inferior de equivalência para cada parâmetro de entrada para fornecer uma análise robusta.

4. Comparações com Linha de Base

Os autores comparam sua abordagem de busca por intervalos com:

• Contagem de Modelos Enumerativa: Encontrar iterativamente soluções satisfatórias via solucionadores SMT.
• Projeção e Contagem de Modelos: Usar eliminação de quantificadores e ferramentas de contagem de modelos (SearchMC, Ganak, qCoral, ABC) para calcular porcentagens de equivalência.

Contribuições Principais

1. Formalização: O artigo formaliza o conceito de equivalência parcial e a superfície de impacto da correção, estendendo a análise de equivalência para incluir condições de equivalência/não equivalência e suas porcentagens correspondentes.
2. Desenvolvimento de Técnica: Propõe uma técnica baseada em busca por intervalos especificamente projetada para análise quantitativa eficiente de domínios de entrada numéricos, fornecendo um limite inferior sólido de equivalência.
3. Análise de Impacto de Correção: A técnica é aplicada para avaliar o impacto da correção, distinguindo entre correções que afetam minimamente o domínio de entrada (correções boas) e aquelas que restringem excessivamente as entradas (correções ruins).
4. Avaliação em Benchmarks: A abordagem é avaliada em:
   • PatchBench: 90 correções de CVE do Linux, Qemu e FFmpeg.
   • JulietBench: 50 programas com correções boas e ruins (incluindo correções ruins geradas por LLM).
   • EqBench: 47 programas C, onde a ferramenta identificou 5 casos rotulados incorretamente como "equivalentes" devido a estouro de inteiros.

Resultados Experimentais

• Diferenciação de Correções: No conjunto de dados JulietBench, correções ruins exibiram uma superfície de impacto média de 96,65%, enquanto correções boas afetaram apenas 29,03% do domínio de entrada.
• Variabilidade do Mundo Real: No PatchBench, 36,25% das correções foram não equivalentes para mais de 90% do domínio de entrada, enquanto 20% afetaram menos de 10%. Isso destaca uma variância significativa nos impactos de correção do mundo real.
• Precisão e Eficiência:
  • A abordagem de Busca por Intervalo Combinada alcançou 81,8% de precisão no PatchBench e 95,2% no EqBench ao produzir resultados de equivalência exata (com verdade fundamental conhecida), superando o próximo melhor método em 30,7%.
  • Fornecia uma aproximação mais próxima da verdade fundamental do que as abordagens de contagem de modelos, com um desvio médio aproximadamente 29,4% menor do que a segunda melhor abordagem.
  • Tempo de Execução: O RangeSearch executou aproximadamente 8x mais rápido que o SearchMC no PatchBench e 2x mais rápido no EqBench.
• Descobertas do EqBench: A análise identificou 5 casos no EqBench rotulados incorretamente como equivalentes; a ferramenta identificou corretamente que eram parcialmente equivalentes devido a condições de estouro de inteiros.

Significado e Alegações

O artigo alega que a Análise Quantitativa de Equivalência Parcial caracteriza e quantifica efetivamente o impacto da correção, oferecendo uma visão mais refinada do que a verificação de equivalência binária.

• Implicações de Segurança: Ajuda a identificar correções que podem exigir escrutínio extra (por exemplo, aquelas que afetam grandes porções do domínio de entrada) e distingue entre correções seguras que preservam a funcionalidade e aquelas que quebram suposições existentes ou pipelines de CI/CD ao restringir excessivamente as entradas.
• Contribuição Metodológica: O trabalho introduz uma nova heurística de busca por intervalos que equilibra escalabilidade e precisão, abordando as limitações das técnicas existentes de execução simbólica e contagem de modelos no contexto da análise de impacto de correção.
• Limitações: Os autores reconhecem que a abordagem depende da execução simbólica diferencial; se resumos simbólicos não puderem ser gerados, a análise não pode prosseguir. Além disso, as heurísticas atuais de busca por intervalos são focadas em domínios numéricos, embora os autores notem potencial para extensão a outros domínios (por exemplo, strings).

Os autores não alegam resolver todos os problemas de análise de correção, mas postulam que sua abordagem quantitativa fornece uma camada necessária de granularidade para entender as consequências comportamentais de correções de software.