Search

Minimizing the precision in which the neurons of a neural network compute, is a desirable objective tolimit the resources needed to execute it. This is specially important for neural networks used in embedded systems, which have limited resources (small memories, CPUs performing integer computations, etc.) Unfortunately, neural networks are very sensitive to the precision in which they have been trained and changing this precision, generally degrades the quality of their answers. Using the fixed-point arithmetic, based on integers and integer operations only, remains a good trade-off between the limited resources of embedded systems and the big number of computations of neural networks. However, this arithmetic is difficult to maintain. The management of the fixed-point position must be done manually, unlike the floating-point numbers, where the exponent is managed automatically. In this thesis, we introduce three new techniques to tune the fixed-point formats and synthesize a fixed-point code for a trained neural network, given as input, using integers only and having the same behavior as the initial floating-point network. For that, the number of bits with which each neuron and each synaptic weight is represented, have to be tuned (the smallest format), so the error committed on the outputs of the synthesized neural network, must not exceed an error threshold, chosen by the user. From a technical point of view, we generate a constraint system with integer variables that can be solved by an SMT solver. The solution to this system, if it exists, gives the minimal number of bits required for each neuron and each synaptic weight., Minimiser la précision avec laquelle les neurones d’un réseau de neurones calculent, est un objectifsouhaitable pour limiter les ressources nécessaires à son exécution. Ceci est particulièrement important pour les réseaux de neurones utilisés dans les systèmes embarqués, ayant des ressources limitées (petites mémoires, CPUs effectuant du calcul entier, etc.) Malheureusement, les réseaux de neurones sont très sensibles à la précision avec laquelle ils ont été entraînés et changer cette précision, dégrade généralement la qualité de leurs réponses. L’utilisation de l’arithmétique à virgule fixe, basée sur les entiers et les opérations entières uniquement, reste un bon compromis entre les ressources limitées des systèmes embarqués et les calculs importants des réseaux de neurones. Cependant, cette dernière est difficile à maintenir. La gestion de la virgule fixe doit se faire manuellement contrairement aux flottants, où l’exposant est géré automatiquement. Dans cette thèse, nous introduisons trois nouvelles techniques pour ajuster les formats fixes et synthétiser un code à virgule fixe pour un réseau de neurones entraîné, donné en entrée, utilisant uniquement des entiers et ayant le même comportement que le réseau flottant initial.Pour se faire, le nombre de bits avec lequel est représenté chaque neurone et chaque poids synaptique,doit être ajusté (la plus petite valeur possible), de telle sorte à ce que le nouveau réseau calcule une sortie, où l’erreur commise n’excède pas un seuil d’erreur, choisi par l’utilisateur. D’un point de vue technique, nous générons un système de contraintes avec des variables entières pouvant être résolues par un solveur SMT. La solution à ce système, si elle existe, donnera le nombre de bits minimal requis pour chaque neurone et chaque poids synaptique.expérimenterons notre méthode sur des réseaux de neurones fournis par les partenaires du laboratoire commun SYFI.

Program transformation is an extremely common practice in computer science. From compilation to tests generation, through many approaches of code analysis and formal verification of programs, it is a process that is both ubiquitous and critical to properly functioning programs and information systems. This thesis proposes to study the program transformations mechanisms in order to express and verify syntactical guarantees on the behaviour of these transformations and on their results.Giving a characterisation of the shape of terms returned by such a transformation is, indeed, a common approach to the formal verification of programs. In order to express some properties often used by this type of approaches, we propose in this thesis a formalism inspired by themodel of compilation passes, which are used to describe the general compilation of a program as a sequence of minimal transformations, and based on the notions of pattern matching and term rewriting.This formalism relies on an annotation mechanism of function symbols in order to express a set of specifications describing the behaviours of the associated functions. We then propose a static analysis method in order to check that a transformation, expressed as a term rewritesystem, actually verifies its specifications., La transformation de programmes est une pratique très courante dans le domaine des sciences informatiques. De la compilation à la génération de test en passant par de nombreuses approches d’analyse de codes et de vérification formelle des programmes, c’est un procédé qui est à la fois omniprésent et crucial au bon fonctionnement des programmes et systèmes informatiques. Cette thèse propose une étude formelle des procédures de transformation de programmes dans le but d’exprimer et de garantir des propriétés syntaxiques sur le comportement et les résultats d’unetelle transformation.Dans le contexte de la vérification formelle des programmes, il est en effet souvent nécessaire de pouvoir caractériser la forme des termes obtenus par réduction suivant une telle transformation. En s’inspirant du modèle de passes de compilation, qui décrivent un séquençage de la compilation d’un programme en étapes de transformation minimales n’affectant qu’un petit nombre des constructions du langage, on introduit, dans cette thèse, un formalisme basé sur les notions de filtrage par motif et de réécriture permettant de décrire certaines propriétés couramment induites par ce type de transformations.Le formalisme proposé se repose sur un système d’annotations des symboles de fonction décrivant une spécification du comportement attendu des fonctions associées. On présente alors une méthode d’analyse statique permettant de vérifier que les transformations étudiées, exprimées par un système de réécriture, satisfont en effet ces spécifications.

In recent years, many companies have introduced object-oriented technology into their software development. The paradigm component, which advocates the assembly of autonomous and reusable software bricks, is indeed an interesting proposition to reduce development and maintenance costs while increasing the quality of applications. Whatever development paradigm we find ourselves in, it is essential for both architects and developers to evaluate what they produce in order to produce software that can meet the needs of users, which is why we offer in this article an approach based on the static analysis of the software and the use of some software engineering model to optimize the software and to guarantee its quality., Ces dernières années, de nombreuses entreprises ont introduit la technologie orientée objet dans leurs développements logiciels. Le paradigme composant, qui prône l’assemblage de briques logiciels autonomes et réutilisables, est en effet une proposition intéressante pour diminuer les coûts de développement et de maintenance tout en augmentant la qualité des applications.Quel que soit le paradigme de développement dans lequel on se retrouve, il est essentiel pour les architectes comme pour les développeurs d’évaluer ce qu’ils produisent afin de produire des logiciels capable de répondre aux besoins des utilisateurs, voilà pourquoi nous proposons dans cet article une approche basé sur l’analyse statique du logiciel et l’usage de quelque modèle d’ingénierie logiciel pour optimiser le logiciel et en garantir la qualité.

La réutilisation est une pratique courante lors du développement de logiciel. Bien souvent, cette réutilisation se fait à travers l’utilisation des librairies. Cette dernière met ses fonctionnalités à disposition des développeurs en utilisant les Interfaces de Programmation d’Application (API). En théorie, les développeurs qui utilisent les API n’ont pas forcément besoin de se préoccuper de comment les éléments internes de cette API fonctionnent. En effet, les API mettent leurs fonctionnalités à disposition des développeurs sans forcément dévoiler ce qui se passe à l’interne. Cependant, pour utiliser correctement une API il est nécessaire de respecter des contraintes d’utilisation qui sont à la fois implicites et explicites ainsi que des modèles d’utilisation. L’usage des librairies et des API est très commun dans le domaine du développement de logiciel. Cela permet aux développeurs d’utiliser les fonctionnalités proposées par l’API et ainsi de se concentrer directement sur la tâche qu’ils doivent effectuer. Toutefois, apprendre et se familiariser avec les contraintes d’usage des API sont des tâches ardues et exigent un effort cognitif considérable de la part du développeur. Les chercheurs ont tenté de corriger ce problème en étudiant les modèles d’utilisation et en analysant les traces d’utilisation de code client pour s’assurer de leurs conformités. Néanmoins, les analyses dynamiques ne sont pas possibles pendant les phases précoces de développement du logiciel, car cela requiert une implémentation minimum et l’exécution du code. Nous proposons l’outil Temporal Usage PAttern Checker (Tupac). Une approche basée sur l’analyse statique interprocédural pour vérifier la conformité du code client aux modèles d’utilisation pendant la phase de développement. Tupac peut être déployé dans un envi- ronnement de développement (IDE) et ainsi fournir des informations relatives à l’utilisation des API plus tôt pendant la phase de développement du logiciel. Nous avons évalué notre approche sur quatre projets Java avec quatre API. Les résultats ont démontré que Tupac a une bonne précision et un taux de rappel intéressant. De plus, nous avons pu conclure qu’en moyenne cela prend une demi-seconde pour vérifier la confor- mité d’un patron pour un projet tout entier. Cela démontre que Tupac peut être déployé dans un rythme de codage régulier., In modern software development, reuse takes the form of using libraries that expose their functionality via Application Programming Interfaces (APIs). In theory, APIs allow developers to write client code that reuses library code without needing to know its internals. In practice, correctly using APIs requires respecting explicit and implicit constraints and usage patterns. This allows developers to use functionality proposed by API so that they can focus directly on the task they want to achieve. APIs require a significant effort from the developer to learn various usage constraint. Ignoring such patterns could lead to errors and design flaws. These often cannot be detected prior to integration and system testing. Researchers have attempted to solve this problem by extracting API usage patterns and analyzing client code traces for conformance. However, dynamic analysis is still impossible to perform early without a minimum of integration and execution. We propose the Temporal Usage PAttern Checker (Tupac) for API, an interprocedural static analysis approach that can verify that client code conforms to temporal API usage patterns as it is being developed. Tupac can be deployed inside an Integrated Development Environment (IDE), thus providing developers with feedback about API usage much earlier in the development process. We evaluated the effectiveness of our approach on four projects with four different APIs. Our evaluation shows that Tupac has good precision and interesting recall. Crucially, we also show that it takes, on average, half a second to check an entire project for conformance to a pattern, meaning that it can realistically be deployed in the regular coding rhythm

Nowadays, digital security is of major importance to our societies. Communications, energy, transport, means of production, Internet of Things… The use of digital systems is ever increasing, making them critical to the correct working of our world. A little more than two decades ago, a new form of attack has risen: fault injection. Essentially, it consists in perturbing a circuit during computation, using various methods such as power glitches, electromagnetic injection or laser injection; in the aim of generating errors. These errors can then be exploited by an attacker to reveal secret information from the circuit, or to bypass some security measures.System complexification and technological advances make digital systems particularly vulnerable against fault injection attacks. In order to thwart these attacks effectively and at a reasonable cost, it is necessary to consider security from the early phases of the design flow. To do that, a better understanding of how faults impact processors is required. Effects provoked by fault injection can be modeled at various levels of abstraction. Currently, if the impact of faults at the hardware level is relatively well known, the same cannot be said for the software level. Security analyses at the software level are based on simple software fault models such as instruction skip, register corruption or test inversion. These models are applied without any serious consideration for the microarchitecture of the attacked processor. This brings the question of the realism of these models, leading to two types of problems: some modeled effects do not correspond to actual attacks; and, conversely, some effects lowering the security of the system are not modeled. These issues then translate to over-engineered, or, worse, under-engineered countermeasures.To face the limitations of typical software fault models, a precise study of processor microarchitectures is necessary. In this thesis, we first explore how various structures of the processor, such as the pipeline or optimization structures like forwarding and speculative execution, can influence the behavior of faults in the inner working of the processor; and how they call into question a pure software vision of how faults impact software execution. RTL injections are conducted in a RISC-V processor, to demonstrate how these effects could be exploited to counter typical software countermeasures and a hardened program that check PIN codes. Then, a method to study more generally the effects of faults in a processor is developed. The point of this method is twofold. The first is about modeling faults at the software level, with the definition of several metrics to evaluate models. The second point is about keeping a link to the RTL level, in order to be able to materialize effects obtained at the software level. Finally, to end this thesis, we study the possibility to use static analysis to analyze the security of programs against software fault models defined previously. Two methods are considered, one using abstract interpretation, and the other using symbolic execution.This thesis, financed by the IRT Nanoelec for the Pulse project, has been conducted within the LCIS laboratory in Valence, in collaboration with the CEA-Leti in Grenoble. It has been supervised by Vincent Beroulle (LCIS), and co-supervised by Christophe Deleuze (LCIS) and Florian Pebay-Peyroula (CEA-Leti)., La sécurité numérique est aujourd’hui un enjeu majeur dans nos sociétés. Communications, énergie, transport, outils de production, Internet des Objets… Les systèmes numériques se multiplient et deviennent toujours plus critiques pour le bon fonctionnement du monde. Depuis un peu plus d’une vingtaine d’années, une nouvelle menace a émergé pour attaquer les systèmes : l’injection de faute. Elle consiste essentiellement à perturber un circuit pendant son fonctionnement, par diverses méthodes comme des perturbations sur l’alimentation du circuit, l’injection électromagnétique, ou l’injection laser ; afin de provoquer des erreurs. Ces erreurs peuvent ensuite être exploitées par un attaquant pour révéler des informations secrètes du circuit, ou passer outre des mesures de sécurité.La complexification des systèmes numériques et les avancées technologiques comme la finesse de gravure rendent particulièrement vulnérables les systèmes numériques face aux attaques par injection de fautes. Pour contrer ces attaques efficacement et à un coût raisonnable, il est nécessaire de penser la sécurité dès la phase de conception du système. Pour cela, il faut comprendre précisément l’impact de ces fautes sur les processeurs. Les effets induits peuvent être modélisés à différents niveaux d’abstraction. Actuellement, si l’impact des fautes est relativement bien connu au niveau matériel, leurs effets au niveau logiciel restent mal compris. Les analyses de vulnérabilité au niveau logiciel se basent donc sur des modèles de faute logiciels simples que sont par exemple le saut d’instruction, la corruption de registre ou l’inversion de test. Ces modèles sont appliqués sans réelle prise en compte de la microarchitecture du processeur attaqué. Cette non-considération de l’aspect matériel pose la question du réalisme des modèles logiciels, qui conduit à deux types de problèmes : certains effets modélisés ne correspondent pas à des vulnérabilités réelles ; et, à l’inverse, certains effets affaiblissant la sécurité ne sont pas modélisés. Ces difficultés se transposent ensuite dans des contremesures sur-dimensionnées, ou, plus grave, sous-dimensionnées.Pour lutter contre ces limitations des modèles de faute logiciels usuels, une étude précise de la microarchitecture des processeurs est requise. Dans cette thèse, nous explorons tout d’abord en quoi différentes structures du processeur, comme le pipeline ou les optimisations de forwarding et d’exécution spéculative, peuvent influer sur le comportement des fautes au sein du processeur et en quoi ces structures peuvent mettre à mal une vision purement logicielle de l’impact des fautes sur l’exécution d’un programme. Des injections au niveau RTL dans un processeur d’architecture RISC-V sont effectuées pour montrer que ces effets pourraient être exploités pour attaquer des contremesures logicielles typiques, ou encore une application de vérification de PIN sécurisée. Dans un deuxième temps est développée une méthode pour étudier plus généralement les effets des fautes dans un processeur. Cette méthode a un intérêt double. Le premier est la modélisation de fautes au niveau logiciel, avec notamment la définition de métriques d’évaluation des modèles. Le second est de conserver un lien avec le niveau RTL afin de pouvoir concrétiser les effets obtenus au niveau logiciel. Pour terminer cette thèse, nous étudions la possibilité d’utiliser des méthodes d’analyse statique pour analyser la sécurité de programmes face aux modèles de faute logiciels définis précédemment. Une analyse par interprétation abstraite et une analyse par exécution symbolique sont abordées.Cette thèse, financée par l’IRT Nanoelec pour le projet Pulse, a été réalisée au sein du laboratoire LCIS de Valence, en collaboration avec le CEA-Leti de Grenoble. Elle a été dirigée par Vincent Beroulle (LCIS) et co-encadrée par Christophe Deleuze (LCIS) et Florian Pebay-Peyroula (CEA-Leti).

Arbitrary-precision integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software or computer algebra systems. GMP is a very widely-used arbitrary-precision integer arithmetic library. It features state-of-the-art algorithms that are intricate enough that their formal verification is both justified and difficult. This thesis tackles the formal verification of the functional correctness of a large fragment of GMP using the Why3 deductive verification platform.In order to make this verification possible, I have made several additions to Why3 that enable the verification of C programs. Why3 features a functional programming and specification language called WhyML. I have developed models of the memory management and datatypes of the C language, allowing me to reimplement GMP's algorithms in WhyML and formally verify them. I have also extended Why3's extraction mechanism so that WhyML programs can be compiled to idiomatic C code, where only OCaml used to be supported.The compilation of my WhyML algorithms results in a verified C library called WhyMP. It implements many state-of-the-art algorithms from GMP, with almost all of the optimization tricks preserved. WhyMP is compatible with GMP and performance-competitive with the assembly-free version. It goes far beyond existing verified arbitrary-precision arithmetic libraries, and is arguably the most ambitious existing Why3 development in terms of size and proof effort.In an attempt to increase the degree of automation of my proofs, I have also added to Why3 a framework for proofs by reflection. It enables Why3 users to easily write dedicated decision procedures that are formally verified programs and make full use of WhyML's imperative features. Using this new framework, I was able to replace hundreds of handwritten proof annotations in my GMP verification by automated proofs., Les algorithmes d'arithmétique entière en précision arbitraire sont utilisés dans des contextes où leur correction et leurs performances sont critiques, comme les logiciels de cryptographie ou de calcul formel. GMP est une bibliothèque d'arithmétique entière en précision arbitraire très utilisée. Elle propose des algorithmes de pointe, suffisamment complexes pour qu'il soit à la fois justifié et difficile de les vérifier formellement. Cette thèse traite de la vérification formelle de la correction fonctionnelle d'une partie significative de GMP à l'aide de la plateforme de vérification déductive Why3.Afin de rendre cette preuve possible, j'ai fait plusieurs ajouts à Why3 qui permettent la vérification de programmes C. Why3 propose un langage fonctionnel de programmation et de spécification appelé WhyML. J'ai développé des modèles de la gestion de la mémoire et des types du langage C. Ceci m'a permis de réimplanter des algorithmes de GMP en WhyML et de les vérifier formellement. J'ai aussi étendu le mécanisme d'extraction de Why3. Les programmes WhyML peuvent maintenant être compilés vers du C idiomatique, alors que le seul langage cible était OCaml auparavant. La compilation de mes programmes WhyML résulte en une bibliothèque C vérifiée appelée WhyMP. Elle implémente de nombreux algorithmes de pointe tirés de GMP en préservant presque toutes les astuces d'implémentation. WhyMP est compatible avec GMP, et est comparable à la version de GMP sans assembleur écrit à la main en termes de performances. Elle va bien au-delà des bibliothèques d'arithmétique en précision arbitraire vérifiées existantes. C'est sans doute le développement Why3 le plus ambitieux à ce jour en termes de longueur et d'effort de preuve. Afin d'augmenter le degré d'automatisation de mes preuves, j'ai ajouté à Why3 un mécanisme de preuves par réflexion. Il permet aux utilisateurs de Why3 d'écrire des procédures de décision dédiées, formellement vérifiées et qui utilisent pleinement les fonctionnalités impératives de WhyML. À l'aide de ce mécanisme, j'ai pu remplacer des centaines d'annotations manuelles de ma preuve de GMP par des preuves automatiques.

