Chukri Soueidi

Résumé:

La vérification à l'exécution est une technique de vérification dynamique cruciale pour le raisonnement formel sur les exécutions de programmes, applicable tant au développement d'applications qu'en ligne dans des environnements de production. L'instrumentation joue un rôle crucial pour garantir que les moniteurs reçoivent des traces précises qui abstraient les informations nécessaires du programme en exécution. Sinon, l'intégrité du processus de surveillance est compromise, rendant les résultats peu fiables. Cette thèse se focalise sur la surveillance à l'exécution et les programmes concurrents, en abordant trois défis principaux : la capture des traces correctes, le guidage efficace de l'instrumentation, et l'évaluation de la validité des traces collectées. Pour répondre à ces défis, nous introduisons BISM, un cadre d'instrumentation au niveau du bytecode pour les langages JVM, offrant des abstractions de haut niveau pour divers utilisateurs dans le domaine de la vérification à l'exécution. BISM permet l'extraction d'événements au niveau du bytecode, accommodant la surveillance de propriétés spécifiées avec divers niveaux de granularité. BISM permet également d'écrire des analyses statiques en spécifiant l'instrumentation. Il offre aux utilisateurs avancés la possibilité de modifier de manière non restreinte et flexible le code existant. Ces dernières caractéristiques sont essentielles pour déployer des moniteurs en ligne ou imposer certaines propriétés comme un ordre séquentiel d'événements concurrents. Nous introduisons aussi une méthode nouvelle pour la vérification à l'exécution résiduelle de propriétés paramétriques, réduisant les points d'instrumentation et applicable à des propriétés de sécurité. Pour les programmes concurrents, nous mettons en évidence les limites de l'utilisation de traces linéaires et introduisons une méthodologie de collecte de traces utilisant un algorithme d'horloge vectorielle en temps réel, minimisant l'impact sur l'exécution. Cette méthode intègre une relation de dépendance causale, permettant d'évaluer la validité des traces dans les programmes concurrents pour un verdict de surveillance fiable. Nos contributions sont évaluées à travers des expériences sur divers benchmarks et applications, utilisant BISM dans un contexte plus large d'analyse dynamique, y compris l'analyse de logs, la couverture des tests, et le profilage. Ces travaux améliorent la fiabilité et l'efficacité de cette surveillance pour les programmes concurrents, fournissant des outils pratiques pour l'avancement du domaine.