Test concolique

Page d’aide sur l’homonymie

Ne doit pas être confondu avec l'exécution symbolique classique, dont le test concolique est une variante.

Le test concolique (un mot-valise formé de concret et symbolique, également appelé exécution symbolique dynamique) est une technique hybride de vérification de logiciel qui effectue une exécution symbolique, technique classique traitant les variables du programme comme des variables symboliques, le long d'un chemin d'exécution concrète (test sur des entrées particulières). L'exécution symbolique est utilisée conjointement avec un démonstrateur automatique de théorèmes ou un solveur de contraintes fondé sur la programmation logique par contraintes afin de générer de nouvelles entrées concrètes (cas de test), dans le but de maximiser la couverture de code. Son objectif principal est de trouver des bugs dans des logiciels réels plutôt que de démontrer la correction d'un programme.

Le concept a été décrit et discuté dans l'article « DART: Directed Automated Random Testing » de Patrice Godefroid, Nils Klarlund et Koushik Sen. L'article « CUTE: A concolic unit testing engine for C », de Koushik Sen, Darko Marinov et Gul Agha, a ensuite étendu l'idée aux structures de données et a été le premier à forger le terme test concolique (concolic testing). Un autre outil, appelé EGT (renommé EXE, puis amélioré et renommé KLEE), fondé sur des idées similaires, a été développé indépendamment par Cristian Cadar et Dawson Engler en 2005, et publié en 2005 et 2006. PathCrawler, a été le premier à proposer d'effectuer une exécution symbolique le long d'un chemin d'exécution concrète, mais, contrairement au test concolique, PathCrawler ne simplifie pas les contraintes symboliques complexes à l'aide de valeurs concrètes. Ces outils (DART, CUTE et EXE) ont appliqué le test concolique aux tests unitaires de programmes en C, et le test concolique a été conçu à l'origine comme une amélioration de type boîte blanche des méthodes établies de test aléatoire. La technique a ensuite été généralisée au test de programmes Java multithreads avec Modèle:Proper name, ainsi qu'au test unitaire de programmes à partir de leur code exécutable (outil OSMOSE). Elle a également été combinée au test par fuzzing et étendue à la détection de failles de sécurité exploitables dans de grands binaires x86 par l'outil SAGE de Microsoft Research,.

L'approche concolique s'applique aussi au model checking. Dans un model checker concolique, le vérificateur parcourt les états du modèle représentant le logiciel vérifié tout en conservant à la fois un état concret et un état symbolique. L'état symbolique sert à vérifier des propriétés du logiciel, tandis que l'état concret sert à éviter d'atteindre des états inaccessibles. ExpliSAT, de Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening et Ishai Rabinovitz, est un outil de ce type.

Naissance du test concolique

La mise en œuvre d'un test fondé sur l'exécution symbolique traditionnelle exige l'implémentation d'un interpréteur symbolique complet pour un langage de programmation. Les auteurs des premiers outils de test concolique ont remarqué qu'il était possible d'éviter l'implémentation d'une exécution symbolique complète en greffant celle-ci sur l'exécution normale du programme au moyen d'une instrumentation. C'est cette idée de simplification de l'exécution symbolique qui a donné naissance au test concolique.

Développement des solveurs SMT

Une raison importante de l'essor du test concolique (et plus généralement de l'analyse de programmes fondée sur l'exécution symbolique) au cours de la décennie qui a suivi son introduction en 2005 est l'amélioration spectaculaire de l'efficacité et de l'expressivité des solveurs SMT. Les principales avancées techniques ayant conduit au développement rapide des solveurs SMT sont la combinaison de théories, la résolution paresseuse, DPLL(T) et les énormes progrès de la vitesse des solveurs SAT. Parmi les solveurs SMT particulièrement adaptés au test concolique figurent Z3, STP, Z3str2 et Boolector.

Exemple

Considérons l'exemple simple suivant, écrit en C :

void f(int x, int y) {
    int z = 2 * y;
    if (x == 100000) {
        if (x < z) {
            assert(0); /* erreur */
        }
    }
}
Arbre des chemins d'exécution de cet exemple. Trois tests sont générés, correspondant aux trois feuilles de l'arbre et aux trois chemins d'exécution du programme.

Un test aléatoire simple, essayant des valeurs aléatoires de x et y, nécessiterait un nombre de tests irréaliste pour reproduire l'erreur.

On commence par un choix arbitraire de x et y, par exemple x = y = 1. Dans l'exécution concrète, la ligne 2 affecte 2 à z et le test de la ligne 3 échoue puisque 1 ≠ 100000. Simultanément, l'exécution symbolique suit le même chemin, mais traite x et y comme des variables symboliques. Elle affecte à z l'expression 2y et note que, le test de la ligne 3 ayant échoué, x ≠ 100000. Cette inégalité est appelée condition de chemin et doit être vraie pour toutes les exécutions qui suivent le même chemin que l'exécution courante.

Puisque l'on souhaite que le programme suive un chemin d'exécution différent lors de la prochaine exécution, on prend la dernière condition de chemin rencontrée, x ≠ 100000, et on la nie, ce qui donne x = 100000. Un démonstrateur automatique de théorèmes est alors invoqué pour trouver des valeurs des variables d'entrée x et y compte tenu de l'ensemble des valeurs symboliques et des conditions de chemin construites pendant l'exécution symbolique. Dans ce cas, une réponse valide du démonstrateur pourrait être x = 100000, y = 0.

