Resumo Técnico: Execução Simbólica Dirigida para Análise de Viabilidade de Caminho em Testes de Segurança de Software

Declaração do Problema

A análise estática é uma técnica escalável para identificar vulnerabilidades de software ao analisar o código sem execução. No entanto, uma limitação significativa dos analisadores estáticos é a geração de relatórios de falsos positivos. Esses relatórios frequentemente decorrem da análise de caminhos de fluxo de controle inviáveis — sequências de blocos básicos que parecem válidas no Grafo de Fluxo de Controle Interprocedural (ICFG), mas que não podem ser executadas em tempo de execução devido a restrições semânticas.

Embora a execução simbólica possa, teoricamente, determinar a viabilidade de tais caminhos construindo e resolvendo restrições de caminho, sua aplicação prática é dificultada pelo problema da "explosão de caminhos". A execução simbólica padrão tenta explorar todos os caminhos alcançáveis, levando ao consumo exponencial de recursos. Além disso, as ferramentas existentes muitas vezes carecem da automação necessária para lidar com complexidades do mundo real, como memória não inicializada, chamadas de funções externas, ponteiros simbólicos e loops, sem intervenção manual ou instrumentação específica.

Metodologia

Os autores propõem um método de Execução Simbólica Dirigida projetado especificamente para verificar a viabilidade de um conjunto pré-definido de caminhos do ICFG. Diferente da execução simbólica tradicional, que explora todo o espaço de estados, esta abordagem direciona a execução estritamente para um caminho alvo, podando ramos não relacionados ao objetivo de verificação.

Algoritmo Central

O algoritmo opera sobre um conjunto de blocos básicos permitidos ($S_{allowed}$) e um conjunto de marcos obrigatórios ($S_{req}$) que devem ser percorridos para alcançar um bloco alvo ($B_{target}$).

1. Poda Dirigida: Em cada ponto de ramificação, o mecanismo explora um bloco sucessor apenas se ele pertencer a $S_{allowed}$. Isso elimina a exploração de regiões irrelevantes do programa.
2. Limitação de Loop (Loop Bounding): Para evitar a não terminação em loops, o método limita o número de iterações do loop ($C_{max}$). Se um loop exceder esse limite, o mecanismo força o estado simbólico a sair do loop através de arestas de saída disponíveis, simbolizando apenas as localizações de memória escritas durante a execução do loop. Isso permite que a análise continue além do loop em vez de terminar.
3. Verificação: Um caminho é considerado viável se a execução simbólica atingir $B_{target}$ tendo visitado todos os blocos em $S_{req}$ enquanto permanece dentro de $S_{allowed}$.

Estratégias de Simbolização Automática

Para permitir a análise totalmente automatizada sem configuração manual, o artigo introduz várias abordagens de simbolização:

• Parâmetros de Ponto de Entrada: Todos os parâmetros da função onde a análise de caminho começa são simbolizados, independentemente de a função ser o ponto de entrada main do programa.
• Memória Não Inicializada: Variáveis locais e regiões de memória alocadas dinamicamente não inicializadas são tratadas como objetos simbólicos com valores não restritos, garantindo que caminhos dependentes de comportamento indefinido não sejam descartados prematuramente.
• Funções Externas:
  • Valores de Retorno: Valores de retorno de funções externas (ex: bibliotecas dinâmicas) são simbolizados.
  • Argumentos de Ponteiro: Regiões de memória referenciadas por argumentos de ponteiro não constantes de chamadas externas são resimbolizadas para considerar potenciais efeitos colaterais.
  • Globais Especiais: O tratamento específico é aplicado ao errno (ressimbolizado após chamadas externas) e ao environ (modelado como um conjunto fixo de variáveis simbólicas com comprimentos fixos para evitar não terminação em funções de manipulação de ambiente).
• Ponteiros de Função e Funções Virtuais: O sistema resolve ponteiros de função simbólicos combinando assinaturas e, para funções virtuais, analisando tabelas virtuais para identificar todas as possíveis sobreposições de classes derivadas, criando ramificações de estado para cada candidato.

Modelo de Memória

O artigo propõe um modelo de memória flexível para ponteiros simbólicos com tamanhos desconhecidos (ex: arrays passados para funções). Em vez de alocar arrays de tamanho fixo, o modelo cria objetos de memória sob demanda na primeira desreferenciação.

