Buffer Overrun Detection using Linear
Programming and Static Analysis
10th ACM Conference on Computer and Communications Security.
Washington, DC, October 2003.
Vinod Ganapathy, Somesh Jha
{vg,jha}@cs.wisc.edu
University of Wisconsin-Madison
David Chandler, David Melski, David Vitek
{chandler,melski,dvitek}@grammatech.com
Grammatech Inc., Ithaca, New York
Centro de Informática/UFPE
Tópicos Avançados em Engenharia de Software 2008-1
Rodrigo Diego Melo Amorim
Recife-PE
O Problema: Buffer Overflows
• Classe de vulnerabilidades altamente exploradas
o Bug extremamente comum
o Programas legados escritos em C continuam vulneráveis
600
500
400
300
200
100
0
1995
1997
Source: NVD/CVE
1999
2001
2003
2005
Buffer Overflows?
void foo (char *bar) {
// no bounds checking...
char c[12];
strcpy(c, bar);
}
int main (int argc, char **argv) {
foo(argv[1]);
}
Buffer Overflows?
void foo (char *bar) {
// no bounds checking...
char c[12];
strcpy(c, bar);
}
int main (int argc, char **argv) {
foo(argv[1]);
}
Buffer Overflows?
void foo (char *bar) {
// no bounds checking...
char c[12];
strcpy(c, bar);
}
int main (int argc, char **argv) {
foo(argv[1]);
}
A Solução:
Análise Estática
código fonte
Possíveis Buffer Overrun’s
• técnica automática que assegura que o código está seguro
antes de ser posto em produção
• Uso de Análise Estática de Programas
• Produção de uma lista de possíveis vulnerabilidades no
código
• combinar alertas de Buffer Overrun's com técnicas de
varredura de código
Análise Estática?
• Análise de Programa
o Conceito abstrato de varredura de código antes de pôr
em produção;
o Também conhecido como entendimento ou compreensão
de programas;
o Várias técnicas, desde análise manual até ferramentas
sofisticadas;
o Normalmente feita por ferramentas;
Contribuição
• Análise de Programa
o detecção de buffer overrun incorporado a uma ferramenta
de análise de programa
o fazer a análise de buffer overrun sensível ao contexto
o Torna os resultados mais precisos
• Resolução de restrições
o uso de programação linear para solucionar o problema de
análise de intervalo
Sensibilidade de Contexto?
Sensibilidade de Contexto?
Sensibilidade de Contexto?
Arquitetura da Ferramenta
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Code Surfer
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Code Surfer
• Ferramenta comercial (Grammatech Inc.)
• Ferramenta de analise de codigo. A partir de codigo,
produz:
o Grafo de Fluxo de Controle (GFC)
o Grafo de Dependência de Programa (GDP)
o Grafo de Dependência de Sistema (GDS)
•
‘Detection Front-End’
o
Associa cada ‘warning’ gerado à linha do código
fonte correspondente através do GDS;
Exemplo - código
Gerador de Restrições
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Geração de Restrições
• Quatro tipos de ponteiros de programa resultam em
restrições:
o Declaração
o Atribuição
o Chamada de Função
o Retorno de Função
• Quatro variáveis para cada buffer:
o buf_usd_max, buf_usd_min, buf_alc_max, buf_alc_min
• Operações em um buffer
o strcpy (tgt, src)
o tgt_usd_max >= src_usd_max
o tgt_usd_min =< src_usd_min
Métodos de Geração de Restrições
• Ordem dos Statements
o Análise sensível ao fluxo
 respeita a ordem do programa
o Análise insensível ao fluxo
 não respeita a ordem do programa
• Chamadas de Função
o Modelagem das funções sensíveis ao contexto
 respeitam a semântica da chamada de retorno
o Modelagem das funções insensíveis ao contexto
 ignoram a semântica da chamada de retorno