Les outils de programmation sont des programmes informatiques qui aident les humains à programmer des ordinateurs. Les outils sont de toutes formes et tailles, par exemple les éditeurs, les compilateurs, les débogueurs et les profileurs. Chacun de ces outils facilite une tâche principale dans le flux de travail de programmation qui consomme des ressources cognitives lorsqu’il est effectué manuellement. Dans cette thèse, nous explorons plusieurs outils qui facilitent le processus de construction de systèmes intelligents et qui réduisent l’effort cognitif requis pour concevoir, développer, tester et déployer des systèmes logiciels intelligents. Tout d’abord, nous introduisons un environnement de développement intégré (EDI) pour la programmation d’applications Robot Operating System (ROS), appelé Hatchery (Chapter 2). Deuxièmement, nous décrivons Kotlin∇, un système de langage et de type pour la programmation différenciable, un paradigme émergent dans l’apprentissage automatique (Chapter 3). Troisièmement, nous proposons un nouvel algorithme pour tester automatiquement les programmes différenciables, en nous inspirant des techniques de tests contradictoires et métamorphiques (Chapter 4), et démontrons son efficacité empirique dans le cadre de la régression. Quatrièmement, nous explorons une infrastructure de conteneurs basée sur Docker, qui permet un déploiement reproductible des applications ROS sur la plateforme Duckietown (Chapter 5). Enfin, nous réfléchissons à l’état actuel des outils de programmation pour ces applications et spéculons à quoi pourrait ressembler la programmation de systèmes intelligents à l’avenir (Chapter 6)., Programming tools are computer programs which help humans program computers. Tools come in all shapes and forms, from editors and compilers to debuggers and profilers. Each of these tools facilitates a core task in the programming workflow which consumes cognitive resources when performed manually. In this thesis, we explore several tools that facilitate the process of building intelligent systems, and which reduce the cognitive effort required to design, develop, test and deploy intelligent software systems. First, we introduce an integrated development environment (IDE) for programming Robot Operating System (ROS) applications, called Hatchery (Chapter 2). Second, we describe Kotlin∇, a language and type system for differentiable programming, an emerging paradigm in machine learning (Chapter 3). Third, we propose a new algorithm for automatically testing differentiable programs, drawing inspiration from techniques in adversarial and metamorphic testing (Chapter 4), and demonstrate its empirical efficiency in the regression setting. Fourth, we explore a container infrastructure based on Docker, which enables reproducible deployment of ROS applications on the Duckietown platform (Chapter 5). Finally, we reflect on the current state of programming tools for these applications and speculate what intelligent systems programming might look like in the future (Chapter 6).

Any software bug or device malfunction in safety-critical systems can have catastrophicconsequences. The validation and analysis of programs in critical systems is of paramountimportance to guarantee that the software satisfies its specification and that it is devoidedof runtime errors.Static program analysis by abstract interpretation computes a sound approximationof the set of reachable states of a program. It discovers invariant properties of programswhich are represented by elements of an abstract domain. Most industrial static analysistools do not use expressive relational numerical abstract domains like convex polyhedradue to their computational cost.We propose a new modular analysis for the automatic discovery of numerical propertiesbased on the computation of disjunctive relational summaries of procedures. Proceduresummaries are computed once and for all, and used to compute the effect of procedurecalls, in a bottom-up fashion. Our approach is especially applied to improve the scalabilityof Linear Relation Analysis, or abstract interpretation with convex polyhedra, althoughit is based on a more general framework usable with any relational abstract domain.Disjunctive relational summaries are finite sets of abstract input-output relations represented by elements of a relational abstract domain. They are computed based on apartitioning of procedure preconditions. We give heuristics to compute an abstract partition of a procedure precondition. We also give ways to improve the precision of summarycomputation, notably through a careful treatment of preconditions during analysis. Ourapproach also applies to recursive procedures where summaries are computed recursivelyin terms of themselves.We implemented our approach in a new static analysis platform for C programs calledmars. We conducted experiments on programs from the Mälardalen benchmark showingthat our approach can significantly reduce the analysis time for Linear Relation Analysiscompared to a full context-sensitive analysis where procedures are analyzed completelyin each call context. Analysis precision is not significantly damaged and can even beimproved due to the use of disjunction.In a second part, we present an approach for the modular analysis of reactive systems for numerical properties. We propose a flexible representation of the behavior ofreactive components called Relational Mode Automata (RMA), which allows the analysisof reactive systems behavior at various levels of abstraction. RMA can be constructedautomatically from disjunctive summaries of the procedures implementing componentreactions. The analysis results of individual components using RMA can be reused toanalyze larger reactive systems with multiple component instantiations in a modular way.We give an application of this approach to the analysis of a simplified automated subwaycontrol system., La présence de bugs ou de dysfonctionnements dans les systèmes critiques peut avoirdes conséquences terribles. La validation et l’analyse des programmes embarqués dans lessystèmes critiques est d’une importance majeure pour garantir que les logiciels présentssoient conformes à leur spécification et dépourvus d’erreurs à l’exécution.L’analyse statique par interprétation abstraite calcule une approximation sûre del’ensemble des états accessibles d’un programme. Elle permet de découvrir des propriétésinvariantes des programmes en les représentant par des éléments d’un domaine abstrait.Les domaines abstraits numériques, comme le domaine des octogones ou des polyèdresconvexes, ont des niveaux de précision différents. Les outils industriels d’analyse statiquen’utilisent généralement pas les domaines abstraits numériques les plus expressifs, commele domaine des polyèdres convexes, à cause de la complexité de leurs opérations.Nous présentons dans cette thèse une analyse modulaire des programmes pour ladécouverte de propriétés numériques, basée sur le calcul de résumés disjonctifs et relationnels de procédures. Les résumés de chaque procédure sont calculés de manière ascendante (bottom-up) et utilisés dans l’analyse de l’effet des appels de procédure. Bien quenotre approche soit appliquée à l’analyse de relations linéaires, ou interprétation abstraitepolyédrique, pour améliorer son passage à l’échelle, elle est définie dans un cadre pluslarge applicable à n’importe quel domaine abstrait relationnel.Les résumés disjonctifs de procédures sont des ensembles finis de relations d’entrée-sortie représentées par des éléments d’un domaine abstrait relationnel. Ils sont calculésen utilisant un partitionnement de la précondition d’une procédure. Nous proposonsdes heuristiques pour calculer des partitions de préconditions. Nous présentons aussi desaméliorations concernant la précision du calcul des résumés, notamment grâce à un traite-ment particulier des préconditions. Notre approche s’applique également aux procéduresrécursives, où les résumés sont calculés en fonction d’eux-mêmes.Notre analyse modulaire à été implémentée dans un nouvel outil d’analyse statiquepour les programmes C, appelé mars. Nos expérimentations montrent que notre approchepeut réduire significativement le temps d’analyse pour l’analyse des relations linéaires, parcomparaison avec une analyse classique qui analyse les procédures dans chaque contexted’appel. La précision des résultats n’est pas considérablement diminuée et peut mêmeêtre améliorée grâce à l’usage de la disjonction dans les résumés.Dans une seconde partie, nous présentons une approche pour l’analyse modulaire dessystèmes réactifs. Nous proposons une représentation flexible des composants réactifs appelée Automates Relationnels de Mode, ou Relational Mode Automata (RMA), permettantune analyse des systèmes réactifs à différents niveaux d’abstraction. Les automates relationnels de mode peuvent être construits automatiquement à partir des résumés disjonctifsdes procédures implémentant la réaction de chaque composant. Les résultats de l’analysede chaque composant peuvent être réutilisés dans l’analyse de systèmes réactifs de plusgrande taille où chaque composant peut être instancié plusieurs fois. Cette approche estappliquée à l’analyse d’un système simplifié de contrôle d’un réseau de métro.

Recent years have seen an increase of heterogeneous architectures combining multi-core CPUs with accelerators such as GPU, FPGA, and Intel Xeon Phi. GPU can achieve significant performance for certain categories of application. Nevertheless, achieving this performance with low-level APIs (e.g. CUDA, OpenCL) requires to rewrite the sequential code, to have a good knowledge of GPU architecture, and to apply complex optimizations that are sometimes not portable. On the other hand, directive-based programming models (e.g. OpenACC, OpenMP) offer a high-level abstraction of the underlying hardware, thus simplifying the code maintenance and improving productivity. They allow users to accelerate their sequential codes on GPU by simply inserting directives. OpenACC/OpenMP compilers have the daunting task of applying the necessary optimizations from the user-provided directives and generating efficient codes that take advantage of the GPU architecture. Although the OpenACC / OpenMP compilers are mature and able to apply some optimizations automatically, the generated code may not achieve the expected speedup as the compilers do not have a full view of the whole application. Thus, there is generally a significant performance gap between the codes accelerated with OpenACC/OpenMP and those hand-optimized with CUDA/OpenCL. To help programmers for speeding up efficiently their legacy sequential codes on GPU with directive-based models and broaden OpenMP/OpenACC impact in both academia and industry, several research issues are discussed in this dissertation. We investigated OpenACC and OpenMP programming models and proposed an effective application parallelization methodology with directive-based programming approaches. Our application porting experience revealed that it is insufficient to simply insert OpenMP/OpenACC offloading directives to inform the compiler that a particular code region must be compiled for GPU execution. It is highly essential to combine offloading directives with loop parallelization constructs. Although current compilers are mature and perform several optimizations, the user may provide them more information through loop parallelization constructs clauses in order to get an optimized code. We have also revealed the challenge of choosing good loop schedules. The default loop schedule chosen by the compiler may not produce the best performance, so the user has to manually try different loop schedules to improve the performance. We demonstrate that OpenMP and OpenACC programming models can achieve best performance with lesser programming effort, but OpenMP/OpenACC compilers quickly reach their limit when the offloaded region code is computed/memory bound and contain several nested loops. In such cases, low-level languages may be used. We also discuss pointers aliasing problem in GPU codes and propose two static analysis tools that perform automatically at source level type qualifier insertion and scalar promotion to solve aliasing issues., L'utilisation d'architectures hétérogènes, combinant des processeurs multicoeurs avec des accélérateurs tels que les GPU, FPGA et Intel Xeon Phi, a augmenté ces dernières années. Les GPUs peuvent atteindre des performances significatives pour certaines catégories d'applications. Néanmoins, pour atteindre ces performances avec des API de bas niveau comme CUDA et OpenCL, il est nécessaire de réécrire le code séquentiel, de bien connaître l’architecture des GPUs et d’appliquer des optimisations complexes, parfois non portables. D'autre part, les modèles de programmation basés sur des directives (par exemple, OpenACC, OpenMP) offrent une abstraction de haut niveau du matériel sous-jacent, simplifiant ainsi la maintenance du code et améliorant la productivité. Ils permettent aux utilisateurs d’accélérer leurs codes séquentiels sur les GPUs en insérant simplement des directives. Les compilateurs d'OpenACC/OpenMP ont la lourde tâche d'appliquer les optimisations nécessaires à partir des directives fournies par l'utilisateur et de générer des codes exploitant efficacement l'architecture sous-jacente. Bien que les compilateurs d'OpenACC/OpenMP soient matures et puissent appliquer certaines optimisations automatiquement, le code généré peut ne pas atteindre l'accélération prévue, car les compilateurs ne disposent pas d'une vue complète de l'ensemble de l'application. Ainsi, il existe généralement un écart de performance important entre les codes accélérés avec OpenACC/OpenMP et ceux optimisés manuellement avec CUDA/OpenCL. Afin d'aider les programmeurs à accélérer efficacement leurs codes séquentiels sur GPU avec les modèles basés sur des directives et à élargir l'impact d'OpenMP/OpenACC dans le monde universitaire et industrielle, cette thèse aborde plusieurs problématiques de recherche. Nous avons étudié les modèles de programmation OpenACC et OpenMP et proposé une méthodologie efficace de parallélisation d'applications avec les approches de programmation basées sur des directives. Notre expérience de portage d'applications a révélé qu'il était insuffisant d'insérer simplement des directives de déchargement OpenMP/OpenACC pour informer le compilateur qu'une région de code particulière devait être compilée pour être exécutée sur la GPU. Il est essentiel de combiner les directives de déchargement avec celles de parallélisation de boucle. Bien que les compilateurs actuels soient matures et effectuent plusieurs optimisations, l'utilisateur peut leur fournir davantage d'informations par le biais des clauses des directives de parallélisation de boucle afin d'obtenir un code mieux optimisé. Nous avons également révélé le défi consistant à choisir le bon nombre de threads devant exécuter une boucle. Le nombre de threads choisi par défaut par le compilateur peut ne pas produire les meilleures performances. L'utilisateur doit donc essayer manuellement différents nombres de threads pour améliorer les performances. Nous démontrons que les modèles de programmation OpenMP et OpenACC peuvent atteindre de meilleures performances avec un effort de programmation moindre, mais les compilateurs OpenMP/OpenACC atteignent rapidement leur limite lorsque le code de région déchargée a une forte intensité arithmétique, nécessite un nombre très élevé d'accès à la mémoire globale et contient plusieurs boucles imbriquées. Dans de tels cas, des langages de bas niveau doivent être utilisés. Nous discutons également du problème d'alias des pointeurs dans les codes GPU et proposons deux outils d'analyse statiques qui permettent d'insérer automatiquement les qualificateurs de type et le remplacement par scalaire dans le code source.

The certification of real-time safety critical programs requires bounding their execution time. Due to the high impact of cache memories on memory access latency, modern Worst-Case Execution Time estimation tools include a cache analysis. The aim of this analysis is to statically predict if memory accesses result in a cache hit or a cache miss. This problem is undecidable in general, thus usual cache analyses perform some abstractions that lead to precision loss. One common assumption made to remove the source of undecidability is that all execution paths in the program are feasible. Making this hypothesis is reasonable because the safety of the analysis is preserved when adding spurious paths to the program model. However, classifying memory accesses as cache hits or misses is still hard in practice under this assumption, and efficient cache analysis usually involve additional approximations, again leading to precision loss. This thesis investigates the possibility of performing an optimally precise cache analysis under the common assumption that all execution paths in the program are feasible.We formally define the problems of classifying accesses as hits and misses, and prove that they are NP-hard or PSPACE-hard for common replacement policies (LRU, FIFO, NMRU and PLRU). However, if these theoretical complexity results legitimate the use of additional abstraction, they do not preclude the existence of algorithms efficient in practice on industrial workloads.Because of the abstractions performed for efficiency reasons, cache analyses can usually classify accesses as Unknown in addition to Always-Hit (Must analysis) or Always-Miss (May analysis). Accesses classified as Unknown can lead to both a hit or a miss, depending on the program execution path followed. However, it can also be that they belong to one of the Always-Hit or Always-Miss category and that the cache analysis failed to classify them correctly because of a coarse approximation. We thus designed a new analysis for LRU instruction that is able to soundly classify some accesses into a new category, called Definitely Unknown, that represents accesses that can lead to both a hit or a miss. For those accesses, one knows for sure that their classification does not result from a coarse approximation but is a consequence of the program structure and cache configuration. By doing so, we also reduce the set of accesses that are candidate for a refined classification using more powerful and more costly analyses.Our main contribution is an analysis that can perform an optimally precise analysis of LRU instruction caches. We use a method called block focusing that allows an analysis to scale by only analyzing one cache block at a time. We thus take advantage of the low number of candidates for refinement left by our Definitely Unknown analysis. This analysis produces an optimal classification of memory accesses at a reasonable cost (a few times the cost of the usual May and Must analyses).We evaluate the impact of our precise cache analysis on the pipeline analysis. Indeed, when the cache analysis is not able to classify an access as Always-Hit or Always-Miss, the pipeline analysis must consider both cases. By providing a more precise memory access classification, we thus prune the state space explored by the pipeline analysis and hence the WCET analysis time.Aside from this application of precise cache analysis to WCET estimation, we investigate the possibility of using the Definitely Unknown analysis in the domain of security. Indeed, caches can be used as side-channel to extract some sensitive data from a program execution, and we propose a variation of our Definitely Unknown analysis to help a developer finding the source of some information leakage., Dans le cadre des systèmes critiques, la certification de programmes temps-réel nécessite de borner leur temps d’exécution. Les mémoires caches impactant fortement la latence des accès mémoires, les outils de calcul de pire temps d’exécution incluent des analyses de cache. Ces analyses visent à prédire statiquement si ces accès aboutissent à des cache-hits ou des cache-miss. Ce problème étant indécidable en général, les analyses de caches emploient des abstractions pouvant mener à des pertes de précision. Une hypothèse habituelle pour rendre le problème décidable consiste à supposer que toutes les exécutions du programme sont réalisables. Cette hypothèse est raisonnable car elle ne met pas en cause la validité de l’analyse : tous les véritables chemins d’exécutions du programme sont couverts par l’analyse. Néanmoins, la classification des accès mémoires reste difficile en pratique malgré cette hypothèse, et les analyses de cache efficaces utilisent des approximations supplémentaires. Cette thèse s’intéresse à la possibilité de réaliser des analyses de cache de précision optimale sous l’hypothèse que tous les chemins sont faisables.Les problèmes de classification d’accès mémoires en hits et miss y sont définis formellement et nous prouvons qu’ils sont NP-difficiles, voire PSPACE-difficiles, pour les politiques de remplacement usuelles (LRU, FIFO, NMRU et PLRU). Toutefois, si ces résultats théoriques justifient l’utilisation d’abstractions supplémentaires, ils n’excluent pas l’existence d’un algorithme efficace en pratique pour des instances courantes dans l’industrie.Les abstractions usuelles ne permettent pas, en général, de classifier tous les accès mémoires en Always-Hit et Always-Miss. Certains sont alors classifiés Unknown par l’analyse de cache, et peuvent aboutir à des cache-hits comme à des cache-miss selon le chemin d’exécution emprunté. Cependant, il est aussi possible qu’un accès soit classifié comme Unknown alors qu’il mène toujours à un hit (ou un miss), à cause d’une approximation trop grossière. Nous proposons donc une nouvelle analyse de cache d’instructions LRU, capable de classifier certains accès comme Definitely Unknown, une nouvelle catégorie représentant les accès pouvant mener à un hit ou à un miss. On est alors certain que la classification de ces accès est due au programme et à la configuration du cache, et pas à une approximation peu précise. Par ailleurs, cette analyse réduit le nombre d’accès candidats à une reclassification par des analyses plus précises mais plus coûteuses.Notre principale contribution est une analyse capable de produire une classification de précision optimale. Celle-ci repose sur une méthode appelée block focusing qui permet le passage à l’échelle en analysant les blocs de cache un par un. Nous profitons ainsi de l’analyse Definitely Unknown, qui réduit le nombre de candidats à une classification plus précise. Cette analyse précise produit alors une classification optimale pour un coût raisonnable (proche du coût des analyses usuelles May et Must).Nous étudions également l’impact de notre analyse exacte sur l’analyse de pipeline. En effet, lorsqu’une analyse de cache ne parvient pas à classifier un accès comme Always-Hit ou Always-Miss, les deux cas (hit et miss) sont envisagés par l’analyse de pipeline. En fournissant une classification plus précise des accès mémoires, nous réduisons donc la taille de l’espace d’états de pipeline exploré, et donc le temps de l’analyse.Par ailleurs, cette thèse étudie la possibilité d’utiliser l’analyse Definitely Unknown dans le domaine de la sécurité. Les mémoires caches peuvent être utilisées comme canaux cachés pour extraire des informations de l’exécution d’un programme. Nous proposons une variante de l’analyse Definitely Unknown visant à localiser la source de certaines fuites d’information.