• Alocação Sob Demanda: Um objeto de memória é criado apenas quando um ponteiro simbólico é acessado.
• Resolução de Aliasing: Quando um ponteiro é desreferenciado, o mecanismo verifica se existem objetos de memória com o mesmo deslocamento (offset). Se um alias for possível, o mecanismo cria uma ramificação (fork) do estado simbólico para explorar cenários onde o ponteiro referencia um objeto existente versus uma localização de memória nova e distinta. Isso suporta a análise de estruturas de dados complexas como listas ligadas e árvores sem restrições de tamanho pré-definidas.

Principais Contribuições

1. Algoritmo de Execução Simbólica Dirigida: Um método para determinar a viabilidade de caminhos específicos do ICFG ao restringir a exploração a um escopo definido.
2. Simbolização Totalmente Automática: Estratégias para lidar com parâmetros de ponto de entrada, variáveis não inicializadas, retornos de funções externas e argumentos de ponteiro sem intervenção do usuário.
3. Modelagem de Memória Simbólica: Um modelo de memória que suporta ponteiros simbólicos e cenários de aliasing, permitindo a análise de estruturas de dados arbitrárias.
4. Estratégia de Limitação de Loop: Um algoritmo que limita as iterações do loop para garantir a terminação enquanto permite que a execução simbólica prossiga para blocos de código subsequentes.
5. Avaliação Empírica: Uma avaliação abrangente utilizando software real (GNU Coreutils) e o NIST Juliet Test Suite.

Resultados Experimentais

O método foi implementado como uma extensão do motor de execução simbólica KLEE (v3.1) e avaliado em três contextos:

1. Escalabilidade em Caminhos do Mundo Real:

   • Testado em 234 caminhos de ICFG extraídos do GNU Coreutils (variando de 22 a 1.218 blocos básicos).
   • Alcançou um recall de 95,3%, verificando com sucesso 223 caminhos.
   • 49 caminhos exigiram a estratégia de limitação de loop (limite definido como 3), enquanto 174 foram verificados sem ela.
   • Os tempos de execução variaram de menos de um minuto para caminhos simples até aproximadamente 30 minutos para caminhos complexos envolvendo aritmética pesada de ponteiros simbólicos.

2. Integração com o Analisador Estático MLH:

   • Avaliado no Juliet Test Suite (subconjunto de CWE-401: Vazamento de Memória).
   • A integração aumentou a precisão da ferramenta MLH de 56,6% para 100% ao filtrar falsos positivos.
   • O recall foi preservado em 100%, confirmando que nenhuma vulnerabilidade real foi descartada.

3. Comparação com KLEEF:

   • Comparado com o KLEEF (um derivado do KLEE para código industrial) usando relatórios do Infer e Clang Static Analyzer (CSA) em subconjuntos do Juliet (CWE-415 e CWE-416).
   • Desempenho do KLEEF: Desempenho significativamente degradado. Para o Infer, o KLEEF reduziu o F1-score de 1,0 para 0,0 (classificando todos os verdadeiros positivos como inviáveis ou causando falhas). Para o CSA, o F1-score caiu de 0,766 para 0,074.
   • Desempenho do Método Proposto: Manteve o F1-score base do Infer (1,0) e melhorou ligeiramente o do CSA (0,767). O método verificou com sucesso todos os verdadeiros positivos e identificou corretamente caminhos viáveis para relatórios de falsos positivos (que podem ser filtrados posteriormente por verificações adicionais).

Significância e Alegações

O artigo alega que o método proposto preenche a lacuna entre a alta precisão da execução simbólica e a escalabilidade necessária para testes de segurança de software práticos. Ao direcionar a execução e automatizar a simbolização, a abordagem consegue filtrar caminhos inviáveis de relatórios de análise estática, eliminando assim falsos positivos sem sacrificar a detecção de vulnerabilidades reais.

Os autores reconhecem que a estratégia de limitação de loop introduz um compromisso (trade-off) entre completude e escalabilidade, podendo permitir a exploração de alguns caminhos logicamente inalcançáveis. No entanto, argumentam que este é um compromisso aceitável no contexto de validação de relatórios de análise estática, onde a prioridade é garantir o alcance do local do defeito em vez da exploração exaustiva de todos os comportamentos do loop. O método é apresentado como uma etapa de pós-processamento robusta que aumenta a confiabilidade das ferramentas de análise estática existentes.