L'exécution du programme sur cette entrée lui permet d'atteindre la branche interne de la ligne 4, qui n'est pas prise puisque 100000 (x) n'est pas inférieur à 0 (z = 2y). Les conditions de chemin sont x = 100000 et x ≥ z. Cette dernière est niée, ce qui donne x < z. Le démonstrateur cherche alors x et y satisfaisant x = 100000, x < z et z = 2y ; par exemple x = 100000, y = 50001. Cette entrée atteint l'erreur.

Algorithme

Pour l'essentiel, un algorithme de test concolique procède comme suit :

  1. Désigner un ensemble particulier de variables comme variables d'entrée. Ces variables seront traitées comme des variables symboliques pendant l'exécution symbolique. Toutes les autres variables seront traitées comme des valeurs concrètes.
  2. Instrumenter le programme de façon que chaque opération susceptible d'affecter la valeur d'une variable symbolique ou une condition de chemin soit consignée dans un fichier de trace, de même que toute erreur survenant.
  3. Choisir une entrée arbitraire pour commencer.
  4. Exécuter le programme.
  5. Réexécuter symboliquement le programme sur la trace, en générant un ensemble de contraintes symboliques (dont les conditions de chemin).
  6. Nier la dernière condition de chemin qui n'a pas encore été niée afin de visiter un nouveau chemin d'exécution. S'il n'existe aucune condition de chemin de ce type, l'algorithme se termine.
  7. Invoquer un solveur de satisfiabilité automatique sur le nouvel ensemble de conditions de chemin pour générer une nouvelle entrée. S'il n'existe aucune entrée satisfaisant les contraintes, revenir à l'étape 6 pour essayer le chemin d'exécution suivant.
  8. Revenir à l'étape 4.

La procédure ci-dessus présente quelques complications :

Succès commercial

L'analyse et le test fondés sur l'exécution symbolique, en général, ont suscité un intérêt notable de la part de l'industrie[réf. nécessaire]. L'outil commercial le plus connu utilisant l'exécution symbolique dynamique (c'est-à-dire le test concolique) est probablement SAGE de Microsoft. Les outils KLEE et S2E (tous deux open source et utilisant le solveur de contraintes STP) sont largement employés dans de nombreuses entreprises, dont Micro Focus Fortify, NVIDIA et IBM[réf. nécessaire]. Ces technologies sont de plus en plus utilisées par les entreprises de sécurité comme par les pirates pour trouver des vulnérabilités.

Limites

Le test concolique présente un certain nombre de limites :

Outils

De nombreux outils, notamment DART et SAGE, n'ont pas été rendus publics. On notera toutefois que SAGE, par exemple, est « utilisé quotidiennement » pour les tests de sécurité internes chez Microsoft.

Notes et références

  1. ↑ Patrice Godefroid, Nils Klarlund et Koushik Sen, « DART: Directed Automated Random Testing », dans Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, New York, NY, ACM, (ISSN 0362-1340, lire en ligne), p. 213–223
  2. ↑ Koushik Sen, Darko Marinov et Gul Agha, « CUTE: a concolic unit testing engine for C », dans Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, New York, NY, ACM, (ISBN 1-59593-014-0, lire en ligne), p. 263–272
  3. ↑ Cristian Cadar, Vijay Ganesh, Peter Pawloski, David L. Dill et Dawson Engler, « EXE: Automatically Generating Inputs of Death », dans Proceedings of the 13th International Conference on Computer and Communications Security (CCS 2006), Alexandria, VA, USA, ACM, (lire en ligne)
  4. ↑ Nicky Williams, Bruno Marre et Patricia Mouy, « On-the-Fly Generation of K-Path Tests for C Functions », dans Proceedings of the 19th IEEE International Conference on Automated Software Engineering (ASE 2004), 20–25 September 2004, Linz, Austria, IEEE Computer Society, (ISBN 0-7695-2131-2), p. 290–293
  5. ↑ Nicky Williams, Bruno Marre, Patricia Mouy et Muriel Roger, « PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis », dans Dependable Computing - EDCC-5, 5th European Dependable Computing Conference, Budapest, Hungary, April 20–22, 2005, Proceedings, Springer, (ISBN 3-540-25723-3), p. 281–292
  6. ↑ Koushik Sen et Gul Agha, « CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools », dans Computer Aided Verification: 18th International Conference, CAV 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings, Springer, (ISBN 978-3-540-37406-0, lire en ligne), p. 419–423
  7. ↑ Sébastien Bardin et Philippe Herrmann, « Structural Testing of Executables », dans Proceedings of the 1st IEEE International Conference on Software Testing, Verification, and Validation (ICST 2008), Lillehammer, Norway, IEEE Computer Society, (ISBN 978-0-7695-3127-4, lire en ligne), p. 22–31
  8. ↑ Patrice Godefroid, Michael Y. Levin et David Molnar, « Automated Whitebox Fuzz Testing », Rapport technique TR-2007-58, sur Microsoft Research,
  9. ↑ Patrice Godefroid, « Random testing for security: blackbox vs. whitebox fuzzing », dans Proceedings of the 2nd international workshop on Random testing: co-located with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), New York, NY, ACM, (ISBN 978-1-59593-881-7, lire en ligne), p. 1
  10. ↑ Sharon Barner, Cindy Eisner, Ziv Glazberg, Daniel Kroening, Ishai Rabinovitz : ExpliSAT: Guiding SAT-Based Software Verification with Explicit States, Haifa Verification Conference 2006, p. 138-154.
  11. ↑ « Software »
  12. ↑ (en) Léo Andrès, « Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly », The Art, Science, and Engineering of Programming, vol. 9, no 1,‎ , article no 3 (DOI 10.22152/programming-journal.org/2025/9/3, lire en ligne)
  13. ↑ SAGE team, « Microsoft PowerPoint - SAGE-in-one-slide », Microsoft Research, (consulté le )

Articles connexes