With the rising complexity of the underlying computer hardware, the analysis of the timing behavior of real-time software is becoming more and more complex and imprecise. Time-predictable computer architectures thus have been proposed to provide hardware support for timing analysis. The goal is to deliver tighter worst-case execution time (WCET) estimates while keeping the analysis overhead minimal. These estimates are typically provided by standalone WCET analysis tools. The emergence of time-predictable architectures is, however, quite recent. While several designs have been introduced, efforts are still needed to assess their effectiveness in actually enhancing the worst-case performance. For many time-predictable hardware, timing analysis is either non-existing or lacking proper support. Consequently, time-predictable architectures are barely supported in existing WCET analysis tools. The general contribution of this thesis is to help filling this gap and turning some opportunities into concrete advantages. For this, we take interest in the Patmos processor. The already existing support around Patmos allows for an effective exploration of techniques to enhance the worst-case performance. Main contributions include: (1) Handling of predicated execution in timing analysis, (2) Comparison of the precision of stack cache occupancy analyses, (3) Analysis of preemption costs for the stack cache, (4) Preemption mechanisms for the stack cache, and (5) Prefetching-like technique for the stack cache. In addition, we present our WCET analysis tool Odyssey, which implements timing analyses for Patmos., En raison de la complexité croissante des architectures matérielles, l'analyse temporelle du logiciel temps-réel devient de plus en plus complexe et imprécise. Les architectures prédictibles des ordinateurs ont donc été proposées afin d'assurer un support matériel dédié à analyse temporelle. The but est de fournir des estimations plus précises de pire-temps d'exécution de programmes (WCET), tout en gardant le coût et la compexité de l'analyse minimal. Ces estimations proviennent typiquement d'outils dédiés à l'analyse WCET. L'émergence de ces architectures spécialisées est, toutefois, assez récent. Bien que plusieurs designs d'architectures ont été proposés, des efforts sont encore nécessaires pour évaluer leurs capacités à améliorer les performances pire cas. Pour plusieurs composants matériels prédictibles, l'analyse temporelle est manquante ou partiellement supportée. En conséquence, les architectures prédictibles sont à peine supportées dans les outils d’analyse WCET existants. Dans cette thèse, nous nous intéressons au processeur prédictible Patmos. Le support existant autour de la plateforme permet une exploration effective des techniques d'optimisation pour les performances pire cas. Les principales contributions comprennent: (1) Une gestion des prédicats dans le flux d'anayse WCET, (2) Une comparaison de la précision des analyses d'occupancy pour le stack cache, (3) Une analyse des coûts de préemption pour le stack cache, (4) Des mécanismes de préemption pour le stack cache, et (5) Des techniques de prefetching pour le stack cache. En outre, nous présentons Odyssey -- notre outil d'analyse WCET pour le processeur Patmos.

Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Relational analyses offer several advantages, such as their ability to infer semantics properties more expressive compared to state analyses. Moreover, they offer the ability to make the analysis compositional, using input-output relations as summaries for procedures, which is an advantage for scalability. In the case of numeric programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input-output memory states and taking shapes into account is challenging. In this Thesis, we propose a set of novel logical connectives to describe such relations, which rely on separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory is modified (and how). Using these connectives, we build an abstract domain and design a compositional static analysis by abstract interpretation that over-approximates relations over memory states containing inductive structures. We implement this approach as a plug-in of the FRAMA-C analyzer. We evaluate it on small programs written in C that manipulate singly linked lists and binary trees, but also on a bigger program that consists of a part of Emacs. The experimental results show that our approach allows us to infer more expressive semantic properties than states analyses, from a logical point of view. It is also much faster on programs with an important number of function calls without losing precision., Les analyses statiques ont pour but d’inférer des propriétés sémantiques de programmes. Nous distinguons deux importantes classes d’analyses statiques : les analyses d’états et les analyses relationnelles. Alors que les analyses d’états calculent une sur-approximation de l’ensemble des états atteignables d’un programme, les analyses relationnelles calculent des propriétés fonctionnelles entre les états d’entrée et les états de sortie d’un programme. Les analyses relationnelles offrent plusieurs avantages, comme leur capacité à inférer des propriétés sémantiques plus expressives par rapport aux analyses d’états. De plus, elles offrent également la possibilité de rendre l’analyse compositionnelle, en utilisant les relations entrée-sortie comme des résumés de procédures, ce qui est un avantage pour le passage à l’échelle. Dans le cas des programmes numériques, plusieurs analyses ont été proposées qui utilisent des domaines abstraits numériques relationnels, pour décrire des relations. D’un autre côté, modéliser des abstractions de relations entre les états mémoires entrée-sortie tout en prenant en compte les structures de données est difficile. Dans cette Thèse, nous proposons un ensemble de nouveaux connecteurs logiques, reposant sur la logique de séparation, pour décrire de telles relations. Ces connecteurs peuvent exprimer qu’une certaine partie de la mémoire est inchangée, fraîchement allouée, ou désallouée, ou que seulement une seule partie de la mémoire est modifiée (et de quelle manière). En utilisant ces connecteurs, nous construisons un domaine abstrait relationnel et nous concevons une analyse statique compositionnelle par interprétation abstraite qui sur-approxime des relations entre des états mémoires contenant des structures de données inductives. Nous avons implémenté ces contributions sous la forme d’un plug-in de l’analyseur FRAMA-C. Nous en avons évalué l’impact sur l’analyse de petits programmes écrits en C manipulant des listes chaînées et des arbres binaires, mais également sur l’analyse d’un programme plus conséquent qui consiste en une partie du code source d’Emacs. Nos résultats expérimentaux montrent que notre approche permet d’inférer des propriétés sémantiques plus expressives d’un point de vue logique que des analyses d’états. Elle se révèle aussi beaucoup plus rapide sur des programmes avec un nombre conséquent d’appels de fonctions sans pour autant perdre en précision.

Scientific applications have an increasing need of resources and many grand scientific challenges require exascale compute capabilities to be addressed. One major concern to achieve exascale is programmability. New automatic methods are required to fill the gap between developers of scientific applications and HPC experts. In addition, as scientific applications are becoming more and more complex and are supposed to run at extreme scale, new tools are required to assist developers in the debugging phase of application development. This thesis explores the combination of static and dynamic methods to improve programmability of HPC applications. Two major issues are investigated: the complexity of programming heterogeneous architectures and the prevention of deadlocks in parallel programs.The first part of this thesis investigates the automatic task adaptation for heterogeneous architectures. More precisely, we propose a new method to improve programmability of heterogeneous architectures. The programmer expresses the parallelism of his application through a sequence of OpenCL tasks without considering issues related to the underlying architecture where its code will be executed. Then our method automatically partitions the tasks into sub-tasks executed by each device and handles load balancing between the devices to take full advantage of the machine capabilities.The second part of this thesis investigates the automatic detection and prevention of deadlocks in parallel programs. We propose a novel static analysis to precisely detect execution paths in parallel programs potentially leading to deadlocks. This static analysis is then combined with a dynamic instrumentation of the code to automatically prevent deadlocks at runtime.The solutions proposed in this thesis have been tested and validated on real parallel applications., Les applications de calcul scientifique ont besoin de ressources de calcul de plus en plus importantes et beaucoup de grands challenges scientifiques exigent des capacités de calcul Exascale (10 puissance 18 calculs par seconde) pour être relevés. L’un des principaux obstacles pour atteindre l’Exascale est la difficulté de programmer les architectures parallèles actuelles. De nouvelles méthodes automatiques sont nécessaires pour combler l’écart entre les développeurs d’applications scientifiques et les experts en calcul haute performance. De plus, les applications scientifiques devenant de plus en plus complexes et étant supposées s’exécuter à très large échelle, de nouveaux outils sont nécessaires pour aider les développeurs lors de la phase de débogage des programmes. Cette thèse explore la combinaison de méthodes statiques et dynamiques pour faciliter la programmation des applications de calcul haute performance. Deux enjeux majeurs sont étudiés : faciliter la programmation des architectures hétérogènes et prévenir les interblocages dans les programmes parallèles.La première partie de cette thèse s’intéresse à l’adaptation automatique des tâches de calcul aux architectures hétérogènes. Nous proposons une nouvelle méthode pour faciliter la programmation des architectures hétérogènes composées de plusieurs unités de calcul (CPUs et GPUs). Le programmeur exprime le parallélisme de son application sous forme de tâches OpenCL sans se soucier des problèmatiques liées à l’architecture sur laquelle son code sera exécuté. Ensuite notre méthode partitionne automatiquement chaque tâche en sous-tâches et équilibre la charge de travail entre les unités de calcul afin de tirer pleinement avantage de toutes les ressources de calcul de la machine.La deuxième partie de cette thèse porte sur la détection automatique des interblocages dans les programmes parallèles. Nous proposons une nouvelle analyse statique permettant de détecter précisément les chemins d’exécution menant à des interblocages dans les programmes parallèles. Cette analyse statique est ensuite combinée à une instrumentation dynamique du code afin de prévenir les interblocages à l’exécution.Les solutions proposées dans cette thèse ont été testée et validées sur des cas réels d’applications parallèles.

Les calculs en nombres flottants sont intensivement utilisés dans divers domaines, notamment les systèmes embarqués critiques. En général, les résultats de ces calculs sont perturbés par les erreurs d’arrondi. Dans un scenario critique, ces erreurs peuvent être accumulées et propagées, générant ainsi des dommages plus ou moins graves sur le plan humain, matériel, financier, etc. Il est donc souhaitable d’obtenir les résultats les plus précis possibles lorsque nous utilisons l’arithmétique flottante. Pour remédier à ce problème, l’outil Salsa [7] permet d’améliorer la précision des calculs en corrigeant partiellement ces erreurs d’arrondi par une transformation automatique et source à source des programmes. La principale contribution de ce travail consiste à analyser, à étudier si l’optimisation par dépliage de boucles améliore plus la précision numérique des calculs dans le programme initial. À cours terme, on souhaite définir un facteur de dépliage de boucles, c’est à dire, trouver quand est-ce qu’il est pertinent de déplier la boucle dans le programme.

In the beginning of the third millennium we are witnessing a new age. This new age is characterized by the shift from an industrial economy to an economy based on information technology. It is the Information Age. Today, we rely on software in practically every aspect of our life. Information technology is used by all economic actors: manufactures, governments, banks, universities, hospitals, retail stores, etc. A single software vulnerability can lead to devastating consequences and irreparable damage. The situation is worsened by the software becoming larger and more complex making the task of avoiding software flaws more and more difficult task. Automated tools finding those vulnerabilities rapidly before it is late, are becoming a basic need for software industry community. This thesis is investigating security vulnerabilities occurring in C language applications. We searched the sources of these vulnerabilities with a focus on C library functions calling. We dressed a list of property checks to detect code portions leading to security vulnerabilities. Those properties give for a library function call the conditions making this call a source of a security vulnerability. When these conditions are met the corresponding call must be reported as vulnerable. These checks were implemented in Carto-C tool and experimented on the Juliet test base and on real life application sources. We also investigated the detection of exploitable vulnerability at binary code level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns by exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our tool Vyper and experimented successfully on Juliet test base and real life application binaries.level. We started by defining what an exploitable vulnerability behavioral patterns are. The focus was on the most exploited vulnerability classes such as stack buffer overflow, heap buffer overflow and use-after-free. After, a new method on how to search for this patterns exploring application execution paths is proposed. During the exploration, necessary information is extracted and used to find the patterns of the searched vulnerabilities. This method was implemented in our Vyper tool and experimented successfully on Juliet test base and real life application binaries, Dans ce début du troisième millénium, nous sommes témoins d'un nouvel âge. Ce nouvel âge est caractérisé par la transition d'une économie industrielle vers une économie basée sur la technologie de l'information. C'est l’âge de l'information. Aujourd’hui le logiciel est présent dans pratiquement tous les aspects de notre vie. Une seule vulnérabilité logicielle peut conduire à des conséquences dévastatrices. La détection de ces vulnérabilités est une tâche qui devient de plus en plus dure surtout avec les logiciels devenant plus grands et plus complexes. Dans cette thèse, nous nous sommes intéressés aux vulnérabilités de sécurité impactant les applications développées en langage C et particulièrement les vulnérabilités provenant de l'usage des fonctions de ce langage. Nous avons proposé une liste de vérifications pour la détection des portions de code causant des vulnérabilités de sécurité. Ces vérifications sont sous la forme de conditions rendant l'appel d'une fonction vulnérable. Des implémentations dans l'outil Carto-C et des expérimentations sur la base de test Juliet et les sources d'applications réelles ont été réalisées. Nous nous sommes également intéressés à la détection de vulnérabilités exploitables au niveau du code binaire. Nous avons défini en quoi consiste le motif comportemental d'une vulnérabilité. Nous avons proposé une méthode permettant de rechercher ces motifs dans les traces d'exécutions d'une application. Le calcul de ces traces d'exécution est effectué en utilisant l'exécution concolique. Cette méthode est basée sur l'annotation de zones mémoires sensibles et la détection d'accès dangereux à ces zones. L'implémentation de cette méthode a été réalisée dans l'outil Vyper et des expérimentations sur la base de test Juliet et les codes binaires d'applications réelles ont été menées avec succès

Shape analyses rely on expressive families of logical properties to infer complex structural invariants, such that memory safety, structure preservation and other memory properties of programs dealing with dynamic data structures can be automatically verified. Many such analyses manipulate abstract memory states that consist of separating conjunctions of basic predicates describing atomic blocks or summary predicates that describe unbounded heap regions like lists or trees using inductive definitions. Moreover, they use finite disjunctions of abstract memory states in order to take into account dissimilar shapes. Although existing analyses enable local reasoning of memory regions, they do, however, have the following issues: (1) The summary predicates are not expressive enough to describe precisely all the dynamic data structures. In particular, a fairly large number of data structures with unbounded sharing, such as graphs, cannot be described inductively in a local manner; (2) Abstract operations that read or write into summaries rely on materialization of memory cells. The materialization operation in general creates new disjunctions, yet the size of disjunctions should be kept small for the sake of efficiency. However, local predicates are not enough to determine the right set of disjuncts that should be clumped together and to define precise abstract join and widen operations. In this thesis, we study separating conjunction-based shape predicates and the related abstract operations, in particular, abstract joining and widening operations that lead to critical modifications of abstract states. We seek a lightweight way to enable some global reasoning in existing shape analyses such that shape predicates are more expressive for abstracting data structures with unbounded sharing and disjuncts can be clumped precisely and efficiently. We propose a shape abstraction based on set variables that when integrated with inductive definitions enables the specification and shape analysis of structures with unbounded sharing. We implemented the shape analysis domain by combining a separation logic-based shape abstract domain of the MemCAD analyzer and a set abstract domain, where the set abstractions are used to track unbounded pointer sharing properties. Based on this abstract domain, we analyzed a group of programs dealing with adjacency lists of graphs. We design a general semantic criterion to clump abstract memory states based on their silhouettes that express global shape properties, \ie, clumping abstract states when their silhouettes are similar. Silhouettes apply not only to the conservative union of disjuncts but also to the weakening of separating conjunctions of memory predicates into inductive summaries. Our approach allows us to define union and widening operators that aim at preserving the case splits that are required for the analysis to succeed. We implement this approach in the MemCAD analyzer and evaluate it on real-world C libraries for different data structures, including doubly-linked lists, red-black trees, AVL-trees and splay-trees. The experimental results show that our approach is able to keep the size of disjunctions small for scalability and preserve case splits that takes into account dissimilar shapes for precision., L'analyse statique des programmes permet de calculer automatiquement des propriétés sémantiques valides pour toutes les exécutions. En particulier, dans le cas des programmes manipulant des structures de données complexes en mémoire, l'analyse statique peut inférer des invariants utiles pour prouver la sûreté des accès à la mémoire ou la préservation d'invariants structurels. Beaucoup d'analyses de ce type manipulent des états mémoires abstraits représentés par des conjonctions en logique de séparation dont les prédicats de base décrivent des blocs de mémoire atomiques ou bien résument des régions non-bornées de la mémoire telles que des listes ou des arbres. De telles analyses utilisent souvent des disjonctions finies d’états mémoires abstraits afin de mieux capturer leurs dissimilarités. Les analyses existantes permettent de raisonner localement sur les zones mémoires mais présentent les inconvénients suivants: (1) Les prédicats inductifs ne sont pas assez expressifs pour décrire précisément toutes les structures de données dynamiques, du fait de la présence de pointeurs vers des parties arbitraires (i.e., non-locales) de ces structures ; (2) Les opérations abstraites correspondant à des accès en lecture ou en écriture sur ces prédicats inductifs reposent sur une opération matérialisant les cellules mémoires correspondantes. Cette opération de matérialisation crée en général de nouvelles disjonctions, ce qui nuit à l'impératif d'efficacité. Hélas, les prédicats exprimant des contraintes de structure locale ne sont pas suffisants pour déterminer de façon adéquate les ensembles de disjonctions devant être fusionnés, ni pour définir les opérations d'union et d'élargissement d'états abstraits. Cette thèse est consacrée à l'étude et la mise au point de prédicats en logique de séparation permettant de décrire des structures de données dynamiques, ainsi que des opérations abstraites afférentes. Nous portons une attention particulière aux opérations d'union et d'élargissement d’états abstraits. Nous proposons une méthode pratique permettant de raisonner globalement sur ces états mémoires au sein des méthodes existantes d'analyse de propriétés structurelles et autorisant la fusion précise et efficace de disjonctions. Nous proposons et implémentons une abstraction structurelle basée sur les variables d'ensembles qui lorsque elle est utilisée conjointement avec les prédicats inductifs permet la spécification et l'analyse de propriétés structurelles globales. Nous avons utilisé ce domaine abstrait afin d'analyser une famille de programmes manipulant des graphes représentés par liste d'adjacence. Nous proposons un critère sémantique permettant de fusionner les états mémoires abstraits similaires en se basant sur leur silhouette, cette dernière représentant certaines propriétés structurelles globales vérifiées par l'état correspondant. Les silhouettes s'appliquent non seulement à la fusion de termes dans les disjonctions d'états mémoires mais également à l'affaiblissement de conjonctions de prédicats de logique de séparation en prédicats inductifs. Ces contributions nous permettent de définir des opérateurs d’union et d'élargissement visant à préserver les disjonctions requises pour que l'analyse se termine avec succès. Nous avons implémenté ces contributions au sein de l'analyseur MemCAD et nous en avons évaluées l'impact sur l'analyse de bibliothèques existantes écrites en C et implémentant différentes structures de données, incluant des listes doublement chaînées, des arbres rouge-noir, des arbres AVL et des arbres "splay". Nos résultats expérimentaux montrent que notre approche est à même de contrôler la taille des disjonctions à des fins de performance sans pour autant nuire à la précision de l'analyse.