Exemplo – restrições geradas
Taint Analyser (Análise de
Segurança)
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Análise de Segurança
• Remove variáveis de restrições não inicializadas
o chamadas a bibliotecas não modeladas
o variáveis de programas não inicializadas
• Remove variáveis de restrições que tem ‘range’ de valores
infinitos;
• Necessário para que os solucionadores funcionem
corretamente
Solucionador de Restrições
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Solucionadores de Restrições
• Problema Abstrato
o Dado um conjunto de restrições em variáves máximas e
mínimas
o Retorna o menor ajuste possível que satisfaça todas as
restrições
• Abordagem
o Modelar e Solucionar como um programa linear
• Foram desenvolvidos dois solucionadores
o Vanilla (+ rápido, - preciso)
o Hierárquico (+ preciso, - rápido)
Programação Linear ?
•
•
•
•
Uma função Objetiva: F
Sujeita a: Um conjunto de restrições lineares C
Objetivo: otimizar o seu resultado
Exemplo:
o Maximize: x
o sujeito a: x =< 3
Solucionador de Restrições - Vanilla
• Objetivo: Obter valores para os limites do buffer
• Modelando como um programa linear:
Menor limite superior
Minimize: var_max
Sujeita a: um conjunto x de restrições
&
Maior limite inferior
Maximize: var_min
Sujeita a: um conjunto y de restrições
Solucionador de Restrições - Vanilla
• é possível reescrever da seguinte forma:
o Min:Σ (var_max) - Σ(var_min)
o sujeito a:um conjunto z de restrições
• Resolvendo apenas um programa linear teremos valores
para todas as variáveis!
Exemplo – valores das variáveis
Solucionador de Restrições - Vanilla
• Método impreciso: porque ?
o programas lineares infactíveis
• Lidamos com isso usando algoritmos de aproximação
• Identificamos Irreducibly Inconsistents Sets (IIS)
Análise insensível ao contexto
bar () {
foo () {
int y;
y = foobar(30);
int x;
x = foobar(5);
}
}
int foobar (int z) {
int i;
i = z + 1;
return i;
}
Resultado: x = y = [6..31]
Caminho correto 1
Caminho correto 2
Caminho falso
Adicionando Sensibilidade de Contexto
bar () {
foo () {
int y;
y = foobar(30);
int x;
x = foobar(5);
}
}
X = 5 +1
int foobar (int z) {
int i;
i = z + 1;
return i;
}
Y = 30 + 1
Resumo: i = z + 1
Sem caminhos falsos
X = [6..6]
Y = [31..31]
I = [6..31]
Adicionando Sensibilidade de Contexto
• Pode separar contexto de chamadas
• Número muito grande de variáveis de restrições
• Não suporta recursão
Detector ‘Front-End’
Código
fonte C
CodeSurfer
CFG’s, PDG’s
e SDG’s
Gerador de
Restrições
Restrições
Lineares
Taint Analyser
Restrições
Lineares
Solucionador
de Restrições
Warnings
Buffer
Overrun’s
Intervalos
para variáveis
Detector ‘Front-End’
buf_alloc_min
buf_used_max
Cenário 1: Possível Buffer Overrun
Detector ‘Front-End’
buf_alloc_min
buf_used_max
Cenário 2: Buffer Overrun
Resultados: Buffer Overrun's
Aplicação
Linhas de
Código
Warnings
Vulnerabidades Detectado?
WU-FTPD-2.5.0
16000
139
CA-1999-13
Sim
WU-FTPD-2.6.2
18000
178
Nenhuma
14 Novos
Sendmail-8.7.6
38000
295
Identificado por
Wagner et al.
Sim
Sendmail-8.11.6
68000
453
CA-2003-07
Sim
Conclusão
• Foi construída uma ferramenta para detectar buffer
overrun's
• Incorporada em um framework de entendimento de
programas
• Relevâncias
o foi adicionado sensibilidade ao fluxo
o reduzindo o número de falso positivos e, ao mesmo
tempo, mantendo a escalabilidade