Resumo Técnico: De TinyGo ao compilador gc: Estendendo o Framework Concolic de Zorya para Binários Go do Mundo Real

Declaração do Problema

A análise de segurança de binários Go compilados com o compilador padrão gc permanece um desafio significativo. Diferentemente dos binários compilados com TinyGo (que produzem executáveis de thread única com runtimes mínimos), os binários compilados com gc utilizam um runtime complexo que gerencia goroutines, coleta de lixo e agendamento preemptivo em múltiplos threads do sistema operacional. Ferramentas existentes de execução simbólica (por exemplo, KLEE, angr, Radius2) são projetadas principalmente para C/C++ e dependem de representações intermediárias (IR) do LLVM, para as quais o Go não compila totalmente. Além disso, essas ferramentas frequentemente falham em modelar mecanismos específicos do runtime do Go, como preemptão cooperativa/assíncrona, agendamento de goroutines e funções mapeadas em memória do VDSO, tornando-as ineficazes contra binários Go de produção. Iterações anteriores do framework Zorya limitavam-se a binários TinyGo, deixando uma lacuna na análise de aplicações Go do mundo real, multithread.

Metodologia

O artigo apresenta uma extensão do Zorya, um framework de execução concolic que eleva binários compilados para a representação intermediária P-Code do Ghidra. A extensão permite a análise de binários multithread compilados com gc através de três mecanismos técnicos principais:

1. Restauração de Estado e Agendamento Multithread:

   • O Zorya restaura o estado de todos os threads do sistema operacional a partir de dumps do gdb na inicialização, capturando estados de registradores, bases de armazenamento local de thread (TLS) e backtraces.
   • Os threads são classificados (por exemplo, thread principal, monitor de sistema, aguardando) para facilitar o agendamento.
   • O framework neutraliza a preemptão do runtime e emprega uma política de agendamento "apenas principal" para análise no modo de função, restringindo a execução concolic à thread principal para evitar interrupções provenientes da coleta de lixo ou monitores de sistema. Isso permite a exploração contínua de funções no nível do usuário.

2. Análise de Caminhos Sobrepostos com Semântica de Cópia ao Escrever (CoW):

   • Para abordar a explosão de caminhos e raciocinar sobre ramos não tomados sem bifurcar todo o estado (o que pode exceder 1 GiB para binários gc), o Zorya implementa um mecanismo de sobreposição.
   • Quando um ramo condicional envolve variáveis simbólicas rastreadas, uma sobreposição leve é criada para o caminho não tomado. Leituras consultam a sobreposição primeiro, recorrendo ao estado base em caso de falha; gravações vão exclusivamente para a sobreposição.
   • Essa sobreposição executa um número limitado de instruções (padrão $N=15$) antes de ser descartada, permitindo a detecção de vulnerabilidades em caminhos não percorridos pelo traço concreto.

3. Detecção de Vulnerabilidades via Rotina Analisadora:

   • O framework executa instruções com valores concretos (a partir do dump do gdb) e expressões simbólicas (gerenciadas pelo solucionador SMT Z3).
   • Uma "Rotina Analisadora" verifica padrões de vulnerabilidade em cada instrução, incluindo desreferenciamento de ponteiro nulo, estouro de inteiro e divisão por zero.
   • Para binários gc, o sistema aproveita tanto a exploração de AST (para localizar chamadas explícitas de pânico) quanto a execução sobreposta (para detectar vulnerabilidades silenciosas que não acionam panics do runtime).

Contribuições Principais

• Extensão para Binários gc: O framework foi estendido para analisar binários multithread produzidos pelo compilador Go padrão, preenchendo a lacuna entre ferramentas de pesquisa e software Go de produção.
• Conjunto de Dados de Vulnerabilidades do Mundo Real: Os autores curaram um corpus de 11 vulnerabilidades do mundo real de projetos de produção (incluindo Kubernetes, Go-Ethereum e CoreDNS), completos com fluxos de trabalho de reprodução e entradas de acionamento.
• Avaliação Comparativa: O Zorya foi avaliado contra sete ferramentas de última geração (três analisadores estáticos, dois fuzzers e dois executores simbólicos em nível de binário).
• Detecção de Vulnerabilidades Silenciosas: O framework detectou com sucesso vulnerabilidades que não acionam panics do runtime, especificamente estouro de inteiro silencioso, sem exigir oráculos escritos manualmente.

Resultados

A avaliação foi conduzida em 11 vulnerabilidades do mundo real em três classes: desreferenciamento de ponteiro nulo, estouro de inteiro e índice fora dos limites.

• Taxa de Detecção: O Zorya detectou 7 de 11 vulnerabilidades.
  • 4 foram capturadas pela Rotina Analisadora no caminho concreto (tomado).
  • 3 foram identificadas via alcançabilidade de pânico em AST no ramo não tomado.
  • 2 descobertas secundárias foram reveladas via execução sobreposta em caminhos não tomados (detectadas dentro do limite de profundidade de 15 instruções).
• Detecção Única: O Zorya foi a única ferramenta a detectar um estouro de inteiro silencioso na função memoryGasCost do Go-Ethereum (v1.6.0). Este bug envolve uma multiplicação que envolve silenciosamente na aritmética sem sinal do Go, permitindo que um atacante aloque memória massiva para gás quase zero. Nenhuma outra ferramenta avaliada encontrou este bug sem um oráculo escrito manualmente.
• Comparação de Ferramentas:
  • Analisadores Estáticos (staticcheck, gosec, nilaway): Detectaram 0 das 11 falhas. O gosec perdeu estouro de aritmética do mesmo tipo, e o nilaway falhou em pacotes do Kubernetes devido a problemas de resolução de dependências.
  • Fuzzers (go test -fuzz, GoLibAFL): Detectaram 5 das 11 falhas (incluindo kube-sm-2025, que o Zorya perdeu devido ao esgotamento de recursos na execução simbólica de runtime.memmove). Fuzzers foram mais rápidos (média de ~0,18s a 7s), mas exigiram harnesses escritos manualmente e perderam vulnerabilidades silenciosas que não causam travamento.
  • Outros Executores Simbólicos (BINSEC, SymQEMU): Detectaram 0 das 11 falhas, principalmente devido à falta de suporte para primitivas do runtime Go.
• Desempenho: O Zorya teve uma média de 16,5 minutos por detecção, significativamente mais lento que fuzzers, mas fornece um traço completo de execução em nível de instrução e opera totalmente automaticamente sem harnesses.

Significado e Alegações

O artigo afirma que o Zorya aborda uma lacuna crítica no cenário de segurança do Go. Enquanto analisadores estáticos falham em raciocinar sobre aritmética e aliasing específicos do programa, e fuzzers exigem harnesses manuais e perdem bugs que não causam travamento, o Zorya oferece uma análise totalmente automática em nível de binário capaz de detectar vulnerabilidades silenciosas.

Os autores posicionam o Zorya como uma ferramenta que combina exploração de sobreposição granular, recuperação de estado inicial multithread e detecção de estouro silencioso especificamente para binários Go. O trabalho demonstra que a execução concolic pode ser adaptada ao runtime complexo e multithread do compilador Go padrão, permitindo a detecção de vulnerabilidades (como estouro de inteiro silencioso) que são invisíveis para outras ferramentas avaliadas. O artigo conclui que, embora o Zorya seja mais lento que fuzzing, sua capacidade de fornecer traços exatos em nível de instrução e detectar bugs que não causam travamento o torna uma adição valiosa ao conjunto de ferramentas de engenharia de segurança de software.