We study the static analysis on both numeric and structural properties of array contents in the framework of abstract interpretation. Since arrays are ubiquitous in most software systems, and software defects related to mis-uses of arrays are hard to avoid in practice, a lot of efforts have been devoted to ensuring the correctness of programs manipulating arrays. Current verification of these programs by static analysis focuses on numeric content properties. However, in some lowlevel programs (like embedded systems or real-time operating systems), arrays often contain structural data (e.g., lists) without using dynamic allocation. In this manuscript, we present a series of techniques to verify both numeric and structural properties of array contents. Our first technique is used to describe properties of numerical stores with optional values (i.e., where some variables may have no value) or sets of values (i.e., where some variables may store a possibly empty set of values). Our approach lifts numerical abstract domains based on common linear inequality into abstract domains describing stores with optional values and sets of values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded memory blocks like in arrays. Our second technique is an abstract domain which utilizes semantic properties to split array cells into groups. Cells with similar properties will be packed into groups and abstracted together. Additionally, groups are not necessarily contiguous. Compared to conventional array partitioning analyses that split arrays into contiguous partitions to infer properties of sets of array cells. Our analysis can group together non-contiguous cells when they have similar properties. Our abstract domain can infer complex array invariants in a fully automatic way. The third technique is used to combine different shape domains. This combination locally ties summaries in both abstract domains and is called a coalesced abstraction. Coalescing allows to define efficient and precise static analysis algorithms in the combined domain. We utilize it to combine our array abstraction (i.e., our second technique) and a shape abstraction which captures linked structures with separation logicbased inductive predicates. The product domain can verify both safety and functional properties of programs manipulating arrays storing dynamically linked structures, such as lists. Storing dynamic structures in arrays is a programming pattern commonly used in low-level systems, so as to avoid relying on dynamic allocation. The verification of such programs is very challenging as it requires reasoning both about the array structure with numeric indexes and about the linked structures stored in the array. Combining the three techniques that we have proposed, we can build an automatic static analysis for the verification of programs manipulating arrays storing linked structures. We report on the successful verification of several operating system kernel components and drivers., Dans cette thèse, nous étudions l'analyse statique par interprétation abstraites de programmes manipulant des tableaux, afin d'inférer des propriétés sur les valeurs numériques et les structures de données qui y sont stockées. Les tableaux sont omniprésents dans de nombreux programmes, et les erreurs liées à leur manipulation sont difficile à éviter en pratique. De nombreux travaux de recherche ont été consacrés à la vérification de tels programmes. Les travaux existants s'intéressent plus particulièrement aux propriétés concernant les valeurs numériques stockées dans les tableaux. Toutefois, les programmes bas-niveau (comme les systèmes embarqués ou les systèmes d'exploitation temps réel) utilisent souvent des tableaux afin d'y stocker des structures de données telles que des listes, de manière à éviter d'avoir recours à l'allocation de mémoire dynamique. Dans cette thèse, nous présentons des techniques permettant de vérifier par interprétation abstraite des propriétés concernant à la fois les données numériques ainsi que les structures composites stockées dans des tableaux. Notre première contribution est une abstraction qui permet de décrire des stores à valeurs numériques et avec valeurs optionnelles (i.e., lorsqu'une variable peut soit avoir une valeur numérique, soit ne pas avoir de valeur du tout), ou bien avec valeurs ensemblistes (i.e., lorsqu'une variable est associée à un ensemble de valeurs qui peut être vide ou non). Cette abstraction peut être utilisée pour décrire des stores où certaines variables ont un type option, ou bien un type ensembliste. Elle peut aussi servir à la construction de domaines abstraits pour décrire des propriétés complexes à l'aide de variables symboliques, par exemple, pour résumer le contenu de zones dans des tableaux. Notre seconde contribution est un domaine abstrait pour la description de tableaux, qui utilise des propriétés sémantiques des valeurs contenues afin de partitionner les cellules de tableaux en groupes homogènes. Ainsi, des cellules contenant des valeurs similaires sont décrites par les mêmes prédicats abstraits. De plus, au contraire des analyses de tableaux conventionnelles, les groupes ainsi formés ne sont pas nécessairement contigüs, ce qui contribue à la généralité de l'analyse. Notre analyse peut regrouper des cellules non-congitües, lorsque celles-ci ont des propriétés similaires. Ce domaine abstrait permet de construire des analyses complètement automatiques et capables d'inférer des invariants complexes sur les tableaux. Notre troisième contribution repose sur une combinaison de cette abstraction des tableaux avec différents domaines abstraits issus de l'analyse de forme des structures de données et reposant sur la logique de séparation. Cette combinaison appelée coalescence opère localement, et relie des résumés pour des structures dynamiques à des groupes de cellules du tableau. La coalescence permet de définir de manière locale des algorithmes d'analyse statique dans le domaine combiné. Nous l'utilisons pour relier notre domaine abstrait pour tableaux et une analyse de forme générique, dont la tâche est de décrire des structures chaînées. L'analyse ainsi obtenue peut vérifier à la fois des propriétés de sûreté et des propriétés de correction fonctionnelle. De nombreux programmes bas-niveau stockent des structures dynamiques chaînées dans des tableaux afin de n'utiliser que des zones mémoire allouées statiquement. La vérification de tels programmes est difficile, puisqu'elle nécessite à la fois de raisonner sur les tableaux et sur les structures chaînées. Nous construisons une analyse statique reposant sur ces trois contributions, et permettant d'analyser avec succés de tels programmes. Nous présentons des résultats d'analyse permettant la vérification de composants de systèmes d'exploitation et pilotes de périphériques.

In this paper we present an implementation in the Session Initiation Protocol (SIP). After a functional analysis of the SIP protocol and based on the work of researchers from an Italian university (University of parma-Italy) to acquire adequate libraries for the development of our communication tool. To optimize the code and improve the prototype with us, in an incremental approach, test techniques on a static analysis based on the evaluation of the complexity of the software with the application of metrics and the cyclomatic number of Mccabe., Dans cet article nous présentons une implémentation en java de la vidéo téléphonie grâce au protocole SIP (Session Initiation Protocol). Après une analyse fonctionnelle du protocole SIP et en se basant sur des travaux des chercheurs d'une université italienne (University of parma-Italy) pour se doter des librairies adéquates pour un développement de notre outil de communication. Afin d'optimiser le code et d'améliorer le prototype nous nous sommes servis, dans une démarche incrémentale, des techniques de test basées sur une analyse statique reposant sur l'évaluation de la complexité du logiciel avec l'application de métriques et le nombre cyclomatique de Mccabe.

In this paper we present an implementation in the Session Initiation Protocol (SIP). After a functional analysis of the SIP protocol and based on the work of researchers from an Italian university (University of parma-Italy) to acquire adequate libraries for the development of our communication tool. To optimize the code and improve the prototype with us, in an incremental approach, test techniques on a static analysis based on the evaluation of the complexity of the software with the application of metrics and the cyclomatic number of Mccabe., Dans cet article nous présentons une implémentation en java de la vidéo téléphonie grâce au protocole SIP (Session Initiation Protocol). Après une analyse fonctionnelle du protocole SIP et en se basant sur des travaux des chercheurs d'une université italienne (University of parma-Italy) pour se doter des librairies adéquates pour un développement de notre outil de communication. Afin d'optimiser le code et d'améliorer le prototype nous nous sommes servis, dans une démarche incrémentale, des techniques de test basées sur une analyse statique reposant sur l'évaluation de la complexité du logiciel avec l'application de métriques et le nombre cyclomatique de Mccabe.

In recent years, many companies have introduced object-oriented technology into their software development. The paradigm component, which advocates the assembly of autonomous and reusable software bricks, is indeed an interesting proposition to reduce development and maintenance costs while increasing the quality of applications. Whatever development paradigm we find ourselves in, it is essential for both architects and developers to evaluate what they produce in order to produce software that can meet the needs of users, which is why we offer in this article an approach based on the static analysis of the software and the use of some software engineering model to optimize the software and to guarantee its quality., Ces dernières années, de nombreuses entreprises ont introduit la technologie orientée objet dans leurs développements logiciels. Le paradigme composant, qui prône l’assemblage de briques logiciels autonomes et réutilisables, est en effet une proposition intéressante pour diminuer les coûts de développement et de maintenance tout en augmentant la qualité des applications.Quel que soit le paradigme de développement dans lequel on se retrouve, il est essentiel pour les architectes comme pour les développeurs d’évaluer ce qu’ils produisent afin de produire des logiciels capable de répondre aux besoins des utilisateurs, voilà pourquoi nous proposons dans cet article une approche basé sur l’analyse statique du logiciel et l’usage de quelque modèle d’ingénierie logiciel pour optimiser le logiciel et en garantir la qualité.

The search for an upper bound of the execution time of a program is an essential part of the verification of real-time critical systems. The execution times of the programs of such systems generally vary a lot, and it is difficult, or impossible, to predict the range of the possible times. Instead, it is better to look for an approximation of the Worst-Case Execution Time (WCET). A crucial requirement of this estimate is that it must be safe, that is, it must be guaranteed above the real WCET. Because we are looking to prove that the system in question terminates reasonably quickly, an overapproximation is the only acceptable form of approximation. The guarantee of such a safety property could not sensibly be done without static analysis, as a result based on a battery of tests could not be safe without an exhaustive handling of test cases. Furthermore, in the absence of a certified compiler (and tech- nique for the safe transfer of properties to the binaries), the extraction of properties must be done directly on binary code to warrant their soundness. However, this approximation comes with a cost : an important pessimism, the gap between the estimated WCET and the real WCET, would lead to superfluous extra costs in hardware in order for the system to respect the imposed timing requirements. It is therefore important to improve the precision of the WCET by reducing this gap, while maintaining the safety property, as such that it is low enough to not lead to immoderate costs. A major cause of overestimation is the inclusion of semantically impossible paths, said infeasible paths, in the WCET computation. This is due to the use of the Implicit Path Enumeration Technique (IPET), which works on an superset of the possible execution paths. When the Worst-Case Execution Path (WCEP), corresponding to the estimated WCET, is infeasible, the precision of that estimation is negatively affected. In order to deal with this loss of precision, this thesis proposes an infeasible paths detection technique, enabling the improvement of the precision of static analyses (namely for WCET estimation) by notifying them of the infeasibility of some paths of the program. This information is then passed as data flow properties, formatted in the FFX portable annotation language, and allowing the communication of the results of our infeasible path analysis to other analyses., La recherche d'une borne supérieure au temps d'exécution d'un programme est une partie essentielle du processus de vérification de systèmes temps-réel critiques. Les programmes de tels systèmes ont généralement des temps d'exécution variables et il est difficile, voire impossible, de prédire l'ensemble de ces temps possibles. Au lieu de cela, il est préférable de rechercher une approximation du temps d'exécution pire-cas ou Worst-Case Execution Time (WCET). Une propriété cruciale de cette approximation est qu'elle doit être sûre, c'est-à-dire qu'elle doit être garantie de majorer le WCET. Parce que nous cherchons à prouver que le système en question se termine en un temps raisonnable, une surapproximation est le seul type d'approximation acceptable. La garantie de cette propriété de sûreté ne saurait raisonnablement se faire sans analyse statique, un résultat se basant sur une série de tests ne pouvant être sûr sans un traitement exhaustif des cas d'exécution. De plus, en l'absence de certification du processus de compilation (et de transfert des propriétés vers le binaire), l'extraction de propriétés doit se faire directement sur le code binaire pour garantir leur fiabilité. Toutefois, cette approximation a un coût : un pessimisme - écart entre le WCET estimé et le WCET réel - important entraîne des surcoûts superflus de matériel pour que le système respecte les contraintes temporelles qui lui sont imposées. Il s'agit donc ensuite, tout en maintenant la garantie de sécurité de l'estimation du WCET, d'améliorer sa précision en réduisant cet écart de telle sorte qu'il soit suffisamment faible pour ne pas entraîner des coûts supplémentaires démesurés. Un des principaux facteurs de surestimation est la prise en compte de chemins d'exécution sémantiquement impossibles, dits infaisables, dans le calcul du WCET. Ceci est dû à l'analyse par énumération implicite des chemins ou Implicit Path Enumeration Technique (IPET) qui raisonne sur un surensemble des chemins d'exécution. Lorsque le chemin d'exécution pire-cas ou Worst-Case Execution Path (WCEP), correspondant au WCET estimé, porte sur un chemin infaisable, la précision de cette estimation est négativement affectée. Afin de parer à cette perte de précision, cette thèse propose une technique de détection de chemins infaisables, permettant l'amélioration de la précision des analyses statiques (dont celles pour le WCET) en les informant de l'infaisabilité de certains chemins du programme. Cette information est passée sous la forme de propriétés de flot de données formatées dans un langage d'annotation portable, FFX, permettant la communication des résultats de notre analyse de chemins infaisables vers d'autres analyses. Les méthodes présentées dans cette thèse sont inclues dans le framework OTAWA, développé au sein de l'équipe TRACES à l'IRIT. Elles usent elles-mêmes d'approximations pour représenter les états possibles de la machine en différents points du programme.

This thesis addresses the problem of proving the safety of systems described by non-linear dynamical models and hybrid dynamical models. A system is said to be safe if all trajectories of its state do not reach an unsafe region. Proving the safety of systems by explicitly computing all its trajectories when its dynamic is non-linear or when its behavior is described by an hybrid model with non-linear dynamics remains a challenging task. This thesis considers the barrier function approach to prove the safety of a system. A barrier function, when it exists, partitions the state space and isolates the trajectories of the system starting from any possible initial values of the state and the unsafe part of the state space. The set of constraints, which have to be satisfied by a barrier function are usually non-convex, rendering the search of satisfying barrier functions hard. Previously, only polynomial barrier functions were taken in consideration and for systems with polynomial dynamics. This thesis considers relatively general dynamical systems with generic non-linear barrier functions. The solutions presented are based on template barrier functions, constraint satisfaction problems, and interval analysis. The first part of the thesis focuses on non-linear dynamical systems. The barrier function design problem is formulated as a constraint satisfaction problem that can be solved using tools from interval analysis. This formulation allows one to prove the safety of a non-linear dynamical system by finding the parameters of a template barrier function such that all constraints are satisfied using the FPS-CSC algorithm, which has been adapted and supplemented with contractors to improve its efficiency. The second part of the thesis is dedicated to the design of barrier functions for systems described by hybrid dynamical models. Safety properties have to be proven during the continuous-time evolution of the system, but also during transitions. This leads to additional constraints that have to be satisfied by candidate barrier functions. Solving all the constraints simultaneously to find all the barrier functions is usually computationally intractable. In the proposed approach, the algorithm explores all the locations sequentially. Transition constraints are introduced progressively between the already explored locations. Backtracking to previous location is considered when transition constraints are not satisfied. The efficiency of the proposed approaches has been compared with state-of-the-art solutions., Cette thèse développe des outils permettant de prouver qu’un système dynamique est sûr. En supposant qu’une partie de l’espace d’état est dangereuse, un système dynamique est dit sûr lorsque son état n’atteint jamais cette partie dangereuse au cours du temps, quel que soit l’état initial appartenant à un ensemble d’états initiaux admissibles et quel que soit le niveau de perturbation restant dans un domaine admissible. Les outils proposés cherchent à établir des preuves de sûreté pour des systèmes décrits par des modèles dynamiques non-linéaires et des modèles dynamiques hybrides. Prouver qu’un système dynamique est sûr en calculant explicitement l’ensemble des trajectoires possibles du système lorsque le modèle dynamique est non-linéaire et perturbé reste une tâche très difficile. C’est pourquoi cette thèse aborde ce problème à l’aide de fonctions barrières paramétrées. Une barrière, lorsqu’elle existe, permet de partitionner l’espace d’état et d’isoler l’ensemble des trajectoires possibles de l’état du système de la partie dangereuse de l’espace d’état. La fonction paramétrique décrivant la barrière doit satisfaire un certain nombre de contraintes impliquant la dynamique du modèle, l’ensemble des états initiaux possibles, et l’ensemble dangereux. Ces contraintes ne sont pas convexes en général, ce qui complique la recherche de fonctions barrières satisfaisantes. Précédemment, seules des fonctions barrières polynomiales ont été considérées pour des modèles dynamiques polynomiaux. Cette thèse considère des systèmes dynamiques relativement généraux avec des barrières paramétriques quelconques. Les solutions présentées exploitent des outils de satisfaction de contraintes sur des domaines continus et des outils issus de l’analyse par intervalles. Dans un premier temps, cette thèse considère des systèmes dynamiques non-linéaires à temps continu. Le problème de conception d’une barrière paramétrique est formulé comme un problème de satisfaction des contraintes sur des domaines réels avec des variables quantifiées de manière existentielle et universelle. L’algorithme CSC-FPS a été adapté afin de résoudre le problème de synthèse de barrière. Cet algorithme combine une exploration de l’espace des paramètres de la barrière et une phase de vérification des propriétés de la barrière. A l’aide de contracteurs, il est possible de significativement accélérer la recherche de solutions. Dans un second temps, ces résultats sont étendus au cas de systèmes décrits par des modèles dynamiques hybrides. La propriété de sûreté doit être prouvée lors de l’évolution à temps continu du système dynamique, mais aussi pendant les transitions du système. Ceci nécessite l’introduction de contraintes supplémentaires qui lient les fonctions barrières associées à chaque mode à temps continu entre elles. Réaliser la synthèse de toutes les fonctions barrières pour les différents modes simultanément n’est envisageable que pour des systèmes de très petite dimension avec peu de modes. Une approche séquentielle a été proposée. Les contraintes liées aux transitions sont introduites progressivement entre les modes pour lesquels une barrière a déjà été obtenue. Lorsque certaines contraintes de transition ne sont pas satisfaites, une méthode de backtracking doit être mise en œuvre afin de synthétiser des barrières offrant une meilleure prise en compte des contraintes de transition non satisfaites. Ces approches ont été évaluées et comparées avec des techniques de l’état de l’art sur des systèmes décrits par des modèles à temps continu et des modèles hybrides.

National audience; Golo est un langage dynamique construit autour de l’instruction "invokedynamic" de la machine virtuelle Java. Originellement développé au laboratoire CITI de l’INSA de Lyon par le groupe Dynamid, Golo est open-source et dédié à la réalisation d’applications dynamiques.L’objectif de ce stage est de pouvoir augmenter la confiance que l’on peut avoir en un programme Golo. L’approche retenue est d’utiliser l’outil Why3 développé par l’équipe Toccata de l’INRIA/LRI/CNRS, originellement conçu pour la vérification de programmes en C, Java et Ada. En s’appuyant sur le travail fait par le plugin Krakatoa pour analyser du code Java avec cet outil, une traduction du code Golo vers du code WhyML exécutable a été implémentée dans le compilateur Golo. Cette implémentation vise à poser une base pour pouvoir analyser statiquement du code Golo avec Why3, ainsi que pour faire des vérifications statiques lors de la traduction. La spécification dans le code Golo devait originellement se faire dans un langage inspiré de JML, cependant l’approche implémentée permet au programmeur de spécifier le code Golo dans le langage de spécification de Why3 directement. Le détail de la mé- thode d’implémentation, des fonctionnalités supportées ainsi que des limitations sera abordé dans une partie ultérieure.

Distributed databases take advantage of replication to bring data close to the client, and to always be available. the primary challenge for such databases is to ensure consistency. recent research provide hybrid consistency models that allow the database supports asynchronous updates by default, but synchronisation is available upon request. to help programmers exploit the hybrid consistency model, we propose a set of useful patterns,proof rules, and tool for proving integrity invariants of applications. in the first part, we study a sound proof rule that enables programmers to check whether the operations of a given application semantics maintain the application invariants under a given amount of parallelism. we have developed a smt-based tool that automates this proof, and verified several example applications using the tool. in the second part, we apply the above methodology to the design of a replicated file system.the main invariant is that the directory structure forms a tree. we study three alternative semantics for the file system. each exposes a different amount of parallelism, and different anomalies. using our tool-assisted rules, we check whether a specific file system semantics maintains the tree invariant, and derive an appropriate consistency protocol. in the third part of this thesis, we present three classes of invariants: equivalence, partial order, and single-item generic. each places some constraints over the state. each of these classes maps to a different storage-layer consistency property: respectively, atomicity, causal ordering, or total ordering., Afin d'assurer disponibilité et réactivité, de nombreux systèmes distribués reposent sur des bases de données répliquées qui maintiennent des copies (répliques) des données sur différents serveurs. la cohérence constitue un défi important dans la mise en oeuvre des bases de données répliquées. les concepteurs de bases de données repliquées doivent faire un choix difficile entre une cohérence forte, qui guarantit une large gamme d'invariants applicatifs, mais qui est lente et fragile, et une réplication asynchrone, qui assure un bon niveau de disponibilité et de réactivité, mais laisse le programmeur face à de possibles anomalies liées à la concurrence.pour résoudre ce dilemme, des bases de données commerciales et recherche fournissent une cohérence hybride qui permet au programmeur d'exiger une cohérence forte pour certaines opérations, et d'ainsi permettre une synchronisation.cette thèse étudie l'analyse et la mise en oeuvre d'une application et de la cohérence associée, de manière à assurer les invariants de cette application avec un minimum d'exigences de cohérence. les trois principales contributions de cette thèse sont: 1) nous proposons le premier outil d'analyse statique destiné à prouver la validité d'invariants d'applications de base de données à modèle de cohérence hybride. 2) nous présentons la mise en application de notre outil d'analyse dans le cadre de la conception d'un système de fichiers dont la sémantique permet un comportement similaire à posix et à un coût résonable. 3)nous proposons un ensemble de patterns utiles, susceptibles d'aider les développeurs d'application dans l'implémentation d'invariants les plus communs.

