Résumé Technique : Amélioration de l'Exécution Symbolique pour l'Analyse de Faisabilité des Chemins de Flux de Contrôle Interprocéduraux

Énoncé du Problème

L'analyse statique est une technique évolutive pour la sécurité et la fiabilité des logiciels, pourtant elle souffre fréquemment de taux élevés de faux positifs. Ces faux positifs surviennent souvent parce que les analyseurs statiques rapportent des chemins de flux de contrôle dans un Graphe de Flux de Contrôle Interprocédural (ICFG) qui sont théoriquement possibles mais en réalité infaisables à l'exécution en raison de contraintes sémantiques (par exemple, des valeurs de variables contradictoires). Déterminer si un chemin spécifique dans l'ICFG d'un programme est exécutable est connu sous le nom d'analyse de faisabilité de chemin.

Bien que l'exécution symbolique soit une technique puissante pour vérifier la faisabilité des chemins en explorant les chemins à l'aide de valeurs symboliques et de solveurs SMT, elle est confrontée à deux défis principaux lorsqu'elle est appliquée à ce problème spécifique :

1. Demande de Ressources et Explosion de Chemins : L'exécution symbolique standard tente d'explorer tous les chemins atteignables, ce qui entraîne une croissance exponentielle des états, particulièrement en présence de boucles et de branchements complexes.
2. Lacunes d'Automatisation : Les moteurs existants nécessitent souvent une configuration manuelle pour gérer les variables dont les valeurs sont inconnues (par exemple, la mémoire non initialisée, les retours de fonctions externes ou les arguments de pointeurs), ce qui entrave une intégration pleinement automatisée avec les outils d'analyse statique.

Méthodologie

Les auteurs proposent une méthode d'exécution symbolique dirigée conçue spécement pour vérifier la faisabilité d'un ensemble prédéfini de chemins d'ICFG. Contraراً à l'exécution symbolique traditionnelle qui explore tout l'espace d'états, cette approche dirige l'exécution strictement vers un chemin cible, éliminant l'exploration de régions de code non pertinentes.

La méthodologie repose sur quatre composantes techniques fondamentales :

1. Exécution Dirigée et Élagage

L'algorithme prend en entrée un ensemble de blocs de base autorisés ($S_{allowed}$) et un ensemble de jalons requis ($S_{req}$). Pendant l'exécution :

• Élagage : À chaque point de branchement, tout successeur de bloc de base n'appartenant pas à $S_{allowed}$ est élagué, empêissant le moteur d'explorer des régions de code non pertinentes.
• Vérification : Un chemin est jugé faisable uniquement si l'exécution atteint le bloc cible ($B_{target}$) tout en ayant visité tous les blocs de $S_{req}$ et en restant dans $S_{allowed}$.

2. Stratégies de Symbolisation Automatique

Pour permettre une analyse entièrement automatisée sans intervention de l'utilisateur, les auteurs introduisent des stratégies pour symboliser les valeurs qui sont typiquement inconnues ou concrètes dans une exécution standard :

• Paramètres de Point d'Entrée : Tous les paramètres de la fonction où l'analyse de chemin commence sont symbolisés.
• Variables et Mémoire Non Initialisées : Les variables locales non initialisées et la mémoire allouée dynamiquement (par exemple, via malloc) sont traitées comme des objets symboliques avec des valeurs non contraintes, plutôt que de provoquer un comportement indéfini ou une initialisation concrète.
• Fonctions Externes :
  • Valeurs de Retour : Les valeurs de retour des fonctions externes (dont le corps est indisponible) sont symbolisées.
  • Arguments de Pointeurs : Les emplacements mémoire référencés par des arguments de pointeurs non constants d'appels externes sont re-symbolisés pour tenir compte des effets de bord.
  • Variables Globales Spéciales : Un traitement spécifique est appliqué à errno (rendu symbolique après les appels externes) et environ (modélisé comme un ensemble fixe de variables symboliques avec des longueurs fixes pour éviter la non-terminaison lors des comparaisons de chaînes).
• Pointeurs de Fonctions et Fonctions Virtuelles : Le système résout les cibles potentielles pour les pointeurs de fonctions et les appels virtuels en analysant les tables virtuelles et les signatures de fonctions, en créant des embranchements (forking) d'états symboliques pour tous les candidats valides.

3. Modèle de Mémoire Flexible

Le document introduit un modèle de mémoire qui supporte les pointeurs symboliques sans dépendre d'allocations de tableaux de taille fixe.

• Allocation Paresseuse (Lazy Allocation) : Les objets de mémoire ne sont pas créés tant qu'un pointeur symbolique n'est pas déréférencé.
• Gestion de l'Aliasing : Lorsqu'un pointeur symbolique est déréférencé, le moteur considère les scénarios d'aliasing. Il crée un embranchement de l'état symbolique pour explorer les cas où le pointeur référence un objet mémoire existant (avec des décalages correspondants ou différents) par rapport à un emplacement mémoire totalement nouveau. Cela permet l'analyse de structures de données complexes comme les listes chaînées et les arbres sans pré-définir leur taille.

