sea dsa

SEADSA: Une analyse de points à la vérification du C / C ++ de bas niveau

SeaDsa est une analyse basée sur un contexte, sur le terrain, sur le terrain et à la table à unification pour un code bit de Bitcode LLVM inspiré de DSA. SeaDsa est un ordre de grandeur plus évolutif et précis que Dsa et une implémentation précédente de SeaDsa grâce à une amélioration de la sensibilité au contexte, de l'ajout d'une sensibilité à l'écoulement partielle et d'une conscience de type.

Bien que SeaDsa puisse analyser Bitcode arbitraire LLVM, il a été adapté à une utilisation dans la vérification du programme des programmes C / C ++. Il peut être utilisé comme un outil autonome ou avec le cadre de vérification des Seahorn et ses analyses.

Cette branche prend en charge LLVM 14.

Exigences

SeaDsa est écrit en C ++ et utilise la bibliothèque Boost. Les principales exigences sont:

• Compilateur C ++ prenant en charge C ++ 14
• Boost> = 1,65
• Llvm 14

Pour exécuter des tests, installez les packages suivants:

• sudo pip install lit OutputCheck
• sudo easy_install networkx
• sudo apt-get install libgraphviz-dev
• sudo easy_install pygraphviz

Structure du projet

1. Les principales structures de données des points de graphes, Graph , Cell et Node , sont définies dans include/Graph.hh et src/Graph.cc .
2. L'analyse locale est dans include/Local.hh et src/DsaLocal.cc .
3. L'analyse ascendante est dans include/BottomUp.hh et src/DsaBottomUp.cc .
4. L'analyse descendante est dans include/TopDown.hh et src/DsaTopDown.cc .
5. Le cloner du nœud interprocédural est dans include/Cloner.hh et src/Clonner.cc .
6. Le code de manutention de type est dans include/FieldType.hh , include/TypeUtils.hh , src/FieldType.cc et src/TypeUtils.cc .
7. La découverte de la fonction d'allocateur est dans include/AllocWrapInfo.hh et src/AllocWrapInfo.cc .

Compilation et utilisation

Benchmarks de vérification du programme

Les instructions sur l'exécution de repères de vérification du programme, ainsi que des recettes de création de projets du monde réel et de nos résultats, peuvent être trouvés dans le thé-dsa-extras.

Intégration dans d'autres projets C ++ (pour les utilisateurs)

SeaDsa contient deux répertoires: include et src . Étant donné que SeaDsa analyse Bitcode LLVM, les fichiers d'en-tête et les bibliothèques LLVM doivent être accessibles lors de la construction avec SeaDsa .

Si votre projet utilise cmake , il vous suffit d'ajouter CMakeLists.txt de votre projet:

 include_directories(seadsa/include)
 add_subdirectory(seadsa)

Autonome (pour les développeurs)

Si vous avez déjà installé llvm-14 sur votre machine:

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run -DLLVM_DIR=__here_llvm-14__/share/llvm/cmake  ..
cmake --build . --target install

Sinon:

 mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=run ..
cmake --build . --target install

Pour exécuter des tests:

 cmake --build . --target test-sea-dsa

Visualiser les graphiques de mémoire et les graphiques d'appels complets

Considérez un programme C appelé 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 ;
}   

1. Générer le code binaire:

    clang -O0 -c -emit-llvm -S tests/c/simple.c -o simple.ll
   

L'option -O0 est utilisée pour désactiver les optimisations de Clang. En général, c'est une bonne idée d'activer les optimisations de Clang. Cependant, pour des exemples triviaux comme simple.c , Clang simplifie trop, donc rien d'utile ne serait observé. Les options -c -emit-llvm -S génèrent un code binaire au format lisible par l'homme.

2. Exécutez sea-dsa sur le code binaire et imprimez des graphiques de mémoire au format DOT:

    seadsa -sea-dsa=butd-cs -sea-dsa-type-aware -sea-dsa-dot  simple.ll
   