Designers of a replicated database face a vexing choice between strong consistency, which ensures certain application invariants but is slow and fragile, and asynchronous replication, which is highly available and responsive, but exposes the programmer to unfamiliar behaviours. To bypass this conundrum, recent research has studied hybrid consistency models, in which updates are asynchronous by default, but synchronisation is available upon request. To help programmers exploit hybrid consistency, we propose the first static analysis tool for proving integrity invariants of applications using databases with hybrid consistency models. This allows a programmer to find minimal consistency guarantees sufficient for application correctness.; La conception d’une base de données répliquées fait face à un choix difficile, entre la cohérence forte, qui garantit certains invariants applicatifs mais reste lente et fragile, et la réplication asynchrone qui est hautement disponible mais expose le programmeur à des comportements inattendus. Pour dépasser cet embarras, des recherches récentes portent sur des modèles de cohérence hybrides, dans lesquels les mises à jour sont asynchrones par défaut, mais les mécanismes de synchronisation sont disponibles sur demande. Afin d’aider les programmeurs à exploiter la cohérence hybride, nous proposons le premier outil statique capable de prouver les invariants d’intégrité d’applications utilisant une base de donnée à cohérence hybride. Ceci permet au programmeur de trouver les garanties de cohérence minimales garantissant que l’application est correcte.

This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1, Cette thèse porte sur l'analyse statique de code par typage dans le but de détecter les erreurs dans les programmes avant leur exécution. Plus précisément, nous nous intéressons ici au domaine du sous-typage, dans lequel les propriétés du code sont représentées par des ensemble de contraintes de la forme (t1

Les calculs en nombres flottants sont intensivement utilisés dans divers domaines, notamment les systèmes embarqués critiques. En général, les résultats de ces calculs sont perturbés par les erreurs d’arrondi. Dans un scenario critique, ces erreurs peuvent être accumulées et propagées, générant ainsi des dommages plus ou moins graves sur le plan humain, matériel, financier, etc. Il est donc souhaitable d’obtenir les résultats les plus précis possible lorsque nous utilisons l’arithmétique flottante. Pour ce faire, nous avons développé un outil qui corrige partiellement ces erreurs d’arrondi, par une transformation automatique et source à source des programmes. Notre transformation repose sur une analyse statique par interprétation abstraite qui fournit des intervalles pour les variables présentées dans les codes sources. Nous transformons non seulement des expressions arithmétiques mais aussi des morceaux de code avec des affectations, des boucles, des conditionnelles, des fonctions, etc. Les résultats obtenus par notre outils sont très prometteurs. Nous avons montré que nous améliorions de manière significative la précision numérique des calculs en minimisant l’erreur par rapport à l’arithmétique exacte des réels. Un autre critère très intéressant est que notre technique permet d’accélérer la vitesse de convergence de méthodes numériques itératives par amélioration de leur précision comme les méthodes de Newton, Jacobi, Gram-Schmidt, etc. Nous avons réussi à réduire le nombre d’itérations nécessaire pour converger de plusieurs dizaines de pourcents. Nous avons aussi étudié l’impact de l’optimisation de la précision sur le format des variables (en simple ou double précision). Pour ce faire, nous avons comparé deux programmes sources écrits en simple et en double précision avec celui transformé en simple précision. Les résultats obtenus montrent que le programme transformé (32 Bits) est très proche du résultat exact de celui de départ (64 Bits). Cela permet à l’utilisateur de dégrader la précision sans perdre beaucoup d’informations. D’un point de vue théorique, nous avons prouvé que les programmes générés n’ont pas forcément la même sémantique que les programmes d’origine, mais que mathématiquement, ils sont équivalents.

Improvement of the robot’s performances is a major challenge in the industrial field. In general, improvement objectives are increasing workspace, transportable capacity, speed and precision of the robot. To achieve these objectives, it must increase rigidity, reduce weight and increase damping capacity of the robot. Currently, the robots are generally made of metals: aluminum or steel, which limits their performances due to low damping capacity of these materials.Composite materials present an advantage to combine different materials, which leads to a variety of composite material properties. Among the types of reinforcements, carbon fibers show high modulus that enables robotic parts with high static rigidities to be designed. However, carbon fibers have generally a low damping capacity. Natural fibers have low density, good specific properties and high damping capacity.This thesis focuses on the improvement of the performances of the 3CRS parallel robot by using the composite material to redesign robot parts initially made of aluminum. The thesis begins with static and dynamic characterizations of the original robot. Then, the shape of segments of the robotic arms is optimized with respect to applying force on the robot. A hybrid laminated composite reinforced with carbon fibers and flax fibers is proposed for the use. This combination enables to combine the advantages of two fiber types in a composite for using in high loaded components. The structure of the new hybrid laminated composite is optimized and a composite segment is then fabricated in order to validate the design. Finally, the analysis of the new robot with composite arms is executed. The result shows that the new robot has a slightly higher rigidity, lighter mass and considerably greater damping capacity in comparison with the original robot. Therefore, the application of the hybrid composite could improve the static and dynamic performances and increases considerably the accuracy in operation of the robot 3CRS., L’amélioration des performances des robots est un enjeu important dans le domaine industriel. Les objectifs visés sont l’augmentation de l’espace de travail, de la capacité de charge transportable, de la vitesse de travail et de la précision du robot. Pour atteindre ces objectifs, il faut en général augmenter la rigidité, diminuer la masse et augmenter la capacité d’amortissement du robot. Les robots actuels sont généralement fabriqués en métaux : aluminium ou acier, ce qui limite leurs performances en raison des faibles capacités d’amortissement des vibrations de ces matériaux. Les matériaux composites présentent l’avantage de combiner des matériaux différents, ce qui conduit à une variété de leurs performances. Parmi les types de renforts, les fibres de carbone présentent un module d’élasticité élevé permettant la conception de pièces de grandes rigidités statiques mais elles possèdent une faible capacité d’amortissement. Les fibres végétales, par contre, possèdent une faible densité, de bonnes propriétés spécifiques et des capacités d’amortissement élevées. Cette thèse porte sur l’amélioration des performances d’un robot parallèle 3CRS en utilisant des matériaux composites pour reconcevoir des pièces initialement fabriquées en aluminium. La thèse commence d’abord par une caractérisation des comportements statiques et dynamiques du robot initial constitué de bras en aluminium. Ensuite, la forme des segments des bras robotiques est optimisée par rapport aux sollicitations mécaniques sur le robot. Un nouveau composite stratifié hybride renforcé par des fibres de carbone et des fibres de lin est alors proposé. Cette combinaison permet d’allier les avantages des deux types de fibres dans un composite pour le dimensionnement des composants sous sollicitation élevée. La structure de ce nouveau composite a été optimisée puis un segment est fabriqué pour valider la conception. Finalement, l’étude du nouveau robot avec des bras en matériaux composites a été réalisée, les résultats montrent que la rigidité du robot augmente, sa masse diminue légèrement et sa capacité d’amortissement augmente considérablement par rapport au robot initial. Donc, l’application du composite stratifié hybride peut améliorer les performances statiques et dynamiques et augmenter significativement la précision en fonctionnement du robot 3CRS.

Supercomputing plays an important role in several innovative fields, speeding up prototyping or validating scientific theories. However, supercomputers are evolving rapidly with now millions of processing units, posing the questions of their programmability. Despite the emergence of more widespread and functional parallel programming models, developing correct and effective parallel applications still remains a complex task. Although debugging solutions have emerged to address this issue, they often come with restrictions. However programming model evolutions stress the requirement for a convenient validation tool able to handle hybrid applications. Indeed as current scientific applications mainly rely on the Message Passing Interface (MPI) parallel programming model, new hardwares designed for Exascale with higher node-level parallelism clearly advocate for an MPI+X solutions with X a thread-based model such as OpenMP. But integrating two different programming models inside the same application can be error-prone leading to complex bugs - mostly detected unfortunately at runtime. In an MPI+X program not only the correctness of MPI should be ensured but also its interactions with the multi-threaded model, for example identical MPI collective operations cannot be performed by multiple nonsynchronized threads. This thesis aims at developing a combination of static and dynamic analysis to enable an early verification of hybrid HPC applications. The first pass statically verifies the thread level required by an MPI+OpenMP application and outlines execution paths leading to potential deadlocks. Thanks to this analysis, the code is selectively instrumented, displaying an error and synchronously interrupting all processes if the actual scheduling leads to a deadlock situation., L’utilisation du parallélisme des architectures actuelles dans le domaine du calcul hautes performances, oblige à recourir à différents langages parallèles. Ainsi, l’utilisation conjointe de MPI pour le parallélisme gros grain, à mémoire distribuée et OpenMP pour du parallélisme de thread, fait partie des pratiques de développement d’applications pour supercalculateurs. Des erreurs, liées à l’utilisation conjointe de ces langages de parallélisme, sont actuellement difficiles à détecter et cela limite l’écriture de codes, permettant des interactions plus poussées entre ces niveaux de parallélisme. Des outils ont été proposés afin de palier ce problème. Cependant, ces outils sont généralement focalisés sur un type de modèle et permettent une vérification dite statique (à la compilation) ou dynamique (à l’exécution). Pourtant une combinaison statique/- dynamique donnerait des informations plus pertinentes. En effet, le compilateur est en mesure de donner des informations relatives au comportement général du code, indépendamment du jeu d’entrée. C’est par exemple le cas des problèmes liés aux communications collectives du modèle MPI. Cette thèse a pour objectif de développer des analyses statiques/dynamiques permettant la vérification d’une application parallèle mélangeant plusieurs modèles de programmation, afin de diriger les développeurs vers un code parallèle multi-modèles correct et performant. La vérification se fait en deux étapes. Premièrement, de potentielles erreurs sont détectées lors de la phase de compilation. Ensuite, un test au runtime est ajouté pour savoir si le problème va réellement se produire. Grâce à ces analyses combinées, nous renvoyons des messages précis aux utilisateurs et évitons les situations de blocage.

The work reported in this thesis revisits in two waysthe abstract domain of polyhedraused for static analysis of programs.First, strong guarantees are provided on the soundness of the operationson polyhedra,by using of the Coq proof assistant to check the soundness proofs.The means used to ensure correctnessdon't hinder the performance of the resultingVerimag Polyhedra Library (VPL).It is built on the principle of result verification:computations are performed by an untrusted oracleand their results are verified by a checkerwhose correctness is proved in Coq.In order to make verification cheap,the oracle computes soundness witnesses along with the results.The other distinguishing feature of VPL is thatit relies only on the constraint representation of polyhedra,as opposed to the common practice of using both constraints and generators.Despite this unusual choice,VPL turns out to be a competitive abstract domain of polyhedra,performance-wise.As expected, the join operator of VPL,which performs the convex hull of two polyhedra,is the costliest operator.Since it builds on the projection operator,this thesis also investigates a new approach toperforming projections,based on parametric linear programming.A new understanding of projection encoded asa parametric linear problem is presented.The thesis closes on a progress report in the design of a new solvingalgorithm,tailored to the specifics of the encodingso as to achieve good performance., Cette thèse revisite de deux manières le domaine abstrait des polyèdres utilisé pour l'analyse statique de programmes.D'abord, elle montre comment utiliser l'assistant à la preuve Coq pour apporter des garanties sur la correction des opérations sur les polyèdres sans compromettre l'efficacité de l'outil VP Lissu de ces travaux.L'outil est fondé sur le principe de la vérification de résultats :un oracle, auquel on ne fait pas confiance, fait les calculs,puis les résultats sont vérifiés par un validateur dont la correction est prouvée avec Coq. De plus, l'oracle fournit des témoins de la correction des résultats afin d'accélérer la vérification.L'autre caractéristique de VPL est l' utilsation de la seule représentation par contraintes des polyèdres,par opposition à l'approche habituelle qui consiste à utiliser à la fois des contraintes et des générateurs.Malgré ce choix inhabituel,les performances de VPL s'avèrent compétitives.Comme on pouvait le prévoir,l'opérateur "join",qui calcule l'enveloppe convexe de deux polyèdres,est le plus coûteux.Puisqu'il nécessite un grand nombre de projections,cette thèse explore plusieurs nouvelles approches de l'opérateur de projection,basées sur la programmation linéaire paramétrique.Elle propose une synthèse des variantes et des combinaisons possibles.La thèse se termine sur les éléments clés d'un nouvel algorithme de résolution tirant parti des spécificités de l'encodage afin d'obtenir de bonnes performances.

The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods., L’objectif général de cette thèse est le développement de méthodes mathématiques correctes et efficaces en pratique pour prouver automatiquement la correction de logiciels. Plus précisément, cette thèse est fondée sur la théorie de l’interprétation abstraite, un cadre mathématique puissant pour l’approximation du comportement des programmes. En particulier, cette thèse se concentre sur la preuve des propriétés de vivacité des programmes, qui représentent des conditions qui doivent être réalisés ultimement ou de manière répétée pendant l’exécution du programme. La terminaison des programmes est la propriété de vivacité la plus fréquemment considérée. Cette thèse conçoit des nouvelles approximations, afin de déduire automatiquement des conditions suffisantes pour la terminaison des programmes et synthétiser des fonctions de rang définies par morceaux, qui fournissent des bornes supérieures sur le temps d’attente avant la terminaison. Les approximations sont paramétriques dans le choix entre l’expressivité et le coût des approximations sous-jacentes, qui maintiennent des informations sur l’ensemble des valeurs possibles des variables du programme ainsi que les relations numériques possibles entre elles. Cette thèse développe également un cadre d’interprétation abstraite pour prouver des propriétés de vivacité, qui vient comme une généralisation du cadre proposé pour la terminaison. En particulier, le cadre est dédié à des propriétés de vivacité exprimées dans la logique temporelle, qui sont utilisées pour s’assurer qu’un événement souhaitable se produit une fois ou une infinité de fois au cours de l’exécution du programme. Comme pour la terminaison,des fonctions de rang définies par morceaux sont utilisées pour déduire des préconditions suffisantes pour ces propriétés, et fournir des bornes supérieures sur le temps d’attente avant un événement souhaitable. Les résultats présentés dans cette thèse ont été mis en œuvre dans un prototype d’analyseur. Les résultats expérimentaux montrent qu’il donne de bons résultats sur une grande variété de programmes, il est compétitif avec l’état de l’art, et il est capable d’analyser des programmes qui sont hors de la portée des méthodes existantes.

Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. In this thesis, we propose several improvements on the abstract interpretation framework that enhance the overall precision of the analysis.Usually, abstract interpretation consists in computing an ascending sequence with widening, which converges towards a fixpoint which is a program invariant; then computing a descending sequence of correct solutions without widening. We describe and experiment with a method to improve a fixpoint after its computation, by starting again a new ascending/descending sequence with a smarter starting value. Abstract interpretation can also be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. Satisfiability modulo theories (SMT), whose efficiency has been considerably improved in the last decade, allows sparse representations of paths and sets of paths. We propose to combine this SMT representation of paths with various state-of-the-art iteration strategies to furtherimprove the overall precision of the analysis. We propose a second coupling between abstract interpretation and SMT in a program verification framework called Modular Path Focusing, that computes function and loop summaries by abstract interpretation in a modular fashion, guided by error paths obtained with SMT. Our framework can be used for various purposes: it can prove the unreachability of certain error program states, but can also synthesize function/loop preconditions for which these error states are unreachable.We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis. We finally describe the design and the implementation of Pagai, a new static analyzer working over the LLVM compiler infrastructure, which computes numerical inductive invariants using the various techniques described in this thesis. Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages and benchmarks used in the community., L’analyse statique de programme a pour but de prouver automatiquement qu’un programme vérifie certaines propriétés. L’interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l’ordre d’itération utilisés pendant le calcul d’invariants. Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l’analyse.Habituellement, l’interprétation abstraite consiste en un calcul de point fixe d’un opérateur obtenu après convergence d’une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d’améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement. L’interprétation abstraite peut également être rendue plus précise en distinguant tous les chemins d’exécution du programme, au prix d’une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d’utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d’itération de l’état de l’art pour obtenir des analyses plus précises.Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d’erreur. Notre technique a différents usages: elle permet de montrer qu’un état d’erreur est inatteignable, mais également d’inférer des préconditions aux boucles et aux fonctions. Nous appliquons nos méthodes d’analyse statique à l’estimation du temps d’exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d’exprimer ce problème via optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l’ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique.Enfin, nous présentons l’implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté.

Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis., Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes.