4. Stratégie de Bornage de Boucle

Pour atténuer l'explosion de chemins dans les boucles, la méthode emploie une stratégie de bornage de boucle :

• Un nombre maximal d'itérations ($C_{max}$) est défini.
• Si un état symbolique entre dans une boucle plus de $C_{max}$ fois, le moteur force l'état à sortir de la boucle via les arêtes de sortie disponibles.
• Crucialement, les emplacements mémoire écrits pendant l'exécution de la boucle sont symbolisés avant la sortie forcée. Cela garantit que le moteur peut toujours explorer des chemins qui dépendent des effets de bord de la boucle, même si le nombre exact d'itérations est tronqué. Cela introduit un compromis entre complétude et évolutivité, privilégiant la joignabilité de l'emplacement du défaut cible.

Contributions Clés

Le papier revendique les contributions suivantes :

1. Un algorithme d'exécution symbolique dirigée pour déterminer la faisabilité de n'importe quel chemin d'ICFG dans un ensemble spécifié.
2. Des stratégies de symbolisation entièrement automatiques pour les variables avec des valeurs inconnues, les retours de fonctions externes et les arguments de pointeurs.
3. Un modèle de mémoire supportant le raisonnement sur les pointeurs symboliques et l'aliasing sans contraintes de taille fixe.
4. Un algorithme de bornage de boucle qui limite les itérations sans interrompre l'exécution symbolique du chemin.
5. Une évaluation empirique sur des logiciels réels et la suite de tests Juliet.

Résultats Expérimentaux

La méthode a été implémentée comme une extension du moteur d'exécution symbolique KLEE (v3.1) et évaluée à l'aide des ensembles de données suivants :

1. Vérification de Chemins Réels (GNU Coreutils)

• Jeu de Données : 234 chemins d'ICFG uniques extraits de GNU Coreutils, allant de 22 à 1 218 blocs de base.
• Résultat : L'outil a atteint un rappel (recall) de 95,3 %, vérifiant avec succès 223 des 234 chemins.
• Observation : 49 chemins ont nécessité la stratégie de bornage de boucle. L'étude a noté qu'une stratégie de recherche en largeur (BFS) était occasionnellement nécessaire pour trouver les états cibles dans des scénarios de boucles complexes où la recherche en profondeur (DFS) ne parvenait pas à atteindre l'état dans les limites de temps imparties.

2. Intégration avec l'Analyseur Statique MLH

• Configuration : La méthode a été intégrée à l'outil d'analyse statique MLH et testée sur la suite de tests Juliet (CWE-401 : Fuite de mémoire).
• Résultat : L'intégration a augmenté la précision de l'outil de 56 % à 100 % tout en maintenant un rappel de 100 %. La méthode a réussi à éliminer tous les faux positifs sans perdre de vrais positifs.

3. Comparaison avec KLEEF

• Configuration : La méthode proposée a été comparée à KLEEF (un dérivé spécialisé de KLEE) en utilisant les rapports de Infer et de Clang Static Analyzer (CSA) sur la suite de tests Juliet (CWE-415 et CWE-416).
• Résultat :
  • Infer : KLEEF a réduit le score F1 de 1,0 à 0,0 (plantant sur 60 rapports et classant tous les vrais positifs comme infaisables). La méthode proposée a maintenu le score F1 à 1,0.
  • CSA : KLEEF a réduit le score F1 de 0,766 à 0,058. La méthode proposée a maintenu le score F1 à 0,767 (améliorant légèrement la précision en filtrant certains faux positifs tout en gardant un rappel de 100 %).
• Analyse : Les auteurs attribuent l'échec de KLEEF à son incapacité à gérer certains appels de fonctions externes et l'arithmétique de pointeurs symboliques, entraînant une terminaison précoce.

Signification et Revendications

Le papier positionne ce travail comme une solution pratique pour combler le fossé entre l'évolutivité de l'analyse statique et la précision de l'exécution symbolique. Les auteurs affirment qu'en dirigeant l'exécution symbolique et en automatisant la symbolisation, la méthode filtre efficacement les chemins infaisables rapportés par les analyseurs statiques.

La signification réside dans la capacité à :

• Automatiser le processus de vérification sans configuration manuelle des variables symboliques.
• Gérer des modèles de mémoire complexes (pointeurs, allocation dynamique) qui font souvent échouer les autres outils ou nécessitent des approximations de taille fixe.
• Améliorer les Métriques de l'Analyse Statique : Plus précisément, la méthode démontre sa capacité à éliminer les faux positifs (augmentant la précision) sans sacrifier la détection de vulnérabilités réelles (préservant le rappel).

Les auteurs reconnaissent un compromis entre complétude et évolutivité dû à la stratégie de bornage de boucle, mais soutiennent que pour l'objectif spécifique de validation des rapports d'analyse statique, prioriser la joignabilité de l'emplacement cible est un compromis acceptable. Des travaux futurs sont proposés pour paralléliser l'analyse et développer des stratégies de sélection d'état spécialisées pour améliorer davantage l'efficacité.