Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Utiliser la visualization de logiciels pour accomplir certaines tâches comme la détection de défauts de design peut être fastidieux. Les utilisateurs doivent d’abord trouver et configurer un outil de visualization qui est adéquat pour représenter les données à examiner. Souvent, ils sont forcés de naviguer à travers le logiciel manuellement pour accomplir leur tâche. Nous proposons une approche plus simple et efficace. Celle ci s’éloigne de la configuration d’un outil et la navigation manuelle d’un système et se concentre sur la définition écrite de la tâche à accomplir. Suite à cela, notre assistant génère le meilleur outil de visualization et guide les utilisateurs à travers la tâche. Notre approche est constituée de trois éléments principaux, un langage dédié à la description de la tâche d’analyse. Un langage pour définir les visualizations comme des mises en oeuvre du patron modèle-vue-contrôleur. Et un processus de génération pour passer d’une tâche d’analyse à une visualization. En enlevant le besoin de configurer un outil de visualization et en guidant la navigation du système, nous pensons que nous avons fait un outil qui plus simple et rapide à utiliser que ses homologues. / Using software visualization to accomplish certain tasks such as design defect detection can prove tedious. Users first need to find and configure a visualization tool that is adequate for representing the data they want to examine. Then all too often, they are forced to manually navigate the software system in order to complete their task. What we propose is a simpler and more efficient approach that moves the emphasis from configuring a tool and manually navigating the system to writing a definition of the work we want to accomplish. Our goal-driven assistant then generates the best visualization tool and guide us through the navigation of the task. Our approach consists of three main components. The first component is a domain specific language (DSL) to describe analysis tasks. The second component is a language to define the visualizations as customized implementations of the model-view-controller (MVC) pattern. The last component is a generation process used to go from the analysis task to the visualization. By removing the need to configure a visualization tool and guiding the navigation of the system, we believe we made a tool that is simpler and faster to use than its conventional counterparts.

Analyser le code permet de vérifier ses fonctionnalités, détecter des bogues ou améliorer sa performance. L’analyse du code peut être statique ou dynamique. Des approches combinants les deux analyses sont plus appropriées pour les applications de taille industrielle où l’utilisation individuelle de chaque approche ne peut fournir les résultats souhaités. Les approches combinées appliquent l’analyse dynamique pour déterminer les portions à problèmes dans le code et effectuent par la suite une analyse statique concentrée sur les parties identifiées. Toutefois les outils d’analyse dynamique existants génèrent des données imprécises ou incomplètes, ou aboutissent en un ralentissement inacceptable du temps d’exécution. Lors de ce travail, nous nous intéressons à la génération de graphes d’appels dynamiques complets ainsi que d’autres informations nécessaires à la détection des portions à problèmes dans le code. Pour ceci, nous faisons usage de la technique d’instrumentation dynamique du bytecode Java pour extraire l’information sur les sites d’appels, les sites de création d’objets et construire le graphe d’appel dynamique du programme. Nous démontrons qu’il est possible de profiler dynamiquement une exécution complète d’une application à temps d’exécution non triviale, et d’extraire la totalité de l’information à un coup raisonnable. Des mesures de performance de notre profileur sur trois séries de benchmarks à charges de travail diverses nous ont permis de constater que la moyenne du coût de profilage se situe entre 2.01 et 6.42. Notre outil de génération de graphes dynamiques complets, nommé dyko, constitue également une plateforme extensible pour l’ajout de nouvelles approches d’instrumentation. Nous avons testé une nouvelle technique d’instrumentation des sites de création d’objets qui consiste à adapter les modifications apportées par l’instrumentation au bytecode de chaque méthode. Nous avons aussi testé l’impact de la résolution des sites d’appels sur la performance générale du profileur. / Code analysis is used to verify code functionality, detect bugs or improve its performance. Analyzing the code can be done either statically or dynamically. Approaches combining both analysis techniques are most appropriate for industrial-scale applications where each one individually cannot provide the desired results. Blended analysis, for example, first applies dynamic analysis to identify problematic code regions and then performs a focused static analysis on these regions. However, the existing dynamic analysis tools generate inaccurate or incomplete data, or result in an unacceptably slow execution times. In this work, we focus on the generation of complete dynamic call graphs with additional information required for blended analysis. We make use of dynamic instrumentation techniques of Java bytecode to extract information about call sites and object creation sites, and to build the dynamic call graph of the program. We demonstrate that it is possible to profile real-world applications to efficiently extract complete and accurate information. Performance measurement of our profiler on three sets of benchmarks with various workloads places the overhead of our profiler between 2.01 and 6.42. Our profiling tool generating complete dynamic graphs, named dyko, is also an extensible platform for evaluating new instrumentation approaches. We tested a new adaptive instrumentation technique for object creation sites which accommodates instrumentation to the bytecode of each method. We also tested the impact of call sites resolution on the overall performance of the profiler.