Nowadays real-time systems are omnipresent and embedded systems thrive in a variety of application fields. When they are integrated into safety-critical systems, the verification of their properties becomes a crucial part. Dependability is a primary design goal in environments that use hard real-time systems, whereas general-use microprocessors were designed with a high performance goal. The average-throughput maximization design choice is intrinsically opposed to design goals such as dependability that benefit mostly from highly deterministic architectures without local optimizations. Besides the growth in complexity of the embedded systems, platforms are getting more and more heterogeneous. With regard to the respect of the timing constraints, real-time systems are classified in two categories: hard real-time systems (the non respect of a deadline can lead to catastrophic consequences) and soft real-time systems (missing a deadline can cause performance degradation and material loss). We analyze hard real-time systems that need precise and safe determination of the worst-case execution time bounds in order to be certified.The validation of their non-functional properties is a complex and resource consuming task. One of the main reasons is that currently available solutions focus on delivering precise estimations through tools that are highly dependent on the underlying platform (in order to provide precise and safe results, the architecture of the system must be taken into account).In this thesis we address the above issues by introducing a timing analysis method that maintains a good level of precision while being applicable to a variety of platforms. This adaptability is achieved through separating as much as possible the worst-case execution time (WCET) estimation from the model of the hardware. Our approach consists in the introduction of a new formal modeling language that captures the complex behaviour of modern hardware and is guided by the timing analysis in order to achieve the needed precision to scalability tradeoff. The analysis drives a conjoint symbolic execution of the program's binary and the processor model using a dynamic prediction module that decides what states to merge in order to limit the state space explosion. Several state merging algorithms are introduced and applied that can also give an estimation of the introduced precision loss., La détermination précise de pires temps d’exécution (WCET) est un sujet de grand intérêt pour les systèmes embarqués critiques. Le sujet de la Thèse adresse des problèmes qui ne sont pas résolus dans la littérature notamment l’inertie notable dans le changement de plateformes cibles des analyseurs existants et la perte de précision lors du passage à l’échelle. Nos travaux se concentrent justement sur une souplesse au changement du processeur à analyser et la maitrise de la perte de précision à l’aide d’un nouvel langage de modélisation du matériel qui se trouve en étroit lien avec l’analyseur même.Une estimation sûre du WCET nécessite la prise en compte du matériel sur lequel le programme est exécuté. Les processeurs embarqués dans les systèmes critiques présentent des composants qui ont été conçus non pas pour faciliter leur analyse mais pour maximiser les performances moyennes, introduisant une variabilité temporelle significative. Le temps d'exécution est donc dépendent, entre autres des valeurs effectives de données mais aussi de l'historique d'exécution. Le but étant d'estimer le pire temps d'exécution, l'option de supposer qu'à chaque fois l'optimisation ne se produit pas et que le pire temps possible est nécessaire conduit à une surestimation trop importante. A ce problème se rajoute aussi le fait que nous ne pouvons pas supposer qu'un pire temps local (par exemple le nombre de cycles pendant une micro-opération du pipeline) contribuera au vrai pire temps global à cause des anomalies temporelles des processeurs. Tous les chemins d'exécution, engendrés par la totalité des entrées possibles doivent donc être analysés. Le fait de devoir gérer cette explosion combinatoire, nous a guidé dans les choix de conception du modèle utilisé pour simuler le processeur. Nous avons conçu une méthode de spécification et d'analyse de systèmes, basée sur la méthode des abstract state machines (ASM). L'extension HiTAsm consiste en l'incorporation des notions de hiérarchie et de temporalité, pour pouvoir gérer l'explosion combinatoire en choisissant une définition d'un composant parmi plusieurs niveaux d'abstraction possibles et pour pouvoir estimer le temps écoulé entre chaque transition des états du système. Cela permet l'estimation de la consommation temporelle et la variation dynamique du niveau d'abstraction du système analysé, afin d'analyser un grand nombre d'états, tout en minimisant la perte de précision. Le modèle du processeur et l'analyseur sont complètement séparés, ce qui est nécessaire pour rendre l'outil adaptable aux changements de plateforme. L'analyseur est basé sur une exécution symbolique conjointe du binaire et du modèle de processeur spécifié avec HiTAsm. En partant des valeurs symboliques, toutes les entrées possibles du binaire sont analysées, en utilisant des sur-approximations uniquement quand c'est nécessaire de manière à minimiser la perte de précision et fournir le pire-temps d’exécution du programme le plus proche de la valeur théorique.

National audience; La sécurité dans les systèmes embarqués tels que les smartphones exige une protection des données privées manipulées par les applications tierces. Certains mécanismes utilisent des techniques d’analyse dynamique basées sur le « data-tainting » pour suivre les flux d’informationsdans le programme. Mais ces techniques ne peuvent pas détecter les flux de contrôles qui utilisent des instructions conditionnelles pour transférer implicitement les informations. En particulier, les applications malveillantes peuvent contourner le système Android et obtenir des informations sensibles à travers les flux de contrôles. Nous proposons une amélioration de l’analyse dynamique qui propage la teinte tout au long des dépendances de contrôles en utilisant les données fournies par l’analyse statique dans les systèmes Android. Notre approche réussit à détecter des attaques de contrôle de flux sur les smartphones.

