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

At a time where software are omnipresent in our daily life, verifying their safety and security present an important challenge for the industry. The most used technique to ensure that a software meets certain requirements is testing, where we run the program with some controlled input sets. A major issue is then to ensure that these input sets cover enough different situations. Many proposals have been made, called coverage criteria, which define test objectives through which at least one execution must pass during tests. In this thesis, we examine different possibilities to combine formal methods (mathematical techniques) and testing in order to improve the efficiency of the testing process. We focused our efforts on dataflow criteria, which observe the behavior of definitions and uses of each variables in the program, and the detection of polluting objectives for these criteria.We proposed several techniques, with their implementations and evaluations on real C programs. We then studied the impact of these dataflow criteria on test generation. Finally, we conclude by designing a method, using polluting objectives detection, to verify the effectiveness of countermeasures against fault injection attacks, and thus find errors in their implementation. This method was applied to the bootloader of WooKey, an encrypted storage device.La vérification de logiciels représente un défi important à l’heure où ces derniers sont présents partout dans notre vie quotidienne. La technique la plus employée pour s’assurer qu’un logiciel répond à certaines exigences reste le test, c’est à dire exécuter le programmes sur un certain nombres d’entrées représentatives. Un enjeu majeur est alors de s’assurer que ces jeux d’entrée couvrent suffisamment de situations différentes.De nombreuses propositions ont été faites, appelées critères de couvertures, qui définissent des objectifs de tests, par lesquels doit passer au moins une exécution au cours du test. Dans cette thèse, nous examinons différentes possibilités pour combiner les méthodes formelles (techniques mathématiques) et le test, dans l’objectif d’améliorer l’efficacité de ce dernier. Nous nous sommes principalement intéressés aux critères de flot de données, qui observent le comportement des définitions et utilisations des variables du programme, et en particulier à la détection des objectifs polluants. Nous avons proposé plusieurs techniques, avec leurs implémentations et évaluations sur des exemples de programmes C réel. Nous étudions ensuite l’impact que ces objectifs de flot de données peuvent avoir sur la génération de test. Enfin, nous terminons en concevant une méthode permettant d’utiliser la détection d’objectifs polluants pour vérifier l’efficacité des contre-mesures contre les attaques par injection de fautes, et de trouver ainsi les erreurs dans leur implémentation. Cette méthode a été appliquée le bootloader de WooKey, un périphérique de stockage chiffré