< Retour au sommaire

Soutenance de thèse de Thibault Martin

Titre: Techniques de test pour des critères de couverture avancés

le

Lieu: Amphi 33/34

English version below

Résumé

Dans les dernières décennies, l’essor de l’informatique et d’internet ont grandement bouleversé nos modes de vie. Nos voitures, avions, trains, sont équipés des systèmes informatiques puissants. Nous pilotons certaines de nos centrales nucléaires avec des logiciels et nous sauvons même des vies grâce à des équipements médicaux avancés. Naturellement, tous ces logiciels sont conçus et développés par des humains qui sont susceptibles de commettre des erreurs lors de la conception ou l’implémentation de ces logiciels Certains de ces bugs peuvent avoir des conséquences très graves et coûteuses pour ceux qui en sont victimes. Développeurs et utilisateurs ont besoin d’avoir confiance en ces systèmes et donc dans la qualité des logiciels qui y sont exécutés. Plusieurs techniques existent afin de vérifier la sûreté et la sécurité des logiciels, par exemple le test, où on exécute le logiciel avec plusieurs entrées possibles afin de vérifier que le comportement correspond à nos attentes. D’autres techniques, dites méthodes formelles, utilisent la logique et les mathématiques pour prouver des propriétés sur un programme. Elles demandent plus d’expertise et de temps que le test, mais amènent souvent à un plus haut niveau de confiance. Dans cette thèse, nous examinons des possibilités pour combiner les différentes techniques de test avec les méthodes formelles, tout en restant automatique pour demander moins d’expertise possible à l’utilisateur, dans le but d’améliorer les performances des tests. Nous avons étudié en particulier des critères de couverture de code avancés, tel que les critères de flot de données qui visent à observer comment les définitions des variables sont utilisées dans le programme. Ces critères définissent alors des objectifs de test qu’il faut couvrir avec des cas de test. Mais il se trouve que certains objectifs peuvent être polluants et ont un impact négatif sur les résultats des tests, notamment les performances (temps d’exécution) ou la couverture. La première contribution de cette thèse était d’identifier des objectifs polluants, pour les critères de flot de données, en utilisant l’analyse de flot de données, l’interprétation abstraite et l’analyse de plus faible précondition. Nos résultats ont montré que ces objectifs complexes sont souvent polluants et nous avons comparé plusieurs techniques de détection. Ensuite, nous avons proposé des techniques de génération de tests à base d’exécution symbolique dynamique pour les critères de flot de données. On s’est intéressé en particulier à deux types de critères plus complexes : les critères de test de flot de données aux limites et la visibilité des objectifs de test dans la sortie des fonctions. Enfin, nous nous sommes penchés sur un sujet un peu différent : l’injection de fautes. L’injection de fautes consiste à modifier la mémoire d’un programme pendant son exécution en inversant par exemple un bit (de 0 à 1 et inversement). Des techniques existent pour se prémunir de ce type de fautes, appelées contre-mesures. Nous avons proposé une méthode utilisant la vérification déductive sur les objectifs polluants pour prouver l’efficacité d’un type de contre-mesures. Nos résultats sur un cas d’étude réel, WooKey, ont permis de prouver la plupart des contre-mesures et de trouver une erreur dans une autre. Toutes les techniques que nous avons proposées sont implémentées dans la boîte à outils LTest qui est publiquement disponible, excepté l’outil de génération de tests.

Jury

English Version

PhD Defense of Thibault Martin

Title: Testing techniques for advanced test coverage criteria

Abstract

In the last decades, the rise of electronic devices and the Internet have greatly changed our way of life. Our cars, planes, trains, are equipped with powerful computer systems. We control some of our nuclear power plants with software and even save lives thanks to advanced medical equipment. Of course, said software products are designed and developed by humans who are prone to make mistakes when designing or implementing them. Some of these bugs can have very serious and costly consequences. Developers and users need to have confidence in these systems and therefore in the quality of the software that is executed on them. Several techniques exist to verify the safety and security of software, for example testing, where we execute the software with several possible inputs to verify that the behavior corresponds to our expectations. Other techniques, called formal methods, use logic and mathematics to prove properties of a program. They require more expertise and human intervention than testing, but often lead to a higher level of confidence. In this thesis, we examine possibilities to combine different testing techniques with formal methods, while remaining automated to require less expertise from the user, in order to improve the performance of the tests. We have studied in particular advanced code coverage criteria, such as dataflow criteria which aim at observing how variable definitions are used in the program. These criteria define test objectives that must be covered with test suites. But it turns out that some objectives can be polluting and have a negative impact on the results of the tests, in particular the performance (execution time) or coverage. The first contribution of this thesis was to identify polluting objectives, for the dataflow criteria, using dataflow analysis, abstract interpretation, and weakest precondition analysis. Our results showed that these complex objectives are often polluting and we compared several detection techniques. Then, we proposed techniques for generating tests based on dynamic symbolic execution for dataflow criteria. We were particularly interested in two more complex types of criteria: dataflow criteria at the boundaries and the visibility of test objectives in the output of functions. Finally, we looked at a slightly different subject: fault injection. Fault injection consists in modifying the memory of a program during its execution by inverting for example a bit (from 0 to 1 and conversely). Techniques exist to protect against this type of faults, called countermeasures. We have proposed a method using deductive verification on polluting objectives to prove the effectiveness of a type of countermeasures. Our results on a real case study, WooKey, allowed us to prove most of the countermeasures and to find an error in one of them. All the techniques we proposed are implemented in the LTest toolkit, which is publicly available, except for the test generation tool.

Defense committee