Cette thèse s'inscrit dans le domaine de la vérification dulogiciel. Le but de la vérification du logiciel est d'assurer qu'uneimplémentation, un programme, répond aux exigences, satisfait saspécification. Cela est particulièrement important pour le logicielcritique, tel que des systèmes de contrôle d'avions, trains oucentrales électriques, où un mauvais fonctionnement pendantl'opération aurait des conséquences catastrophiques.Les exigences du logiciel peuvent concerner la sûreté ou lefonctionnement. Les exigences de sûreté, tel que l'absence d'accès à lamémoire en dehors des bornes valides, sont souvent implicites, dans lesens que toute implémentation est censée être sûre. D'autre part, les exigences fonctionnelles spécifient ce que leprogramme est censé faire. La spécification d'un programme est souventexprimée informellement en décrivant en anglais la mission d'une partie du code source. La vérification duprogramme se fait alors habituellement par relecture manuelle,simulation et tests approfondis. Par contre, ces méthodes negarantissent pas que tous les possibles cas d'exécution sontcapturés. La preuve déductive de programme est une méthode complète pour assurerla correction du programme. Ici, un programme, ainsi que saspécification formalisée à l'aide d'un langage logique, est un objetmathématique et ses propriétés désirées sont des théorèmes logiques àprouver formellement. De cette façon, si le système logiquesous-jacent est cohérent, on peut être complètement sûr que lapropriété prouvée est valide pour le programme en question et pourn'importe quel cas d'exécution. La génération de conditions de vérification est une techniquecensée aider le programmeur à prouver les propriétés qu'il veut surson programme. Ici, un outil (VCG) analyse un programme donné avec saspécification et produit une formule mathématique, dont la validitéimplique la correction du programme vis à vis de saspécification, ce qui est particulièrement intéressant lorsque lesformules générées peuvent être prouvées automatiquement à l'aide desolveurs SMT. Cette approche, basée sur des travaux de Hoare et Dijkstra,est bien comprise et prouvée correcte en théorie. Des outils devérification déductive ont aujourd'hui acquis une maturité qui leurpermet d'être appliqués dans un contexte industriel où un hautniveau d'assurance est requis. Mais leurs implémentations doiventgérer toute sorte de fonctionnalités des langages et peuvent donc devenir très complexes et contenir des erreurs ellesmêmes - au pire des cas affirmer qu'un programme est correct alorsqu'il ne l'est pas. Il se pose donc la question du niveau de confianceaccordée à ces outils.Le but de cette thèse est de répondre à cette question. Ondéveloppe et certifie, dans le système Coq, un VCGpour des programmes C annotés avec ACSL, le langage logique pour laspécification de programmes ANSI/ISO C.Notre première contribution est la formalisation d'un VCGexécutable pour le langage intermédiaire Whycert, un langageimpératif avec boucles, exceptions et fonctions récursives, ainsi quesa preuve de correction par rapport à la sémantique opérationnelle bloquante à grand pas du langage. Une deuxièmecontribution est la formalisation du langage logique ACSL et lasémantique des annotations ACSL dans Clight de Compcert. De lacompilation de programmes C annotés vers des programmes Whycert et sapreuve de préservation de la sémantique combiné avec uneaxiomatisation en Whycert du modèle mémoire Compcert résulte notrecontribution principale: une chaîne intégrée certifiée pour lavérification de programmes C, basée sur Compcert. En combinant notrerésultat de correction avec celui de Compcert, on obtient un théorèmeen Coq qui met en relation la validité des l'obligations de preuvegénérées avec la sûreté du code assembleur compilé. / This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements, the specification. This is especiallyimportant for critical computer programs, such as control systems forair planes, trains and power plants. Here a malfunctioning occurringduring operation would have catastrophic consequences. Software requirements can concern safety or functioning. Safetyrequirements, such as not accessing memory locations outside validbounds, are often implicit, in the sense that any implementation isexpected to be safe. On the other hand, functional requirementsspecify what the program is supposed to do. The specification of aprogram is often expressed informally by describing in English or someother natural language the mission of a part of the program code.Usually program verification is then done by manual code review,simulation and extensive testing. But this does not guarantee that allpossible execution cases are captured. Deductive program proving is a complete way to ensure soundness of theprogram. Here a program along with its specificationis a mathematical object and its desired properties are logicaltheorems to be formally proved. This way, if the underlying logicsystem is consistent, we can be absolutely sure that the provenproperty holds for the program in any case.Generation of verification conditions is a technique helpingthe programmer to prove the properties he wants about his programs.Here a VCG tool analyses a program and its formal specification andproduces a mathematical formula, whose validity implies the soundnessof the program with respect to its specification. This is particularlyinteresting when the generated formulas can be proved automatically byexternal SMT solvers.This approach is based on works of Hoare and Dijkstra and iswell-understood and shown correct in theory. Deductive verificationtools have nowadays reached a maturity allowing them to be used inindustrial context where a very high level of assurance isrequired. But implementations of this approach must deal with allkinds of language features and can therefore become quite complex andcontain errors -- in the worst case stating that a program correcteven if it is not. This raises the question of the level ofconfidence granted to these tools themselves. The aim of this thesis is to address this question. We develop, inthe Coq system, a certified verification-condition generator (VCG) forACSL-annotated C programs.Our first contribution is the formalisation of an executableVCG for the Whycert intermediate language,an imperative language with loops, exceptions and recursive functionsand its soundness proof with respect to the blocking big-step operational semantics of the language.A second contribution is the formalisation of the ACSL logicallanguage and the semantics of ACSL annotations of Compcert's Clight.From the compilation of ACSL annotated Clight programs to Whycertprograms and its semantics preservation proof combined with a Whycertaxiomatisation of the Compcert memory model results our maincontribution: an integrated certified tool chainfor verification of C~programs on top of Compcert. By combining oursoundness result with the soundness of the Compcert compiler we obtaina Coq theorem relating the validity of the generated proof obligationswith the safety of the compiled assembly code.