This report presents the bulk of my research work from the completion of my PhD, in late 2004, until the present day. The overall aim of my research is the development of mathematically sound and practically efficient methods to check the correctness of computer software. Efficiency is achieved using approximations, while soundness is guaranteed by employing over-approximations of program behaviors. My research is grounded in the theory of abstract interpretation, a powerful mathematical framework facilitating the development, use, comparison, and composition of approximations in a sound way. I am mainly interested in developing new reusable abstraction components (so called abstract domains) that can be readily implemented, and in using them to develop static analyzers, which are computer programs able to check automatically the safety of software. While my early research was focused on inferring the values of variables in sequential programs, my current interest and latest results concern the analysis of concurrent programs, hence the title of this report. The first two chapters of this report constitute an introduction. The first chapter is an informal introduction to the problem at hand, existing solutions, their strengths and their shortcomings. The second chapter presents prior mathematical and formal tools on which our work is based, including some notions of abstract interpretation, a description of existing abstract domains and their application to the static analysis of sequential programs. It also recalls some results I obtained during my PhD and that will be useful in the rest of the report. The subsequent chapters describe the work I performed after completing my PhD. The third chapter is devoted to aspects of static analyzers that are specific to concurrent programs. This topic of personal research has led to the construction of a generic analysis method for concurrent programs, parametrized by the choice of abstract domains. The method is based on a notion of ''interference'' that abstracts thread interleavings in a sound way in order to achieve a thread-modular analysis. It is related to Jones' rely-guarantee proof method, and we make this connection formal in a first part. Then, we present an interference-based analysis in big-step form that is efficient and easy to implement. In a third part, we study the interaction of the analysis with weakly consistent memory models, found in modern processors and language specifications. The last part discusses how to adapt the analysis to exploit some properties of the scheduling (such as the use of real-time thread priorities and synchronization primitives). The fourth and fifth chapters are devoted to the design of abstract domains. Although some of them found their application in the analysis of concurrent programs, they are actually generic and could be exploited in any kind of static analysis, for concurrent or sequential programs. The fourth chapter concerns numeric domains to infer linear equality and inequality relations, developed in collaboration with Liqian Chen while he visited ENS during his PhD. The initial motivation was to revise the classic polyhedra domain using sound floating-point arithmetic to improve its efficiency, but it unexpectedly yielded the construction of new, more expressive domains based on interval affine relations, which we also present. The fifth chapter concerns the abstraction of realistic data-types as found in the C programming language, including machine integers, floating-point numbers, and structured blocks of memory (structs, unions, and arrays). We design abstractions that are aware of the low-level memory representation of data-types, to support the analysis of programs that rely on assumptions about this representation (such as ''type punning'' constructions in C). The need for such abstractions was motivated by the analysis, in the scope of the Astrée and AstréeA static analyzers, of industrial C programs, where such low-level constructions are widespread. The sixth chapter is devoted to the application of these methods to the design of static analyzer tools. It mainly reports on my experience with the Astrée analyzer, a team effort initiated during my PhD in 2001 that extended well beyond it and culminated in its industrialization in 2009. Much of my theoretical work could find some application in Astrée, as Astrée fuelled my research with not only practical problems to solve, but also concrete problems that could only be overcome by theoretical developments. This part also reports my own ongoing effort on AstréeA, an extension of Astrée that incorporates the interference abstraction presented above and aims at proving the absence of run-time error in concurrent embedded programs (while Astrée only considers synchronous programs). Additionally, this chapter presents the Apron abstract domain library, another, more academic, team effort, which aims at encouraging the research on numeric abstract domains. The report concludes with some perspectives for future researches., Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et performantes en pratique pour s'assurer de la correction des logiciels. J'utilise des approximations pour permettre une bonne performance, tandis que la validité des résultats est garantie par l'emploi exclusif de sur-approximations des ensembles des comportements des programmes. Ma recherche est basée sur l'interprétation abstraite, une théorie très puissante des approximations de sémantiques permettant aisément de les développer, les comparer, les combiner. Je m'emploie en particulier au développement de nouveaux composants réutilisables d'abstraction, les domaines abstraits, qui sont directement implantables en machine, ainsi qu'à leur utilisation au sein d'analyseurs statiques, qui sont des outils de vérification automatique de programmes. Mes premières recherches concernaient l'inférence de propriétés numériques de programmes séquentiels, tandis que mes recherches actuelles se tournent vers l'analyse de programmes concurrents, d'où le titre de ce mémoire. Les deux premiers chapitres de ce mémoire constituent une introduction, tandis que les suivants présentent mon travail d'habilitation proprement dit. Le premier chapitre est une introduction informelle à la problématique de l'analyse de programmes, aux méthodes existantes, leurs forces et leurs faiblesses. Le deuxième chapitre présente de manière formelle les outils dont nous aurons besoin par la suite : les bases de l'interprétation abstraite, quelques domaines abstraits existants et la construction d'analyses statiques par interprétation abstraite, ainsi que quelques résultats utiles que j'ai obtenu en doctorat. Le troisième chapitre est consacré aux aspects spécifiques de l'analyse de programmes concurrents. Cette recherche, très personnelle, a abouti à la construction d'une méthode d'analyse de programmes concurrents, paramétrée par le choix de domaines abstraits, et basée sur une notion d'interférence abstrayant les interactions entre threads. Ainsi, l'analyse construite est modulaire pour les threads. Cette méthode est reliée aux preuves rely-guarantee proposées par Jones, ce que nous montrons formellement dans une première partie. Nous construisons ensuite une analyse à grands pas basée sur les interférences, efficace et facile à implanter. Les deux dernière parties étudient les liens entre l'analyse et les modèles mémoires faiblement cohérents (désormais incontournables) ainsi que le raffinement de l'analyse pour tenir compte des propriétés spécifiques des ordonnanceurs temps-réels (nous étudions en particulier l'effet des priorités des threads et l'emploi d'objets de synchronisation). Le quatrième et le cinquième chapitres sont consacrés à la constructions de domaines abstraits. Ceux-ci ne sont pas spécifiquement liés au problème de la concurrence ; ils sont utiles à l'analyse de tous programmes, séquentiels comme concurrents. Le chapitre 4 étudie des domaines numériques inférant des égalités et inégalités affines, développés en collaboration avec Liqian Chen, alors doctorant en visite à l'ENS. La motivation première était l'emploi de nombres à virgule flottante afin d'améliorer l'efficacité du domaine des polyèdres, mais ces travaux ont également débouché sur la découverte de nouveaux domaines, basés sur les relations affines à coefficients intervalles, que nous présentons également. Le chapitre 5 étudie les abstractions de types de données réalistes, comme ceux rencontrés dans le langage C : les entiers machines, les nombres à virgule flottante, et les blocs structurés (tableaux, structures, unions). Nos abstractions modélisent finement les détails de l'encodage en mémoire des données afin de permettre l'analyse de programmes qui en dépendent (par exemple, ceux utilisant le type-punning). Ces abstractions sont motivées par nos expériences d'analyses, avec les outils Astrée et AstréeA, de programmes C industriels ; ceux-ci employant fréquemment ce type de constructions de bas niveau. Le sixième chapitre est consacré aux applications des méthodes présentées ci-dessus à la construction d'outils d'analyse statique. Il décrit en particulier mon travail sur l'outil Astrée que j'ai co-développé avec l'équipe Abstraction pendant et après mon doctorat, et qui a été industrialisé en 2009. Mes résultats théoriques et appliqués ont contribué au succès d'Astrée, tandis que celui-ci m'a fourni de nouveaux thèmes de recherches, sous la forme de problèmes concrets dont la résolution n'a pu se faire que grâce à des développements théoriques. Ce chapitre décrit également AstréeA, une extension d'Astrée utilisant l'abstraction d'interférences proposée plus haut pour l'analyse de programmes concurrents (Astrée étant limité aux programmes séquentiels). Il décrit également Apron, une bibliothèque de domaines abstraits numériques que j'ai co-développée. Il s'agit d'un outil plus académique, dont le but est d'encourager la recherche sur les domaines numériques abstraits. Le mémoire se conclue par quelques perspectives sur des recherches futures.

The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc., Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct.

Context-aware pervasive computing has attracted a significant research interest from both academy and industry worldwide. It covers a broad range of applications that support many manufacturing and daily life activities. For instance, industrial robots detect the changes of the working environment in the factory to adapt their operations to the requirements. Automotive control systems may observe other vehicles, detect obstacles, and monitor the essence level or the air quality in order to warn the drivers in case of emergency. Another example is power-aware embedded systems that need to work based on current power/energy availability since power consumption is an important issue. Those kinds of systems can also be considered as smart applications. In practice, successful implementation and deployment of context-aware systems depend on the mechanism to recognize and react to variabilities happening in the environment. In other words, we need a well-defined and efficient adaptation approach so that the systems' behavior can be dynamically customized at runtime. Moreover, concurrency should be exploited to improve the performance and responsiveness of the systems. All those requirements, along with the need for safety, dependability, and reliability pose a big challenge for developers.In this thesis, we propose a novel programming language called INI, which supports both event-based and rule-based programming paradigms and is suitable for building concurrent and context-aware reactive applications. In our language, both events and rules can be defined explicitly, in a stand-alone way or in combination. Events in INI run in parallel (synchronously or asynchronously) in order to handle multiple tasks concurrently and may trigger the actions defined in rules. Besides, events can interact with the execution environment to adjust their behavior if necessary and respond to unpredictable changes. We apply INI in both academic and industrial case studies, namely an object tracking program running on the humanoid robot Nao and a M2M gateway. This demonstrates the soundness of our approach as well as INI's capabilities for constructing context-aware systems. Additionally, since context-aware programs are wide applicable and more complex than regular ones, this poses a higher demand for quality assurance with those kinds of applications. Therefore, we formalize several aspects of INI, including its type system and operational semantics. Furthermore, we develop a tool called INICheck, which can convert a significant subset of INI to Promela, the input modeling language of the model checker SPIN. Hence, SPIN can be applied to verify properties or constraints that need to be satisfied by INI programs. Our tool allows the programmers to have insurance on their code and its behavior., Les applications réactives et sensibles au contexte sont des applications intelligentes qui observent l’environnement (ou contexte) dans lequel elles s’exécutent et qui adaptent, si nécessaire, leur comportement en cas de changements dans ce contexte, ou afin de satisfaire les besoins ou d'anticiper les intentions des utilisateurs. La recherche dans ce domaine suscite un intérêt considérable tant de la part des académiques que des industriels. Les domaines d'applications sont nombreux: robots industriels qui peuvent détecter les changements dans l'environnement de travail de l'usine pour adapter leurs opérations; systèmes de contrôle automobiles pour observer d'autres véhicules, détecter les obstacles, ou surveiller le niveau d'essence ou de la qualité de l'air afin d'avertir les conducteurs en cas d'urgence; systèmes embarqués monitorant la puissance énergétique disponible et modifiant la consommation en conséquence. Dans la pratique, le succès de la mise en œuvre et du déploiement de systèmes sensibles au contexte dépend principalement du mécanisme de reconnaissance et de réaction aux variations de l'environnement. En d'autres termes, il est nécessaire d'avoir une approche adaptative bien définie et efficace de sorte que le comportement des systèmes peut être modifié dynamiquement à l'exécution. En outre, la concurrence devrait être exploitée pour améliorer les performances et la réactivité des systèmes. Tous ces exigences, ainsi que les besoins en sécurité et fiabilité constituent un grand défi pour les développeurs.C’est pour permettre une écriture plus intuitive et directe d'applications réactives et sensibles au contexte que nous avons développé dans cette thèse un nouveau langage appelé INI. Pour observer les changements dans le contexte et y réagir, INI s’appuie sur deux paradigmes : la programmation événementielle et la programmation à base de règles. Événements et règles peuvent être définis en INI de manière indépendante ou en combinaison. En outre, les événements peuvent être reconfigurésdynamiquement au cours de l’exécution. Un autre avantage d’INI est qu’il supporte laconcurrence afin de gérer plusieurs tâches en parallèle et ainsi améliorer les performances et la réactivité des programmes. Nous avons utilisé INI dans deux études de cas : une passerelle M2M multimédia et un programme de suivi d’objet pour le robot humanoïde Nao. Enfin, afin d’augmenter la fiabilité des programmes écrits en INI, un système de typage fort a été développé, et la sémantique opérationnelle d’INI a été entièrement définie. Nous avons en outre développé un outil appelé INICheck qui permet de convertir automatiquement un sous-ensemble d’INI vers Promela pour permettre un analyse par model checking à l’aide de l’interpréteur SPIN.

Traditional behavior analysis usually operates at the implementation level of a malicious behavior. Yet, it is mostly concerned with the identification of a given behavior, independently of its technical implementation, and is therefore more naturally defined at a functional level. In this thesis, we define a form of program behavior analysis which operates on the function realized by a program rather than on its elementary interactions with the system. This function is extracted from program traces, a process we call abstraction. We define in a simple, intuitive and formal way the basic functionalities to abstract and the behaviors to detect, then we propose an abstraction mechanism applicable both to a static or to a dynamic analysis setting, with practical algorithms of reasonable complexity, finally we describe a behavior analysis technique integrating this abstraction mechanism. Our method is particularly suited to the analysis of programs written in high level languages or with a known source code, for which static analysis is facilitated: programs intended for virtual machines like Java or .NET, Web scripts, browser addons, off-the-shelf components. The formalism we propose for behavior analysis by abstraction relies on the theory of string and terms rewriting, word and tree languages and model checking. It allows an efficient identification of functionalities in traces and thus the construction of a representation of traces at a functional level; it defines functionalities and behaviors in a natural way, using temporal logic formulas, which assure their simplicity and their flexibility and enables the use of model checking techniques for behavior detection; it operates on an unrestricted set of execution traces; it handles the data flow in execution traces; and it allows the consideration of uncertainty in the identification of functionalities, with no complexity overhead. We validate our results on a set of experiments, which we conducted on existing malicious codes, whose traces are obtained either by dynamic binary instrumentation or by static analysis., L'analyse comportementale traditionnelle opère en général au niveau de l'implantation du comportement malveillant. Pourtant, elle s'intéresse surtout à l'identification d'un comportement donné, indépendamment de sa mise en œuvre technique, et elle se situe donc plus naturellement à un niveau fonctionnel. Dans cette thèse, nous définissons une forme d'analyse comportementale de programmes qui opère non pas sur les interactions élémentaires d'un programme avec le système mais sur la fonction que le programme réalise. Cette fonction est extraite des traces d'un programme, un procédé que nous appelons abstraction. Nous définissons de façon simple, intuitive et formelle les fonctionnalités de base à abstraire et les comportements à détecter, puis nous proposons un mécanisme d'abstraction applicable à un cadre d'analyse statique ou dynamique, avec des algorithmes pratiques à complexité raisonnable, enfin nous décrivons une technique d'analyse comportementale intégrant ce mécanisme d'abstraction. Notre méthode est particulièrement adaptée à l'analyse des programmes dans des langages de haut niveau ou dont le code source est connu, pour lesquels l'analyse statique est facilitée : les programmes conçus pour des machines virtuelles comme Java ou .NET, les scripts Web, les extensions de navigateurs, les composants off-the-shelf. Le formalisme d'analyse comportementale par abstraction que nous proposons repose sur la théorie de la réécriture de mots et de termes, les langages réguliers de mots et de termes et le model checking. Il permet d'identifier efficacement des fonctionnalités dans des traces et ainsi d'obtenir une représentation des traces à un niveau fonctionnel ; il définit les fonctionnalités et les comportements de façon naturelle, à l'aide de formules de logique temporelle, ce qui garantit leur simplicité et leur flexibilité et permet l'utilisation de techniques de model checking pour la détection de ces comportements ; il opère sur un ensemble quelconque de traces d'exécution ; il prend en compte le flux de données dans les traces d'exécution ; et il permet, sans perte d'efficacité, de tenir compte de l'incertitude dans l'identification des fonctionnalités. Nous validons nos résultats par un ensemble d'expériences, menées sur des codes malicieux existants, dont les traces sont obtenues soit par instrumentation binaire dynamique, soit par analyse statique.

The most common anomaly detection mechanisms at application level consists in detecting a deviation of the control-flow of a program. A popular method to detect such anomaly is the use of application sequences of system calls. However, such methods do not detect mimicry attacks or attacks against the integrity of the system call parameters. These kinds of attacks can be achieved by targeting non-control-data items used by the process. To enhance such detection mechanisms, we propose an approach to detect in the application the corruption of non-control-data items that have an influence on the system calls. This approach consists in building automatically a data-oriented behaviour model of an application by static analysis of its source code. We have implemented our approach in a detection mecanism that targets applications written in C. This implementation is used to illustrate the proposed approach on various examples. To further evaluate our detection mecanism, we also propose an approach to simulate attacks that target non-control-data items. This approach consists in building a fault model that reproduces the internal state of an application after such an attack. We have implemented an evaluation platform using our fault model together with an injection mecanism. This plateform is used to perform an injection campaign on two examples in order to evaluate the detection capabilities of our data-oriented behaviour model., Le chapitre 2 présente la première partie importante de nos travaux : l'approche pour la détection que nous proposons. Nous avons tout d'abord expliqué les caractéristiques des attaques contre les données de calcul et en quoi ces dernières se distinguent des autres types d'attaque. Ceci nous a notamment permis de montrer que pour perpétuer une intrusion, un utilisateur malveillant va chercher à cibler un ensemble bien précis de données de calcul. À l'aide de la logique de Hoare, nous avons ensuite expliqué que le code source des applications peut contenir des informations qui peuvent être utilisées pour détecter ce type bien précis d'attaque. Nous avons détaillé cela sur un exemple d'exploitation de vulnérabilité. Puis, nous avons présenté notre modèle de détection. Nous l'avons tout d'abord présenté empiriquement sur un cas réel d'attaques contre les données de calcul. Pour cela, nous avons détaillé la vulnérabilité utilisée dans notre exemple ainsi que les différents scénarios d'attaque et comment des invariants portant sur certaines variables permettent de détecter ces attaques. Enfin, nous avons présenté formellement notre modèle de détection. Celui-ci correspond à l'ensemble des domaines de variation des variables qui influencent l'exécution des appels de fonction. Ces domaines de variation sont calculés juste avant les appels de fonction et uniquement pour les variables qui sont atteignables à ces endroits du code source. Nous avons ensuite présenté une méthode pour construire un tel modèle. Premièrement, nous proposons d'utiliser le graphe de dépendance du programme pour déterminer pour chaque appel de fonction l'ensemble des variables qui influencent son exécution. Deuxièmement, nous proposons d'utiliser l'interprétation abstraite pour calculer pour chacun de ces ensembles de variables leur domaine de variation. Pour finir, nous présentons une implémentation de notre approche que nous avons réalisée pour les programmes écrits en langage C. Nous détaillons d'abord la phase de construction du modèle qui repose sur un outil d'analyse statique existant, Frama-C. Nous détaillons ensuite la phase d'instrumentation, celle-ci ayant pour contrainte de ne pas modifier le processus original de compilation. Le chapitre 3 présente la seconde partie importante de nos travaux : l'approche pour l'évaluation que nous proposons. Nous commençons par aborder la problématique de la simulation des erreurs engendrées par les attaques contre les données de calcul. Pour cela, nous présentons d'abord le modèle de faute que nous proposons pour simuler ce type bien particulier d'attaques. Nous étudions les caractéristiques qui doivent être simulées, quel sera leur impact sur le programme et dans quel cas ces dernières peuvent être détectées. Nous expliquons ensuite comment nous proposons de construire notre modèle de simulation. La principale problématique ici est de savoir comment déterminer l'ensemble des cibles potentielles. Il s'agit du même ensemble de variables que pour la détection. Nous proposons donc à nouveau de nous reposer sur le graphe de dépendance du programme et d'embarquer les mécanismes d'injection au sein des applications. Nous expliquons ensuite comment notre modèle de faute peut être utilisé pour l'évaluation d'un système de détection d'intrusion. Nous posons comme objectif que le résultat obtenu doit être une sur-approximation du taux de faux négatifs réel. Cela implique que nous voulons placer le système de détection d'intrusion à évaluer dans la situation la moins favorable possible. Pour respecter cette contrainte, nous montrons que notre modèle de faute doit être utilisé pour simuler une intrusion qui ne nécessite qu'une seule exploitation de la vulnérabilité, que la vulnérabilité donne accès à l'ensemble de l'espace mémoire du processus et que l'exploitation ne vise qu'une seule variable. Nous présentons enfin les modifications que nous avons apportées à notre outil afin qu'il instrumente aussi les programmes pour l'injection et comment les mécanismes d'injection ainsi ajoutés doivent être utilisés. Le chapitre 4 présente la dernière partie de nos travaux : l'évaluation de notre système de détection d'intrusion, notamment à l'aide de notre modèle de simulation d'attaque. Nous commençons par présenter la plateforme de tests que nous avons développée autour de nos mécanismes d'injection. Il s'agit d'une plateforme qui automatise la réalisation de tests ainsi que l'analyse des résultats obtenus. Nous abordons tout d'abord les problématiques d'écriture des scénarios d'exécution et de collecte des informations. Les scénarios doivent permettre de couvrir suffisamment le code des programmes utilisés pour les tests. Nous avons choisi de mesurer ce taux de couverture en fonction des appels de fonction. Les informations collectées sont utilisées pour produire deux résultats : une sur-approximation du taux réel de faux négatifs et une évaluation du taux de détection pour les injections ayant provoqué une déviation comportementale. Pour finir, nous présentons les résultats de l'évaluation de notre système de détection d'intrusion. Nous commençons par donner les performances de l'analyse. On note que la durée d'analyse peut être très grande, notamment en fonction de la taille du code à analyser, mais qu'en fonction de la sémantique du code, deux programmes de taille similaire peuvent présenter des durées d'analyse complètement différentes. Puis, nous donnons le niveau de surcharge à l'exécution. On note que la surcharge induite par nos mécanismes de détection est très faible, toujours inférieure à 1%. Nous continuons avec les performances de la détection. Nous pouvons voir que les résultats de la détection varient grandement d'un programme à l'autre, malgré un taux d'instrumentation similaire. Ce qui change, c'est le nombre d'invariants vérifiés. On voit ici la limite de notre approche : si la sémantique du code original ne permet pas de calculer suffisamment d'invariants, l'efficacité de notre approche sera alors limitée. De plus, la propagation de l'erreur n'apporte que peu d'aide à notre modèle de détection. Dans tous les cas, nous avons pu vérifier que notre approche ne génère bien pas de faux positif.

Software validation remains a crucial part in software development process. Two major techniques have improved in recent years, dynamic and static analysis. They have complementary strengths and weaknesses. We present in this thesis a new original combination of these methods to make the research of runtime errors more accurate, automatic and reduce the number of false alarms. We prove as well the correction of the method. In this combination, static analysis reports alarms of runtime errors some of which may be false alarms, and test generation is used to confirm or reject these alarms. When applied on large programs, test generation may lack time or space before confirming out certain alarms as real bugs or finding that some alarms are unreachable. To overcome this problem, we propose to reduce the source code by program slicing before running test generation. Program slicing transforms a program into another simpler program, which is equivalent to the original program with respect to certain criterion. Four usages of program slicing were studied. The first usage is called all. It applies the slicing only once, the simplification criterion is the set of all alarms in the program. The disadvantage of this usage is that test generation may lack time or space and alarms that are easier to classify are penalized by the analysis of other more complex alarms. In the second usage, called each, program slicing is performed with respect to each alarm separately. However, test generation is executed for each sliced program and there is a risk of redundancy if some alarms are included in many slices. To overcome these drawbacks, we studied dependencies between alarms on which we base to introduce two advanced usages of program slicing : min and smart. In the min usage, the slicing is performed with respect to subsets of alarms. These subsets are selected based on dependencies between alarms and the union of these subsets cover the whole set of alarms. With this usage, we analyze less slices than with each, and simpler slices than with all. However, the dynamic analysis of some slices may lack time or space before classifying some alarms, while the dynamic analysis of a simpler slice could possibly classify some. Usage smart applies previous usage iteratively by reducing the size of the subsets when necessary. When an alarm cannot be classified by the dynamic analysis of a slice, simpler slices are calculated. These works are implemented in sante, our tool that combines the test generation tool PathCrawler and the platform of static analysis Frama-C. Experiments have shown, firstly, that our combination is more effective than each technique used separately and, secondly, that the verification is faster after reducing the code with program slicing. Simplifying the program by program slicing also makes the detected errors and the remaining alarms easier to analyze, La validation des logiciels est une partie cruciale dans le cycle de leur développement. Deux techniques de vérification et de validation se sont démarquées au cours de ces dernières années : l’analyse statique et l’analyse dynamique. Les points forts et faibles des deux techniques sont complémentaires. Nous présentons dans cette thèse une combinaison originale de ces deux techniques. Dans cette combinaison, l’analyse statique signale les instructions risquant de provoquer des erreurs à l’exécution, par des alarmes dont certaines peuvent être de fausses alarmes, puis l’analyse dynamique (génération de tests) est utilisée pour confirmer ou rejeter ces alarmes. L’objectif de cette thèse est de rendre la recherche d’erreurs automatique, plus précise, et plus efficace en temps. Appliquée à des programmes de grande taille, la génération de tests, peut manquer de temps ou d’espace mémoire avant de confirmer certaines alarmes comme de vraies erreurs ou conclure qu’aucun chemin d’exécution ne peut atteindre l’état d’erreur de certaines alarmes et donc rejeter ces alarmes. Pour surmonter ce problème, nous proposons de réduire la taille du code source par le slicing avant de lancer la génération de tests. Le slicing transforme un programme en un autre programme plus simple, appelé slice, qui est équivalent au programme initial par rapport à certains critères. Quatre utilisations du slicing sont étudiées. La première utilisation est nommée all. Elle consiste à appliquer le slicing une seule fois, le critère de simplification étant l’ensemble de toutes les alarmes du programme qui ont été détectées par l’analyse statique. L’inconvénient de cette utilisation est que la génération de tests peut manquer de temps ou d’espace et les alarmes les plus faciles à classer sont pénalisées par l’analyse d’autres alarmes plus complexes. Dans la deuxième utilisation, nommée each, le slicing est effectué séparément par rapport à chaque alarme. Cependant, la génération de tests est exécutée pour chaque programme et il y a un risque de redondance d’analyse si des alarmes sont incluses dans d’autres slices. Pour pallier ces inconvénients, nous avons étudié les dépendances entre les alarmes et nous avons introduit deux utilisations avancées du slicing, nommées min et smart, qui exploitent ces dépendances. Dans l’utilisation min, le slicing est effectué par rapport à un ensemble minimal de sous-ensembles d’alarmes. Ces sous-ensembles sont choisis en fonction de dépendances entre les alarmes et l’union de ces sous-ensembles couvre l’ensemble de toutes les alarmes. Avec cette utilisation, on a moins de slices qu’avec each, et des slices plus simples qu’avec all. Cependant, l’analyse dynamique de certaines slices peut manquer de temps ou d’espace avant de classer certaines alarmes, tandis que l’analyse dynamique d’une slice éventuellement plus simple permettrait de les classer. L’utilisation smart consiste à appliquer l’utilisation précédente itérativement en réduisant la taille des sous-ensembles quand c’est nécessaire. Lorsqu’une alarme ne peut pas être classée par l’analyse dynamique d’une slice, des slices plus simples sont calculées. Nous prouvons la correction de la méthode proposée. Ces travaux sont implantés dans sante, notre outil qui relie l’outil de génération de tests PathCrawler et la plate-forme d’analyse statique Frama-C. Des expérimentations ont montré, d’une part, que notre combinaison est plus performante que chaque technique utilisée indépendamment et, d’autre part, que la vérification devient plus rapide avec l’utilisation du slicing. De plus, la simplification du programme par le slicing rend les erreurs détectées et les alarmes restantes plus faciles à analyser

Les systèmes d'information sont de nos jours de plus en plus confrontés à de nombreux risques menaçant leur sécurité. La protection de ces systèmes suppose, dans un premier temps, de définir une politique de sécurité exprimant les besoins en terme de confidentialité, intégrité et disponibilité des biens et services puis, dans un second temps, de mettre en oeuvre cette politique. Généralement, des mécanismes d'authentication et de contrôles d'accès sont déployés pour la mise en oeuvre de la politique de sécurité. Ils vérifient d'abord l'identité des utilisateurs puis s'assurent que ces derniers ont bien les autorisations nécessaires pour accéder aux ressources du système. Cependant, il est important de noter que ces approches préventives ne sont pas toujours suffisantes pour garantir les propriétés de sécurité. Elles nécessitent la vérification et le contrôle des actions des utilisateurs afin de s'assurer a posteriori que la politique est bien respectée. Intervient alors la détection d'intrusion qui n'est autre que la détection des violations de la politique de sécurité [And80]. Plusieurs modèles de systèmes de détection d'intrusion (IDS) ont été proposés depuis les travaux séminaux d'Anderson [FHS97, SCS98, KR02, ZMB03, HMZ+07]. Certaines approches, dites par scénarios, se basent sur une connaissance a priori des attaques contre le système. D'autres, dites comportementales, définissent plutôt le comportement de référence du système. Ces approches comportementales ont l'avantage de pouvoir détecter même des attaques nouvelles contrairement aux approches par scénarios. Dans le cadre de ce stage, nous nous intéressons en particulier à un modèle comportemental de détection d'intrusion, paramétré par la politique de sécurité et reposant sur le suivi du flux d'information. Ce modèle proposé par le laboratoire SSIR, a été implémenté au niveau du système d'exploitation Linux. Une deuxième implémentation a ensuite été réalisée au niveau de la machine virtuelle Java (JVM). Cette seconde implémentation (JBlare) s'intègre avec la première (Blare) et permet d'assurer un suivi dynamique du flux d'information à différents niveaux selon les applications. L'objectif de ce stage est d'étudier les techniques d'analyse statique qui pourraient être mises en oeuvre pour le suivi des flux d'information au niveau des programmes Java afin de diminuer l'impact de l'analyse dynamique et améliorer la précision du suivi.

Despite major advances in the engineering of maintainable and robust software over the years, upgrading software remains a primitive and error-prone activity. In this dissertation, we argue that several problems with upgrading software are caused by a poor integration between upgrade deployment, testing, and problem reporting. To support this argument, we present a characterization of software upgrades resulting from a survey we conducted of 50 system administrators. Motivated by the survey results, we present Mirage, a distributed framework for integrating upgrade deployment, testing, and problem reporting into the overall upgrade development process. Mirage's deployment subsystem allows the vendor to deploy its upgrades in stages over clusters of users sharing similar environments. Staged deployment incorporates testing of the upgrade on the users' machines. It is effective in allowing the vendor to detect problems early and limit the dissemination of buggy upgrades. Oasis, the testing subsystem of Mirage, improves on current state-of-the-art concolic and symbolic engines by implementing a new heuristic to prioritize the exploration of new or affected code in the upgrade. Furthermore, interactive symbolic execution, a new approach exposing the problem of path exploration to the tester using a graphical user interface, can be used to develop new search heuristics or manually guide testing to important areas of the source code. In spite of all of these efforts, some bugs are bound to remain in the software when it is deployed, and will be discovered and reported only later by the users. With the last component of Mirage, we consider the problem of instrumenting programs to reproduce bugs effectively, while keeping user data private. In particular, we develop static and dynamic analysis techniques to minimize the amount of instrumentation, and therefore the overhead incurred by the users, while considerably speeding up debugging. By combining up-front testing, stage deployment, testing on user machines, and efficient reporting, Mirage successfully reduces the number of problems, minimizes the number of users affected, and shortens the time needed to fix remaining problems.

This Phd thesis presents a static analysis algorithm for programs with threads. It generalizes abstract interpretation techniques used in the single-threaded case and allows to detect runtimes errors, e.g, invalid pointer dereferences, array overflows, integer overflows. We have implemented this algorithm. It analyzes a large industrial multithreaded code (100K LOC) in few hours. Our technique is modular, it uses any abtract domain designed for the single-threaded-case. Furthermore, without any change in the fixpoint computation, sorne abstract domains allow to detect data-races or deadlocks. This technique does not assume sequential consistency, since, in practice (INTEL and SPARC processors, JAVA, ... ), program execution is not sequentially consistent. E.g, it works in TSO (Total Store ordering) or PSO (Partial Store Ordering) memory models., Cette thèse présente un algorithme d'analyse statique pour des programmes parallèles. Il généralise des techniques d'interprétation abstraite utilisée dans le cas de programmes sans parallélisme et permet de détecter des erreurs d'exécution, exempli gratia, les déréférencements de pointeur invalide, les débordements de tableaux, les débordements d'entiers. Nous avons implémenté cet algorithme. Il analyse un code industriel de taille conséquente (100 000 lignes de code) en quelques heures. Notre technique est modulaire, elle peut utiliser n'importe quel domaine abstrait créé pour le cas de programmes non-parallèles. En outre, sans change le calcul du point fixe, certains de nos domaines abstraits. permettent la détection de data-races ou de deadlocks. Cette technique ne présuppose pas la consistance séquentielle (i.e. ne présuppose pas que l'exécution d'un programme parallèle est l'entrelacement de l'exécution de sous-programmes) puisque, en pratique (les processeurs INTEL et SPARC, JAVA, ... ) l'exécution des programmes n'est pas séquentiellement consistante. Exempli gratia notre technique fonctionne avec les modèles TSO (Total Store Ordering) et PSO (Partial Store Ordering).

This Phd thesis presents a static analysis algorithm for programs with threads. It generalizes abstract interpretation techniques used in the single-threaded case and allows to detect runtimes errors, e.g, invalid pointer dereferences, array overflows, integer overflows. We have implemented this algorithm. It analyzes a large industrial multithreaded code (100K LOC) in few hours. Our technique is modular, it uses any abtract domain designed for the single-threaded-case. Furthermore, without any change in the fixpoint computation, sorne abstract domains allow to detect data-races or deadlocks. This technique does not assume sequential consistency, since, in practice (INTEL and SPARC processors, JAVA, ... ), program execution is not sequentially consistent. E.g, it works in TSO (Total Store ordering) or PSO (Partial Store Ordering) memory models., Cette thèse présente un algorithme d'analyse statique pour des programmes parallèles. Il généralise des techniques d'interprétation abstraite utilisée dans le cas de programmes sans parallélisme et permet de détecter des erreurs d'exécution, exempli gratia, les déréférencements de pointeur invalide, les débordements de tableaux, les débordements d'entiers. Nous avons implémenté cet algorithme. Il analyse un code industriel de taille conséquente (100 000 lignes de code) en quelques heures. Notre technique est modulaire, elle peut utiliser n'importe quel domaine abstrait créé pour le cas de programmes non-parallèles. En outre, sans change le calcul du point fixe, certains de nos domaines abstraits. permettent la détection de data-races ou de deadlocks. Cette technique ne présuppose pas la consistance séquentielle (i.e. ne présuppose pas que l'exécution d'un programme parallèle est l'entrelacement de l'exécution de sous-programmes) puisque, en pratique (les processeurs INTEL et SPARC, JAVA, ... ) l'exécution des programmes n'est pas séquentiellement consistante. Exempli gratia notre technique fonctionne avec les modèles TSO (Total Store Ordering) et PSO (Partial Store Ordering).

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexamples. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. To achieve their respective goal, the former builds and refine reachability tress while the latter annotates location with abstract states and rely on overapproximation to accelerate convergence. In this thesis we focus on capturing within a framework existing approaches as well as new solutions with the objective of enabling a better understanding of the fundamental similarities and differences between approaches and with a strong accent on implementability. In a first step, we designed and implemented a framework and a corresponding algorithm for software verification called configurable program analysis. The algorithm can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. An instance of an analysis in the framework consists of one or more program analyses, such as a predicate abstraction or a shape analysis, and their execution and interaction is controlled using several parameters of our generic verification algorithm. Our experiments consider different configurations of combinations of symbolic analyses. By varying the value of parameters we were able to explore a continuous precision-efficiency spectrum and we showed that it can lead to dramatic improvements in efficiency. In a second step, we improved our framework and algorithm to enable the program analysis to dynamically (on-line) adjust its precision depending on the accumulated results. The framework of configurable program analysis offers flexible, but static, composition of program analyses. Our extension enables composite analyses to adjust the precision of each of their component analyses independently and dynamically. To illustrate, we can allow the explicit tracking of the values of a variable to be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. We evaluated the dynamic precision adjustment mechanism by considering combinations of symbolic and explicit analyses. We analyzed code taken from an SSH client/server software as well as hand-crafted examples. We showed that the new approach offers significant gains compared with a purely symbolic, predicate-abstraction-based approach. In a third step, we consider the problem of refinement in addition to the dynamic adjustment of the precision. In contrast to precision adjustment, refinement only increases the precision of the analysis. Moreover, when a refinement occurs, states with a lower precision are discarded and replaced by states with a higher precision. Based on our framework, we present a novel refinement approach for shape analysis, a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structure implementations. The approach uses two techniques to guide the refinement of shape abstractions. First, during program exploration, an explicit heap analysis collects sample instances of the heap structures. The samples are used to identify the data structures that are manipulated by the program. Second, during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We were able to successfully verify example programs from a data-structure library that manipulate doubly-linked lists and trees. The techniques presented in this thesis have been implemented as an extension to the BLAST model checker.

Array bound checking has been widely studied. However, there are very few convincing results about array contents analysis. For such an analysis, numerical analyses are fundamental. In particular, when assigning a[i], knowledge about a[j] is kept unchanged if the invariant i ≠ j is discovered. We propose a new weakly relational numerical analysis, combining potential constraints (x - y ≤ c or ±x ≤ c) with disequalities (x ≠ y or x ≠ 0). If the variables are valued in a dense set, the analysis runs in O(n4). In the arithmetic case, the satisfiability problem of the conjunction of such constraints is NP-complete. We propose an analysis with complexity O(n4) for this case too. In the core of array contents analyses we also find symbolic partitioning analyses. To precisely analyze a loop "for i = 1 to n", in which an array is accessed at index i, slices [1, i - 1], [i, i] and [i + 1, n] of arrays contents must be considered. We define a semantic partitioning analysis and then an array contents analysis based on its results. This later analysis binds to each slice φ a property ψ whose variables stand for the arrays contents of the slice. The properties ψ are interpreted pointwise on the slice. So for φ = [1, i - 1] and ψ = (a = b + 1), it means that ∀ k ∈ [1, i - 1], a[k] = b[k] + 1. Experimental results show that our automatic analysis is efficient and precise on simple programs: one-dimensional arrays, indexed by one variable at most (x + c or c), traversed by possibly nested "for" loops, the counters of which follow an arithmetic progression. The analysis is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a "sentinel", the index stays within the bounds., Si l'analyse automatique des accès aux tableaux a été largement étudiée, on trouve très peu de résultats convaincants sur l'analyse du contenu des tableaux. Pour une telle analyse, les analyses numériques sont centrales. Notamment, si l'on découvre l'invariant i ≠ j, on évite d'affaiblir la connaissance sur a[j] lors d'une affectation à a[i]. Nous proposons une nouvelle analyse numérique faiblement relationnelle, combinant des contraintes de zones (x - y ≤ c ou ±x ≤ c) à des contraintes de non-égalités (x ≠ y ou x ≠ 0). Cette analyse a une complexité en O(n4), si les variables prennent leur valeurs dans un ensemble dense. Dans le cas arithmétique, décider de la satisfaisabilité d'une conjonction de telles contraintes est un problème NP-complet. Nous proposons une analyse en O(n4) également pour ce cas. Au cœur des analyses du contenu des tableaux on trouve aussi des analyses de partitionnement symbolique. Pour une boucle " for i = 1 to n ", où un tableau est accédé à la cellule i, il est nécessaire de considérer le contenu des tableaux sur les tranches [1, i - 1], [i, i] et [i + 1, n] pour être précis. Nous définissons une analyse de partitionnement sémantique, puis une analyse du contenu des tableaux basée sur ses résultats. Cette dernière associe à chaque tranche φ une propriété ψ dont les variables représentent le contenu des tableaux sur cette tranche. La propriété ψ est interprétée cellule-par-cellule, ainsi pour φ = [1, i - 1] et ψ = (a = b + 1) il est exprimé que ∀ k ∈ [1, i - 1], a[k] = b[k] + 1. Les résultats expérimentaux montrent que notre analyse automatique est efficace et précise, sur une classe de programmes simples : tableaux unidimensionnels, indexés par une variable au plus (x + c ou c), traversés par des boucles, imbriquées ou non, avec des compteurs suivant une progression arithmétique. Elle découvre par exemple que le résultat d'un tri par insertion est un tableau trié, ou que durant le parcours d'un tableau gardé par une "sentinelle", tous les accès à ce tableau sont corrects.

Developing static analyzers requires an intensive handling of tree and graph structures representing the program. Even if generalist languages such as Java or C++ have libraries dedicated to the manipulation of such structures, the absence of specialized statements makes the code complex and difficult to maintain. The purpose of this thesis is to provide dedicated language constructs to prototype tools for analysis and program transformation inspired by the term and term-graph rewriting. The originality of our approach is to embed these new statements in generalist languages. This is motivated by the development of the Tom language that offers rewriting constructs for generalist languages like Java. The first contribution of this thesis is to formalize embedded languages in the concept of island languages. This formalism enables the certification of the Tom compiler. Our work on Bytecode analysis leads us to propose a dedicated language for the representation and manipulation of program flow graphs. Thus we propose language constructs based on the term-graph rewriting. A further contribution of this thesis is to design a strategy language adapted to the expression of properties on a program. Associated with matching capabilities, this language allows to express in a declarative way analysis and transformations on trees or graphs. Finally, all the proposals of this thesis have been integrated into the Tom language in the form of new statements or improvements of existing ones. This language proposal has been applied to the analysis of Java programs., Développer des analyseurs statiques nécessite une manipulation intensive de structures d'arbres et de graphes représentant le programme. La finalité de cette thèse est de proposer des constructions de langage dédiées au prototypage d'outils d'analyse et de transformation de programmes et inspirées de la réécriture de termes et de termes-graphes. L'originalité de notre approche est d'embarquer ces nouvelles constructions dans les langages généralistes sous la forme d'un langage dédié embarqué. Les travaux de cette thèse se fondent sur le langage Tom qui propose d'embarquer des constructions de réécriture dans des langages généralistes comme Java. La première contribution de cette thèse a été de formaliser les langages embarqués sous le concept de langage îlot. Ce formalisme a ainsi permis de certifier la compilation du langage Tom. Nos travaux sur l'analyse de Bytecode nous ont ensuite conduit à réfléchir à la représentation et la manipulation de graphes de flot de programmes et nous avons alors proposé des constructions de langage inspirées de la réécriture de termes-graphes. Une autre contribution de cette thèse est la conception d'un langage de stratégies adapté à l'expression de propriétés sur un programme. Associé au filtrage, ce langage permet d'exprimer de manière déclarative des analyses et des transformations sur des arbres ou des graphes. Enfin, l'ensemble des propositions de cette thèse a été intégré au langage Tom sous la forme de nouvelles constructions syntaxiques ou d'améliorations de constructions existantes et a ainsi pu être appliqué à l'analyse du langage Java.

Software applications have gained a notable role in our everyday activities, mobile code applications being a significant portion of these software agents. The mobile code paradigm entails the distribution of applications from the code producer to heterogeneous client environments in which they are executed. An extended practice of this paradigm consists in the development of third party components, that are transferred across an untrusted network such as Internet and finally integrated in a host execution environment such as a PC or a cellular phone. Naturally, this computational environment opens the door to the deployment of malicious code in client workstations. In some cases a potential misbehavior of the mobile code does not constitute a serious risk, for example when the integrity of the data affected by the execution is irrelevant, or when the execution architecture imposes strong constraints on the computational capabilities of the foreign application. There still are, however, situations in which it is essential to verify the functional correctness of the code before executing it, for instance when the confidentiality of critical data such as credit card information could be compromised, or when the execution environment does not have a special mechanism to monitor excessive resource consumption. George Necula proposed a technique to provide trust to code consumers about the program correctness without trusting the code producer side. The technique, Proof Carrying Code (PCC), consists in deploying code together with a formal proof of its correctness. Correctness is an inherent property of the received code that cannot be inferred from the identity of the code producer. That naturally puts PCC in advantage with respect to methods based on trusting a third party authority. Indeed, a signature from a trusted authority it is not sufficient to provide absolute trust on the execution of the received code. From its origins, the typical mechanism of PCC to generate certificates relies on a certifying compiler, an extension of a standard compiler that automatically produces certificates for decidable safety policies. Extending the set of enforceable properties is challenging and in the most general case it requires human interaction. One possibility, is to verify the final executable code from scratch. However, the lack of structure makes low level code verification a less natural, and hence more daunting, task. This, together with the fact that verification environments target mostly high level code, makes more appropriate the idea of moving the generation of certificates at the source code level. The main drawback of producing certificates ensuring source code correctness is that they do not entail correctness of the final compiled code. Several techniques may be proposed to transfer evidence of program correctness from the source code to the executable counterpart. That includes, for instance, deploying the source program and original certificates in addition to the executable code and certifying the correctness of the compilation process. However, this approach is not satisfactory, since in addition to require availability of the source code, a certificate ensuring compiler correctness can be prohibitively large. A more viable alternative is to provide a mechanism to generate certificates for compiled code from certificates of the original source program. Compilers are complex procedures composed of several steps, in which the original program is progressively transformed into intermediate lower level representations. Barthe et al. and Pavlova have shown that original certificates are preserved, up to minor differences, along with the first compiler phase: a nonoptimizing compilation from source level to an unstructured intermediate representation. However, compiler optimizations applied to the intermediate representations represent a challenge since a priori certificates cannot be reused. In this thesis, we analyze how optimizations affect the validity of certificates and propose a mechanism, Certificate Translation, to transform certificates in order to overcome the effects of program transformations, rendering feasible the generation of certificates for executable mobile code at the source level. Chapter 2 introduces certificate translation for common compiler optimizations applied in the context of an intermediate RTL language. The main difficulties are presented, and a classification of program transformations is given in terms of the effort required to transform the original certificates. A general scheme is provided to cover transformations that performs arithmetic simplifications such as constant propagation and common subexpression elimination. In addition, ad-hoc techniques are proposed for other standard optimizations that do not correspond to this classification. Chapter 3 studies the existence of certificate translators in a mild extension of an abstract interpretation framework that includes a notion of certificates. This abstract setting provides considerable advantages with respect to the approach of Chapter 2 since it allows us to extend certificate translation to diverse programming languages and several analysis environments. Certificate transformation is studied in this abstract setting for simple program transformations which can be composed to represent a wide variety of program optimizations, for instance those considered in Chapter 2. In a second part of the thesis, we extend certificate translation to less typical settings, that can be of interest in PCC scenarios. More precisely, the chapters in the second part consider the aspect oriented paradigm, hybrid verification methods and parallel programs executing in memory hierarchies. For each setting, appropriate analysis and verification settings are provided. Then, the effect of common transformations over verification results are studied., Le paradigme du code mobile implique la distribution des applications par les producteurs de code à environnements hétérogènes dans lesquels elles sont exécutées. Une pratique étendue de ce paradigme est constituée par le développement d'applications telles que les applets ou les scripts Web, transferés à travers un réseau non sécurisé comme Internet à des systèmes distants, par exemple un ordinateur, un téléphone mobile ou un PDA (Assistant personnel). Naturellement, cet environnement peux ouvrir la porte au déploiement de programmes malveillants dans des plateformes distantes. Dans certains cas, la mauvaise conduite du code mobile ne constitue pas un risque grave, par exemple lorsque l'intégrité des données affectées par l'exécution n'est pas critique ou lorsque l'architecture d'exécution impose de fortes contraintes sur les capacités d'exécution du code non sécurisé. Il y a toujours, toutefois, des situations dans lesquelles il est indispensable de vérifier la correction fonctionnelle du code avant son exécution, par exemple lorsque la confidentialité de données critiques comme l'information des cartes de crédit pourrait être en danger, ou lorsque l'environnement d'exécution ne possède pas un mécanisme spécial pour surveiller la consommation excessive des ressources. George Necula a proposé une technique pour apporter de la confiance aux consommateurs sur la correction du code sans faire confiance aux producteurs. Cette technique, Proof Carrying Code (PCC), consiste à déploier le code avec une preuve formelle de sa correction. La correction est une propriété inhérente du code reçuu qui ne peut pas être directement déduite du producteur du code. Naturellement, cela donne un avantage à PCC quant-aux méthodes basées sur la confiance à l'autorité d'un tiers. En effet, une signature d'une autorité ne suffit pas à fournir une confiance absolue sur l'exécution du code reçu. Depuis les origines du PCC, le type de mécanisme utilisé pour générer des certificats repose sur des analyses statiques qui font partie du compilateur. Par conséquent, en restant automatique, il est intrinsèquement limité à des propriétés très simples. L'augmentation de l'ensemble des propriétés à considerer est difficile et, dans la plupart des cas, cela exige l'interaction humaine. Une possibilité consiste à vérifier directement le code exécutable. Toutefois, l'absence de structure rend la vérification du code de bas niveau moins naturelle, et donc plus laborieuse. Ceci, combiné avec le fait que la plupart des outils de vérification ciblent le code de haut niveau, rend plus appropriée l'idée de transferer la production de certificats au niveau du code source. Le principal inconvénient de produire des certificats pour assurer l'exactitude du code source est que les preuves ne comportent pas la correction du code compilé. Plusieurs techniques peuvent etre proposées pour transférer la preuve de correction d'un programme à sa version exécutable. Cela implique, par exemple, de déployer le programme source et ses certificats originaux (en plus du code exécutable) et de certifier la correction du processus de compilation. Toutefois, cette approche n'est pas satisfaisante, car en plus d'exiger la disponibilité du code source, la longueur du certificat garantissant la correction du compilation peut être prohibitive. Une alternative plus viable consiste à proposer un mécanisme permettant de générer des certificats de code compilé à partir des certificats du programme source. Les compilateurs sont des procédures complexes composées de plusieurs étapes, parmi lesquelles le programme original est progressivement transformé en représentations intermédiaires. Barthe et al. et Pavlova ont montré que les certificats originaux sont conservés, à quelques différences près non significatives, par la première phase de compilation: la compilation non optimale du code source vers une représentation non structurée de niveau intermédiaire. Toutefois, les optimisations des compilateurs sur les représentations intermédiaires représentent un défi, car a priori les certificats ne peuvent pas être réutilisés. Dans cette thèse, nous analysons comment les optimisations affectent la validité des certificats et nous proposons un mécanisme, Certificate Translation, qui rend possible la génération des certificats pour le code mobile exécutable à partir des certificats au niveau du code source. Cela implique transformer les certificats pour surmonter les effets des optimisations de programme.

In this thesis, we define a static analysis by abstract interpretation of memory manipulations. It is based on a new numerical abstract domain, which is able to infer program invariants involving the operators min and max. This domain relies on tropical polyhedra, which are the analogues of convex polyhedra in tropical algebra. Tropical algebra refers to the set IR U {-oo} endowed with max as addition and + as multiplication. This abstract domain is provided with sound abstract primitives, which allow to automatically compute over-approximations of semantics of programs by means of tropical polyhedra. Thanks to them, we develop and implement a sound static analysis inferring min- and max-invariants over the program variables, the length of the strings, and the size of the arrays in memory. In order to improve the scalability of the abstract domain, we also study the algorithmics of tropical polyhedra. In particular, a tropical polyhedron can be represented in two different ways, either internally, in terms of extreme points and rays, or externally, in terms of tropically affine inequalities. Passing from the external description of a polyhedron to its internal description, or inversely, is a fundamental computational issue, comparable to the well-known vertex/facet enumeration or convex hull problems in the classical algebra. It is also a crucial operation in our numerical abstract domain. For this reason, we develop two original algorithms allowing to pass from an external description of tropical polyhedra to an internal description, and vice versa. They are based on a tropical analogue of the double description method introduced by Motzkin et al. We show that they outperform the other existing methods, both in theory and in practice. The cornerstone of these algorithms is a new combinatorial characterization of extreme elements in tropical polyhedra defined by means of inequalities: we have proved that the extremality of an element amounts to the existence of a strongly connected component reachable from any node in a directed hypergraph. We also show that the latter property can be checked in almost linear time in the size of the hypergraph. Moreover, in order to have a better understanding of the intrinsic complexity of tropical polyhedra, we study the problem of determining the maximal number of extreme points in a tropical polyhedron. In the classical case, this problem is addressed by McMullen upper bound theorem. We prove that the maximal number of extreme points in the tropical case is bounded by a similar result. We introduce a class of tropical polyhedra appearing as natural candidates to be maximizing instances. We establish lower and upper bounds on their number of extreme points, and show that the McMullen type bound is asymptotically tight when the dimension tends to infinity and the number of inequalities defining the polyhedra is fixed. Finally, we experiment our tropical polyhedra based static analyzer on programs manipulating strings and arrays. These experimentations show that the analyzer successfully determines precise properties on memory manipulations, and that it scales up to highly disjunctive invariants which could not be computed by the existing methods. The implementation of all the algorithms and abstract domains on tropical polyhedra developed in this work is available in the Tropical Polyhedra Library (TPLib).