jdataflow

jdataflow

JDataflow est un analyseur de flux de données basé sur le solveur Z3 pour le code source Java.

Capacités

À l'heure actuelle, Jdataflow a des vérificateurs qui permettent de détecter les erreurs logiques (toujours vraies / fausses expressions), les déréférences du pointeur nul, les indices de tableau hors limites, etc.

Par exemple:

 void f ( boolean c ) {
    int x = 5 ;
    int y = c ? 3 : 2 ;
    if ( x < y ) {} // <= always false
}

void g ( int x , int y ) {
    if ( 2 * x + 3 * y == 12 ) {
        if ( 5 * x - 2 * y == 11 ) {
            if ( x == 3 ) {} // <= always true
            if ( y == 2 ) {} // <= always true
        }
    }
}

void h ( Something x ) {
    if ( x == null ) {
        x . f (); // <= null dereference
    }
}

void z () {
    int [] arr = new int [] { 1 , 2 , 4 , 8 , 16 , 32 };
    int x = arr [ 9 ]; // <= array index out of bounds
}

Consultez le répertoire du test pour plus d'exemples.

En général, Jdataflow est capable d'évaluer les expressions statiquement, d'effectuer une exécution symbolique, de gérer le flux de contrôle d'un programme, etc. Il dispose également d'un modèle de mémoire approprié, il traite donc bien de l'alias de référence.

Construire et courir

Afin de construire Jdataflow, vous avez besoin de JDK 8 ou plus récent. Vous devez également télécharger et installer Z3.

Windows:

1. Téléchargez Z3-4.8.4 ici: https://github.com/z3prover/z3/releases
2. Ajouter le répertoire bin à votre variable d'environnement de chemin
3. Exécuter gradlew build

Remarque: Visual C ++ 2015 Redistribuable peut être nécessaire.

Linux:

1. Téléchargez Z3-4.8.4 ici https://github.com/z3prover/z3/releases
2. Ajoutez un répertoire bin à votre ld_library_path: export LD_LIBRARY_PATH=/path/to/z3/bin
3. Run ./gradlew build

macOS:

1. Téléchargez Z3-4.8.4 ici https://github.com/z3prover/z3/releases
2. Ajoutez un répertoire bin à votre dyld_library_path: export DYLD_LIBRARY_PATH=/path/to/z3/bin
3. Run ./gradlew build

Notez que vous devrez peut-être encore configurer des variables d'environnement ou java.lang.path dans votre IDE.

Vous pouvez maintenant aller au répertoire de construction et exécuter le pot résultant:
java -jar jdataflow.jar --sources <args...> [--classpath <arg>] [--classpath-file <arg>]

Si vous souhaitez vérifier votre projet Ant, Maven ou Gradle avec JDataflow, vous devez utiliser Scan Utils.

Sous le capot

Ast

Jdataflow utilise la bibliothèque de la cuillère pour construire et traverser AST de manière post-ordre. Tout en traversant l'AST, il traduit le code source en une forme compréhensible par Z3 Solver. Ensuite, les contrôles sont effectués par le solveur.

Formulaire statique à affectation unique (SSA)

Tout d'abord, pour être utilisé avec Z3, le code doit être présent dans le formulaire d'attribution unique statique. Nous le faisons pour maintenir l'ordre d'un programme dans une formule logique. Voici un exemple simple:

Formulaire original:

 x = 1;
y = 2;
x = x + y;

Formulaire SSA:

 x0 = 1;
y0 = 2;
x1 = x0 + y0;

Conditions

Après l'instruction IF Traversing, nous créons une nouvelle variable, qui est le résultat d'une fonction spéciale if-then-else fournie par Z3. Cette fonction rejoint essentiellement les valeurs des branches sur une condition.

Formulaire original:

 if (c) {
    x = 1;
} else {
    x = 2;
}

Formulaire SSA:

 if (c) {
    x0 = 1;
} else {
    x1 = 2;
}
x3 = ITE(c0, x0, x1);

Fonctions et analyse interprocédurale

L'approche la plus évidente pour gérer les appels de fonction est de les alimenter. Malheureusement, nous ne pouvons le faire que pour les petites fonctions (comme les getters ou les setters), en raison des considérations de performance.
Une autre approche consiste à créer des résumés de fonctions (automatiquement ou manuellement), qui contiennent des informations sur les contrats, la pureté, les valeurs de retour, etc.
Mais en général, toute fonction inconnue réinitialise les valeurs de ses arguments.

Boucles

L'approche la plus évidente pour gérer les boucles est de les dérouler. Malheureusement, nous ne pouvons le faire que lorsque le nombre d'itérations est connu statiquement et relativement petit.
Donc, en général, nous devons trouver des invariants de boucle et réinitialiser tout le reste, comme pour les fonctions inconnues.
Cependant, certains cas particuliers pourraient être traités différemment.

Modèle de mémoire

JDataflow utilise le modèle de mémoire indexé de type (modèle de mémoire de Burstall). Dans ce modèle de mémoire, chaque type ou champ de données a son propre tableau de mémoire. Il permet de détecter quelque chose comme ça:

 void m () {
    C a = new C ();
    a . x = 10 ;
    C b = a ;
    b . x = 20 ;
    if ( a . x == 20 ) {} // <= always true
}

Voici quelques liens utiles avec une explication plus détaillée des différents modèles de mémoire:

• https://llvm.org/pubs/2009-01-vmcai-scalablememorymodel.pdf
• https://www.researchgate.net/publication/221430855_a_memory_model_for_static_analysis_of_c_programs

Liste de faire

Pour le moment, ce projet n'est qu'une preuve de concept, il y a donc beaucoup de travail à faire:

• Meilleure analyse interprocédurale et résumés de fonctions;
• Meilleure analyse de boucle;
• Analyse parallèle;
• Analyser les chaînes (Z3STR a cependant des limites de performance);
• Détecter les déréférences nulles potentielles et l'OOB potentiel ;