Analyser le code permet de vérifier ses fonctionnalités, détecter des bogues ou améliorer sa performance. L’analyse du code peut être statique ou dynamique. Des approches combinants les deux analyses sont plus appropriées pour les applications de taille industrielle où l’utilisation individuelle de chaque approche ne peut fournir les résultats souhaités. Les approches combinées appliquent l’analyse dynamique pour déterminer les portions à problèmes dans le code et effectuent par la suite une analyse statique concentrée sur les parties identifiées. Toutefois les outils d’analyse dynamique existants génèrent des données imprécises ou incomplètes, ou aboutissent en un ralentissement inacceptable du temps d’exécution. Lors de ce travail, nous nous intéressons à la génération de graphes d’appels dynamiques complets ainsi que d’autres informations nécessaires à la détection des portions à problèmes dans le code. Pour ceci, nous faisons usage de la technique d’instrumentation dynamique du bytecode Java pour extraire l’information sur les sites d’appels, les sites de création d’objets et construire le graphe d’appel dynamique du programme. Nous démontrons qu’il est possible de profiler dynamiquement une exécution complète d’une application à temps d’exécution non triviale, et d’extraire la totalité de l’information à un coup raisonnable. Des mesures de performance de notre profileur sur trois séries de benchmarks à charges de travail diverses nous ont permis de constater que la moyenne du coût de profilage se situe entre 2.01 et 6.42. Notre outil de génération de graphes dynamiques complets, nommé dyko, constitue également une plateforme extensible pour l’ajout de nouvelles approches d’instrumentation. Nous avons testé une nouvelle technique d’instrumentation des sites de création d’objets qui consiste à adapter les modifications apportées par l’instrumentation au bytecode de chaque méthode. Nous avons aussi testé l’impact de la résolution des sites d’appels sur la performance générale du profileur. / Code analysis is used to verify code functionality, detect bugs or improve its performance. Analyzing the code can be done either statically or dynamically. Approaches combining both analysis techniques are most appropriate for industrial-scale applications where each one individually cannot provide the desired results. Blended analysis, for example, first applies dynamic analysis to identify problematic code regions and then performs a focused static analysis on these regions. However, the existing dynamic analysis tools generate inaccurate or incomplete data, or result in an unacceptably slow execution times. In this work, we focus on the generation of complete dynamic call graphs with additional information required for blended analysis. We make use of dynamic instrumentation techniques of Java bytecode to extract information about call sites and object creation sites, and to build the dynamic call graph of the program. We demonstrate that it is possible to profile real-world applications to efficiently extract complete and accurate information. Performance measurement of our profiler on three sets of benchmarks with various workloads places the overhead of our profiler between 2.01 and 6.42. Our profiling tool generating complete dynamic graphs, named dyko, is also an extensible platform for evaluating new instrumentation approaches. We tested a new adaptive instrumentation technique for object creation sites which accommodates instrumentation to the bytecode of each method. We also tested the impact of call sites resolution on the overall performance of the profiler.

