sea dsa
1.0.0
SeaDsa é um ponto de base de unificação para análise de contexto, campo e matriz para LLVM, inspirado no DSA. SeaDsa é uma ordem de magnitude mais escalável e precisa do que Dsa e uma implementação anterior de SeaDsa , graças ao melhor manuseio da sensibilidade ao contexto, adição de sensibilidade ao fluxo parcial e consciência do tipo.
Embora SeaDsa possa analisar o código de bits arbitrário LLVM, ele foi adaptado para uso na verificação do programa de programas C/C ++. Ele pode ser usado como uma ferramenta independente ou junto com a estrutura de verificação do Seahorn e suas análises.
Esta filial suporta LLVM 14.
SeaDsa é escrito em C ++ e usa a biblioteca de impulso. Os principais requisitos são:
Para executar testes, instale os seguintes pacotes:
sudo pip install lit OutputChecksudo easy_install networkxsudo apt-get install libgraphviz-devsudo easy_install pygraphvizGraph , Cell e Node , são definidas em include/Graph.hh e src/Graph.cc .include/Local.hh e src/DsaLocal.cc .include/BottomUp.hh e src/DsaBottomUp.cc .include/TopDown.hh e src/DsaTopDown.cc .include/Cloner.hh e src/Clonner.cc .include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc e src/TypeUtils.cc .include/AllocWrapInfo.hh e src/AllocWrapInfo.cc . As instruções sobre a execução de benchmarks de verificação do programa, juntamente com as receitas para a criação de projetos do mundo real e nossos resultados, podem ser encontrados no Tea-DSA-extras.
SeaDsa contém dois diretórios: include e src . Como os arquivos e bibliotecas de cabeçalho SeaDsa Analyzes LLVM, LLVM devem estar acessíveis ao criar com SeaDsa .
Se o seu projeto usar cmake , você só precisará adicionar CMakeLists.txt do seu projeto:
include_directories(seadsa/include)
add_subdirectory(seadsa)
Se você já instalou llvm-14 em sua máquina:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake ..
cmake --build . --target install
De outra forma:
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install
Para executar testes:
cmake --build . --target test-sea-dsa
Considere um programa C chamado tests/c/simple.c :
#include <stdlib.h>
typedef struct S {
int * * x ;
int * * y ;
} S ;
int g ;
int main ( int argc , char * * argv ){
S s1 , s2 ;
int * p1 = ( int * ) malloc ( sizeof ( int ));
int * q1 = ( int * ) malloc ( sizeof ( int ));
s1 . x = & p1 ;
s1 . y = & q1 ;
* ( s1 . x ) = & g ;
return 0 ;
} Gerar bitcode:
clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
A opção -O0 é usada para desativar otimizações de CLANG. Em geral, é uma boa idéia habilitar otimizações de Clang. No entanto, para exemplos triviais como simple.c , Clang simplifica muito, então nada útil seria observado. As opções -c -emit-llvm -S geram código de bits em formato legível por humanos.
Execute sea-dsa no código de bits e imprima gráficos de memória no formato de ponto:
seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot simple.ll
As opções -sea-dsa=butd-cs -sea-dsa-type-aware atabillem a análise implementada em nosso artigo FMCAD'19 (consulte Referências). Este comando gerará um arquivo FUN.mem.dot para cada função FUN no programa Bitcode. No nosso caso, a única função é main e, portanto, há um arquivo chamado main.mem.dot . O arquivo é gerado no diretório atual. Se você deseja armazenar os arquivos .dot em um diretório diferente DIR adicione a opção -sea-dsa-dot-outdir=DIR
Visualize main.mem.dot , transformando -o em um arquivo pdf :
dot -Tpdf main.mem.dot -o main.mem.pdf
open main.mem.pdf // replace with you favorite pdf viewer
Em nosso modelo de memória, um valor de ponteiro é representado por uma célula que é um par de um objeto de memória e deslocamento. Os objetos de memória são representados como nós no gráfico de memória. As bordas estão entre as células.
Cada campo do nó representa uma célula (ou seja, um deslocamento no nó). Por exemplo, os campos do nó <0,i32**> e <8,i32**> apontados por %6 e %15 , respectivamente, são duas células diferentes do mesmo objeto de memória. O campo <8,i32**> representa a célula no deslocamento 8 no objeto de memória correspondente e seu tipo é i32** . As bordas pretas representam pontos para as relações entre as células. Eles são rotulados com um número que representa o deslocamento no nó de destino. As bordas azuis conectam parâmetros formais da função com uma célula. Bordas roxas Connectar variáveis de ponteiro LLVM com células. Os nós podem ter marcadores como S (Memória alocada da pilha), H (Memória alocada de Heap), M (Memória Modificada), R (Leia Memória), E (memória alocada externamente), etc. Se um nó estiver vermelho, significa que a análise perdeu a sensibilidade do campo para esse nó. O rótulo {void} é usado para denotar que o nó foi alocado, mas não foi usado pelo programa.
sea-dsa também pode resolver chamadas indiretas. Uma chamada indireta é uma chamada em que o Callee não é conhecido estaticamente. sea-dsa identifica todos os callees possíveis de uma chamada indireta e gera um gráfico de chamada LLVM como saída.
Considere este exemplo nos tests/c/complete_callgraph_5.c :
struct class_t ;
typedef int ( * FN_PTR )( struct class_t * , int );
typedef struct class_t {
FN_PTR m_foo ;
FN_PTR m_bar ;
} class_t ;
int foo ( class_t * self , int x )
{
if ( x > 10 ) {
return self -> m_bar ( self , x + 1 );
} else
return x ;
}
int bar ( class_t * self , int y ) {
if ( y < 100 ) {
return y + self -> m_foo ( self , 10 );
} else
return y - 5 ;
}
int main ( void ) {
class_t obj ;
obj . m_foo = & foo ;
obj . m_bar = & bar ;
int res ;
res = obj . m_foo ( & obj , 42 );
return 0 ;
}Digite os comandos:
clang -c -emit-llvm -S tests/c/complete_callgraph_5.c -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll
Ele gera um arquivo .dot chamado callgraph.dot no diretório atual. Novamente, o arquivo .dot pode ser convertido em um arquivo .pdf e aberto com os comandos:
dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf
sea-dsa também pode imprimir algumas estatísticas sobre o processo de resolução de gráficos de chamadas (observe que você precisa chamar clang com -g para imprimir informações de arquivo, linha e coluna):
sea-dsa --sea-dsa-callgraph-stats ex.ll
=== Sea-Dsa CallGraph Statistics ===
** Total number of indirect calls 0
** Total number of resolved indirect calls 3
%16 = call i32 %12(%struct.class_t* %13, i32 %15) at tests/c/complete_callgraph_5.c:14:12
RESOLVED
Callees:
i32 bar(%struct.class_t*,i32)
%15 = call i32 %13(%struct.class_t* %14, i32 10) at tests/c/complete_callgraph_5.c:23:16
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
%11 = call i32 %10(%struct.class_t* %2, i32 42) at tests/c/complete_callgraph_5.c:36:9
RESOLVED
Callees:
i32 foo(%struct.class_t*,i32)
A semântica do ponteiro de chamadas externas pode ser definida escrevendo um invólucro que chama qualquer uma dessas funções definidas em seadsa/seadsa.h :
extern void seadsa_alias(const void *p, ...);extern void seadsa_collapse(const void *p);extern void seadsa_mk_seq(const void *p, unsigned sz); seadsa_alias unifica as células de todos os argumentos, seadsa_collapse diz ao sea-dsa para colapso (ou seja, perda de sensibilidade de campo) a célula apontada por p , e seadsa_mk_seq diz ao sea-dsa para marcar como sequência o nó apontado por p com tamanho sz .
Por exemplo, considere uma chamada externa foo definida da seguinte forma:
extern void* foo(const void*p1, void *p2, void *p3);
Suponha que o ponteiro retornado seja unificado para p2 , mas não para p1 . Além disso, gostaríamos de colapsar a célula correspondente a p3 . Em seguida, podemos substituir o protótipo acima do foo pela seguinte definição:
#include "seadsa/seadsa.h"
void* foo(const void*p1, void *p2, void*p3) {
void* r = seadsa_new();
seadsa_alias(r,p2);
seadsa_collapse(p3);
return r;
}
"Um modelo de memória sensível ao contexto para verificação de programas C/C ++", de A. Gurfinkel e JA Navas. Em SAS'17. (Papel) | (Slides)
"Análise de ponteiro baseada em unificação sem compartilhamento", de J. Kuderski, Ja Navas e A. Gurfinkel. Em fmcad'19. (Papel)