Les options -sea-dsa=butd-cs -sea-dsa-type-aware permettent l'analyse mise en œuvre dans notre article FMCAD'19 (voir références). Cette commande générera un fichier FUN.mem.dot pour chaque fonction FUN dans le programme Bitcode. Dans notre cas, la seule fonction est main et donc, il y a un fichier nommé main.mem.dot . Le fichier est généré dans le répertoire actuel. Si vous souhaitez stocker les fichiers .dot dans un autre répertoire DIR , ajoutez l'option -sea-dsa-dot-outdir=DIR

3. Visualisez main.mem.dot en le transformant en un fichier pdf :

    dot -Tpdf main.mem.dot -o main.mem.pdf
    open main.mem.pdf  // replace with you favorite pdf viewer 
   

Dans notre modèle de mémoire, une valeur de pointeur est représentée par une cellule qui est une paire d'un objet de mémoire et d'un décalage. Les objets de mémoire sont représentés comme des nœuds dans le graphique de mémoire. Les bords sont entre les cellules.

Chaque champ de nœud représente une cellule (c'est-à-dire un décalage dans le nœud). Par exemple, les champs de nœud <0,i32**> et <8,i32**> pointés par %6 et %15 , sont respectivement deux cellules différentes du même objet de mémoire. Le champ <8,i32**> représente la cellule au décalage 8 dans l'objet de mémoire correspondant et son type est i32** . Les bords noirs représentent des relations entre les cellules. Ils sont étiquetés avec un nombre qui représente le décalage dans le nœud de destination. Les bords bleus connectent les paramètres formels de la fonction avec une cellule. Les bords violets relient les variables de pointeur LLVM avec les cellules. Les nœuds peuvent avoir des marqueurs tels que S (mémoire allouée par pile), H (mémoire d'allocat de tas), M (mémoire modifiée), R (mémoire de lecture), E (mémoire allouée externe), etc. Si un nœud est rouge, cela signifie que la sensibilité au champ perdu d'analyse pour ce nœud. L'étiquette {void} est utilisée pour indiquer que le nœud a été alloué mais qu'il n'a pas été utilisé par le programme.

sea-dsa peut également résoudre les appels indirects. Un appel indirect est un appel où la Callee n'est pas connue statiquement. sea-dsa identifie toutes les callees possibles d'un appel indirect et génère un graphique d'appel LLVM comme sortie.

Considérez cet exemple dans 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 ;
}

Tapez les commandes:

 clang -c -emit-llvm -S tests/c/complete_callgraph_5.c  -o ex.ll
sea-dsa --sea-dsa-callgraph-dot ex.ll

Il génère un fichier .dot appelé callgraph.dot dans le répertoire actuel. Encore une fois, le fichier .dot peut être converti en fichier .pdf et ouvert avec les commandes:

 dot -Tpdf callgraph.dot -o callgraph.pdf
open callgraph.pdf  

sea-dsa peut également imprimer des statistiques sur le processus de résolution du graphique d'appel (notez que vous devez appeler clang avec -g pour imprimer des informations sur les fichiers, la ligne et la colonne):

 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)

Traitant de la bibliothèque C / C ++ et des appels externes

La sémantique du pointeur des appels externes peut être définie en écrivant un wrapper qui appelle l'une de ces fonctions définies dans 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 unifie toutes les cellules de l'argument, seadsa_collapse dit à sea-dsa de s'effondrer (c'est-à-dire, la perte de sensibilité sur le terrain) la cellule pointée par p , et seadsa_mk_seq indique à sea-dsa de marquer comme séquence le nœud pointé par p avec la taille sz .

Par exemple, considérez un foo externe défini comme suit:

 extern void* foo(const void*p1, void *p2, void *p3);

Supposons que le pointeur retourné soit unifié à p2 mais pas à p1 . De plus, nous aimerions effondrer la cellule correspondant à p3 . Ensuite, nous pouvons remplacer le prototype ci-dessus de foo par la définition suivante:

 #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;
}

Références

1. "Un modèle de mémoire sensible au contexte pour la vérification des programmes C / C ++" par A. Gurfinkel et Ja Navas. En sas'17. (Papier) | (Diapositives)

2. "Analyse du pointeur basé sur l'unification sans surpopulation" par J. Kuderski, JA Navas et A. Gurfinkel. Dans FMCAD'19. (Papier)