Le frelatage (ou fuzzing) est l'une des approches les plus efficaces pour la détection de vulnérabilités dans les logiciels de tailles importantes et dont le code source n'est pas disponible. Malgré une utilisation très répandue dans l'industrie, les techniques de frelatage "classique" peuvent avoir des résultats assez limités, et pas toujours probants. Ceci est dû notamment à une faible couverture des programmes testés, ce qui entraîne une augmentation du nombre de faux-négatifs; et un manque de connaissances sur le fonctionnement interne de la cible, ce qui limite la qualité des entrées générées. Nous présentons dans ce travail une approche automatique de recherche de vulnérabilités logicielles par des processus de test combinant analyses avancées de code binaire et frelatage. Cette approche comprend : une technique de minimisation de suite de tests, pour optimiser le rapport entre la quantité de code testé et le temps d'exécution ; une technique d'analyse de couverture optimisée et rapide, pour évaluer l'efficacité du frelatage ; une technique d'analyse statique, pour localiser les séquences de codes potentiellement sensibles par rapport à des patrons de vulnérabilités; une technique dynamique d'analyse de teinte, pour identifier avec précision les zones de l'entrée qui peuvent être à l'origine de déclenchements de vulnérabilités; et finalement une technique évolutionniste de génération de test qui s'appuie sur les résultats des autres analyses, afin d'affiner les critères de décision et d'améliorer la qualité des entrées produites. Cette approche a été mise en œuvre à travers une chaîne d'outils intégrés et évalués sur de nombreuses études de cas fournies par l'entreprise. Les résultats obtenus montrent son efficacité dans la détection automatique de vulnérabilités affectant des applications majeures et sans accès au code source. / Fuzz testing (a.k.a. fuzzing) is one of the most effective approaches for discovering security vulnerabilities in large and closed-source software. Despite their wide use in the software industry, traditional fuzzing techniques suffer from a poor coverage, which results in a large number of false negatives. The other common drawback is the lack of knowledge about the application internals. This limits their ability to generate high quality inputs. Thus such techniques have limited fault detection capabilities. We present an automated smart fuzzing approach which combines advanced binary code analysis techniques. Our approach has five components. A test suite reduction technique, to optimize the ratio between the amount of covered code and the execution time. A fast and optimized code coverage measurement technique, to evaluate the fuzzing effectiveness. A static analysis technique, to locate potentially sensitive sequences of code with respect to vulnerability patterns. An origin-aware dynamic taint analysis technique, to precisely identify the input fields that may trigger potential vulnerabilities. Finally, an evolutionary based test generation technique, to produce relevant inputs. We implemented our approach as an integrated tool chain, and we evaluated it on numerous industrial case studies. The obtained results demonstrate its effectiveness in automatically discovering zero-day vulnerabilities in major closed-source applications. Our approach is relevant to both defensive and offensive security purposes.

Nous proposons une approche basée sur la formulation interactive des requêtes. Notre approche sert à faciliter des tâches d’analyse et de compréhension du code source. Dans cette approche, l’analyste utilise un ensemble de filtres de base (linguistique, structurel, quantitatif, et filtre d’interactivité) pour définir des requêtes complexes. Ces requêtes sont construites à l’aide d’un processus interactif et itératif, où des filtres de base sont choisis et exécutés, et leurs résultats sont visualisés, changés et combinés en utilisant des opérateurs prédéfinis. Nous avons évalués notre approche par l’implantation des récentes contributions en détection de défauts de conception ainsi que la localisation de fonctionnalités dans le code. Nos résultats montrent que, en plus d’être générique, notre approche aide à la mise en œuvre des solutions existantes implémentées par des outils automatiques. / We propose an interactive querying approach for program analysis and comprehension tasks. In our approach, an analyst uses a set of basic filters (linguistic, structural, quantitative, and user selection) to define complex queries. These queries are built following an interactive and iterative process where basic filters are selected and executed, and their results displayed, changed, and combined using predefined operators. We evaluated our querying approach by implementing recent state-of-the-art contributions on feature location and design defect detection. Our results show that, in addition to be generic; our approach helps improving existing solutions implemented by fully-automated tools.

Nous proposons une approche basée sur la formulation interactive des requêtes. Notre approche sert à faciliter des tâches d’analyse et de compréhension du code source. Dans cette approche, l’analyste utilise un ensemble de filtres de base (linguistique, structurel, quantitatif, et filtre d’interactivité) pour définir des requêtes complexes. Ces requêtes sont construites à l’aide d’un processus interactif et itératif, où des filtres de base sont choisis et exécutés, et leurs résultats sont visualisés, changés et combinés en utilisant des opérateurs prédéfinis. Nous avons évalués notre approche par l’implantation des récentes contributions en détection de défauts de conception ainsi que la localisation de fonctionnalités dans le code. Nos résultats montrent que, en plus d’être générique, notre approche aide à la mise en œuvre des solutions existantes implémentées par des outils automatiques. / We propose an interactive querying approach for program analysis and comprehension tasks. In our approach, an analyst uses a set of basic filters (linguistic, structural, quantitative, and user selection) to define complex queries. These queries are built following an interactive and iterative process where basic filters are selected and executed, and their results displayed, changed, and combined using predefined operators. We evaluated our querying approach by implementing recent state-of-the-art contributions on feature location and design defect detection. Our results show that, in addition to be generic; our approach helps improving existing solutions implemented by fully-automated tools.