Search

Evaluating the complexity of an algorithm is an important step when developing applications,as it impacts both its time and energy performance. Computational complexity, which is thenumber of arithmetic operations of a program, is easy to characterize for affine programs,that are composed of simple loops with static bounds. Data movement (or, I/O) complexityis more complex to evaluate as it refers, when considering all possible valid schedules, to theminimum required number of I/O between a slow memory with large capacity, and a faststorage location with limited capacity.This thesis presents IOOpt, a fully automated tool that automatically computes symbolicbounds on the I/O complexity of an affine program. Given a description of an affine program,it automatically computes: 1. a lower bound of the I/O complexity as a symbolic expressionof the cache size and program parameters; 2. an upper bound that allows one to assess thetightness of the lower bound; 3. a tiling recommendation (loop permutation and tile sizes)that matches the upper bound. This tool is implemented as an open-source program, anda demonstration is available at https://iocomplexity.corse.inria.fr/. This was madepossible by combining advanced mathematical results with powerful program analysis toolssuch as polyhedral representation. Our data movement model is notably based on the onedesigned by Hong&Kung (red-blue pebble game), adapted to be able de decompose and re-compose complex programs.We demonstrate the effectiveness of our approach by deriving symbolic bounds for a widerange of affine programs. In many cases, the bounds found by IOOpt can be proven optimal,or close to optimal by a constant factor.; L’évaluation de la complexité d’un algorithme est une étape importante lors du développement d’une application, de par son impact sur son temps d’exécution et sa consommation énergétique. La complexité arithmétique, qui est le nombre d’opérations effectuées par un programme, est en général facile à caractériser pour un programme affine, composé de boucles simples avec des bornes statiques. La complexité de mouvement de données (ou complexitéI/O) est plus complexe à évaluer. En effet, elle se réfère à la quantité minimale de données à transférer entre une mémoire lente de grande capacité, et une mémoire rapide de capacité limitée, et ce en considérant tous les ordonnancements valides des opérations. Dans cette thèse, nous présentons IOOpt, un outil automatisé capable de calculer des bornes symboliques sur la complexité I/O de programmes affines. Étant donné une description d’un programme affine, il génère : 1. une borne inférieure sur la complexité I/O sous la forme d’une expression symbolique dépendant de la taille de la mémoire rapide et des paramètres du programme ; 2. une borne supérieure qui permet d’évaluer la précision de la borne inférieure 3. une recommandation de tuilage (taille des tuiles et permutation des boucles) quipermet d’atteindre la borne supérieure. Cet outil est implémenté sous la forme d’une application open-source, et peut être testé sur la page https://iocomplexity.corse.inria.fr/.Le développement de cet outil a été possible grâce à la combinaison de résultats mathématiques avancés avec des outils puissants d’analyse de programmes, tels la représentation polyédrique. Notre modèle de mouvement de données est notamment basé sur celui proposé parHong&Kung (« Red-blue pebble game »), adapté pour pouvoir décomposer et recomposer des programmes complexes. L’applicabilité de cette approche est démontrée en combinant des bornes symboliques sur un large panel de programmes affines. Dans de nombreux cas, les bornes trouvées par IOOpt sont optimales, ou proches de la borne optimale par un facteur constant.

Proving properties of programs using data-structures such as arrays often requires universally quantified invariants, e.g., ``all elements below index i are nonzero''. Instead of directly manipulating programs, we use Horn formulas which have recently become a popular format to express safety properties of programs. In this manuscript, we propose a general abstraction scheme operating on Horn formulas for unbounded data-structures. The main idea is to use abstraction to simplify the unbounded data-structures into simpler types such as integers. As such a simplification loses information, not all safety properties can be proven after abstraction. It is thus key to choose the right abstraction for the given problem.Our contribution is a general framework for which the data-structures and the abstraction to apply are parameterized. The specificity of that framework is the attention spent to ensure that our algorithm exactly implements the simplification induced by the abstraction by using a property called relative completeness. This contrasts with previous work that mainly uses benchmarks to prove the validity of the technique instead of analyzing whether the technique verifies a similar property.Although the proposed framework is general and may theoretically handle data-structures such as trees or graphs, our focus has been on a specific abstraction of arrays that has already been studied in the literature called cell abstraction. This abstraction is of particular interest as it can handle most container algorithms.There are three main contributions in this manuscript. First, a demonstration that our framework in combination with cell-abstraction can express many existing techniques, and thus our framework handles those as well. Secondly, a proof that an existing restricted technique actually satisfies relative completeness and an extension of the technique to handle a broader class of programs. Thirdly, the framework gives definitions, algorithms and theorems parameterized by the desired abstraction and, even though we have only used this framework for arrays, it gives the foundation for future abstraction of other data-structures.; Prouver des propriétés sur des programmes utilisant des structures de données telles que des tableaux nécessite souvent des invariants universellement quantifiés, par exemple, "tous les éléments avec indice plus petit que i sont non nuls". Au lieu de manipuler directement les programmes, nous utilisons des clauses de Horn, un format de plus en plus courant pour exprimer les propriétés de sécurité des programmes. Dans ce manuscrit, nous proposons un schéma d'abstraction général opérant sur des formules de Horn pour des structures de données non bornées. L'idée principale est d'utiliser l'abstraction pour simplifier les structures de données en types plus simples tels que les entiers. Comme une telle simplification perd de l’information, toutes les propriétés ne peuvent pas être prouvées après abstraction. Il est donc essentiel de choisir la bonne abstraction pour le problème donné. Notre contribution est d'avoir créé une méthode générale où les structures de données et l'abstraction à appliquer sont paramétrées. La spécificité de cette méthode est l'attention portée à une propriété que nous nommons complétude relative et qui spécifie que l’algorithme implémente exactement la simplification induite par l'abstraction. Cette approche contraste avec les travaux antérieurs qui utilisent principalement des benchmarks pour prouver la validité de la technique au lieu d'analyser si la technique vérifie une propriété similaire. Bien que le cadre proposé soit général et puisse théoriquement gérer des structures de données telles que des arbres et graphes, nous nous sommes concentrés sur une abstraction spécifique de tableaux, déjà étudiée dans la littérature et appelée abstraction de cellule. Cette abstraction est particulièrement intéressante car elle peut gérer la plupart des algorithmes de conteneur. La contribution de ce manuscrit peut être résumée en trois points. Tout d'abord, nous démontrons que notre méthode, en combinaison avec l'abstraction de cellule, permet d'exprimer, et donc de gérer, de nombreuses techniques existantes. Deuxièmement, nous prouvons qu'une de ces techniques existantes satisfait le propriété de complétude relative et une extension de celle-ci pour gérer une classe plus large de programmes. Troisièmement, même si nous nous sommes focalisés sur les tableaux, les définitions, algorithmes et théorèmes que nous fournissons sont paramétrés avec l'abstraction souhaitée et donne les bases pour de futures abstractions d'autres structures de données.

As software is an essential component of many embedded systems or online information systems, its malfunction can cause harm or security vulnerabilities. New bugs and vulnerabilities keep being discovered in existing software; many of those bugs and vulnerabilities are caused by violations of memory safety. In particular, low-level code, written in languages that offer few safety guarantees, is the most prone to this kind of bug. However, writing low-level code is sometimes necessary for performance or direct access to hardware features. Formal methods can be used to verify the safety of low-level programs, but automated analysis techniques to verify memory-related properties, such as shape analyses, still require important human effort, preventing wide adoption. In this thesis, we propose a practical automated analysis based on types that express structural invariants on memory down to the byte level. This analysis, which we formalize in the framework of abstract interpretation, offers a trade-off between precise, flow-sensitive shape analyses and scalable, flow-insensitive pointer analyses. It can be applied to low-level code with only a small amount of manual annotations. We show how the type-based abstraction can be complemented with retained and staged points-to predicates to handle precisely common low-level code patterns, such as data structure initialization. We demonstrate the effectiveness and practicality of the analysis by verifying the preservation of structural invariants (implying spatial memory safety) on C and machine code programs, showing that it can be helpful in eliminating an entire class of security vulnerabilities. We then apply our analysis to executables of embedded kernels and show that our type-based invariants allow to verify absence of runtime errors and absence of privilege escalation. To do this, we introduce the concept of implicit properties, i.e. properties which can be defined without reference to a specific program, and therefore lend themselves well to automated verification; and we prove that absence of privilege escalation is an implicit property. Parameterized verification, i.e. verification of the kernel independently from applicative code and data, poses many challenges, such as the need to summarize memory, or the dependence on a complex precondition on the initial state. We propose a methodology to solve them using our analysis technique. We apply this methodology to verify absence of runtime errors and absence of privilege escalation on a full, unmodified embedded kernel with a high level of automation.; Les logiciels étant des composants essentiels de nombreux systèmes embarqués et de nombreux systèmes d'information, un dysfonctionnement logiciel peut entraîner d'importants dommages ou des failles de sécurité. De nouveaux bugs et de nouvelles vulnérabilités sont trouvés régulièrement dans les programmes existants; une grande partie d'entre eux est causeé par des violations de la sûreté mémoire. En particulier, le code bas niveau, écrit dans des langages de programmation qui offrent peu de garanties de sûreté, est le plus susceptible de contenir ce type de bug. Malgré cela, écrire dans un langage bas niveau reste parfois nécessaire pour des raisons de performance, ou pour accéder directement aux fonctionnalités du matériel. Les méthodes formelles peuvent permettre de vérifier la sûreté des programmes bas niveau, mais les techniques automatisées de vérification de propriétés mémoire, telles que les analyses de forme, nécessitent encore un effort manuel im portant, ce qui est un obstacle à une adoption large. Dans cette thèse, nous proposons une analyse automatisée facilement applicable, basée sur un système de types exprimant des invariants structurels sur la mémoire, précis jusqu'au niveau de l'octet. Cette analyse, que nous formalisons dans le cadre de l'interprétation abstraite, offre un compromis entre les analyses de forme, précises et sensibles au flot de contrôle, et les analyses de pointeurs, qui sont insensibles au flot de contrôle mais passent très bien à l'échelle. Elle peut être appliquée à du code bas niveau avec peu d'annotations manuelles. Nous montrons comment cette analyse basée sur les types peut être complémentée par des prédicats de pointeurs conservés et reportés, afin de supporter précisément des motifs fréquents en code bas niveau tels que l'initialisation de structures de données. Nous démontrons l'efficacité et l'applicabilité de l'analyse en vérifiant la conservation d'invariants structurels (qui impliquent la sûreté mémoire spatiale) sur des program mes C et du code machine, montrant qu'elle peut être utile pour éliminer toute une classe de failles de sécurité. Nous appliquons ensuite notre analyse à des exécutables de noyaux embarqués, et nous montrons que nos invariants à base de types permettent de vérifier l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges. Pour cela, nous introduisons le concept de propriété implicite, c'est-à-dire de propriété qui peut être définie sans référence à un programme en particulier, qui se prêtent bien à la vérification automatique; et nous montrons que l'absence d'escalade de privilèges est une propriété implicite. La vérification paramétrée, c'est-à-dire la vérification de noyaux indépendamment du code et des données des applications, comporte plusieurs défis, comme le besoin de résumer la mémoire ou bien la dépendance à une précondition complexe sur l'état initial. Nous proposons une méthodologie pour les résoudre à l'aide de notre technique d'analyse. À l'aide de cette méthodologie, nous vérifions l'absence d'erreurs à l'exécution et l'absence d'escalade de privilèges su r un noyau entier sans modification, avec un haut niveau d'automatisation.

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.

Although users of High Performance Computing (HPC) are most interested in raw performance, both storage costs and power consumption have become critical concerns. This is due to several technological issues such as the power limitation of processors and the massive cost of communications which arise when executing applications on such architectures. In recent years, the use of precision tuning to improve the performance metrics is emerging as a new trend to save the resources on the available processors. In this thesis, we introduce a new technique for precision tuning radically different from the existing ones. The main idea of our approach is based on a semantical modelling of the propagation of the numerical errors throughout the program source. This yields a system of constraints whose minimal solution gives the best tuning of the program. Based on a static analysis approach, we formulate the problem of precision tuning with two different methods. The first method combines a forward and a backward error analysis which are two popular paradigms of error analysis. Next, our analysis is expressed as a set of linear constraints, made of propositional logic formulas and relations between integer elements only, checked by a SMT solver. The second method consists of generating an Integer Linear Problem (ILP) from the program. Basically, this is done by reasoning on the most significant bit and the number of significant bits of the values which are integer quantities. The integer solution to this problem, computed in polynomial time by a classical linear programming solver, gives the optimal data types at bit-level. A finer set of semantic equations is also proposed which does not reduce directly to an ILP problem. So, we use the policy iteration technique to find a solution. Both methods have been implemented in a tool named, POP. We provide in this thesis a detailed evaluation of the performance of POP on several benchmarks coming from various application domains such as embedded systems, Internet of Things (IoT), physics, etc. Also, we show that our results of precision tuning encompass the results of the state-of-the-art tools in several manners.; Bien que les utilisateurs de calcul haute performance (HPC) soient plus intéressés par les performances brutes, les coûts de stockage et la consommation d'énergie sont devenus des préoccupations importantes. Ces dernières années, l'utilisation du réglage de la précision pour améliorer les métriques de performance est devenu une nouvelle tendance pour économiser les ressources sur les processeurs disponibles. Ce processus est appelé réglage de précision (precision tuning). Dans cette thèse, nous introduisons une nouvelle technique de réglage de précision radicalement différente de celles existantes. Notre approche est basée sur une modélisation sémantique de la propagation des erreurs numériques à travers le programme. Cela génère un système de contraintes dont la solution minimale donne le meilleur réglage de précision du programme. En se basant sur une approche d'analyse statique, nous formulons le problème du réglage de précision avec deux méthodes différentes. La première méthode combine une analyse d'erreurs en avant et en arrière. Ensuite, nos analyses sont exprimées sous la forme d'un ensemble de contraintes linéaires vérifiées par un solveur SMT. La deuxième méthode consiste à générer un problème de programmation linéaire en nombres entiers (ILP) à partir du code source du programme. Cela se fait en raisonnant sur le bit de poids fort et le nombre de bits significatifs des valeurs des variables. La solution entière à ce problème, calculée en temps polynomial par un solveur de programmation linéaire classique, donne une optimisation des types de données en nombre de bits. Un ensemble plus fin d'équations sémantiques est également proposé dans cette thèse. Il utilise la méthode d'itération sur les politiques pour trouver les nouvelles précisions. Les deux méthodes ont été implémentées dans un outil appelé, POP. Nous proposons dans cette thèse une évaluation détaillée des performances de POP sur plusieurs exemples couvrant divers domaines d'application tels que les systèmes embarqués, l'Internet des objets (IoT), la physique, etc. De plus, nous proposons une comparaison détaillée entre POP et les outils de l'état de l'art.

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é.

With the advent of Internet of things (IoT), there is a need to provide energy for a massive number of smart tiny devices without using large, heavy, and high maintenance batteries. One promising way is to harvest energy from the environment and store it into an energy buffer such as a capacitor. In this way, programs are being executed as long as there is available energy in the capacitor, and crash when it exhausts. Recently, different software and hardware based checkpointing strategies have been proposed to make forward progress toward execution for energy harvesting IoT devices. This thesis introduces two different software solutions based on static and dynamic compilation. The proposed static compiler inserts checkpoints based on statically-computed worst-case energy consumption of code sections. Moreover, it applies classical compiler optimizations in order to decrease the required number of checkpoints at runtime. The proposed dynamic compilation technique delays checkpoint placement and specialization to the runtime and takes decisions based on the past power failures and execution paths taken before each power failure. Both proposed solutions guarantee making forward progress as well as keeping the memory consistent. Furthermore, they aim to increase portability by not using any hardware feature of the IoT device. In addition, they are transparent to the programmer.; Récemment, différentes stratégies de checkpointing basées sur le logiciel et le matériel ont été proposées pour avancer vers l'exécution pour les dispositifs IoT de récolte d'énergie. Cette thèse présente deux solutions logicielles différentes basées sur la compilation statique et dynamique. Le compilateur statique proposé insère des points de contrôle basés sur la pire consommation d'énergie des sections de code calculée de manière statique. En outre, il applique les optimisations classiques du compilateur afin de réduire le nombre de points de contrôle requis à l'exécution. La technique de compilation dynamique proposée reporte le placement et la spécialisation des points de contrôle au moment de l'exécution et prend des décisions en fonction des pannes de courant passées et des chemins d'exécution empruntés avant chaque panne de courant. Les deux solutions proposées garantissent une progression vers l'avant ainsi que le maintien de la cohérence de la mémoire. En outre, elles visent à accroître la portabilité en n'utilisant aucune caractéristique matérielle des systèmes IoT. En outre, elles sont transparentes pour le programmeur.

With the advent of Internet of things (IoT), there is a need to provide energy for a massive number of smart tiny devices without using large, heavy, and high maintenance batteries. One promising way is to harvest energy from the environment and store it into an energy buffer such as a capacitor. In this way, programs are being executed as long as there is available energy in the capacitor, and crash when it exhausts. Recently, different software and hardware based checkpointing strategies have been proposed to make forward progress toward execution for energy harvesting IoT devices. This thesis introduces two different software solutions based on static and dynamic compilation. The proposed static compiler inserts checkpoints based on statically-computed worst-case energy consumption of code sections. Moreover, it applies classical compiler optimizations in order to decrease the required number of checkpoints at runtime. The proposed dynamic compilation technique delays checkpoint placement and specialization to the runtime and takes decisions based on the past power failures and execution paths taken before each power failure. Both proposed solutions guarantee making forward progress as well as keeping the memory consistent. Furthermore, they aim to increase portability by not using any hardware feature of the IoT device. In addition, they are transparent to the programmer.; Récemment, différentes stratégies de checkpointing basées sur le logiciel et le matériel ont été proposées pour avancer vers l'exécution pour les dispositifs IoT de récolte d'énergie. Cette thèse présente deux solutions logicielles différentes basées sur la compilation statique et dynamique. Le compilateur statique proposé insère des points de contrôle basés sur la pire consommation d'énergie des sections de code calculée de manière statique. En outre, il applique les optimisations classiques du compilateur afin de réduire le nombre de points de contrôle requis à l'exécution. La technique de compilation dynamique proposée reporte le placement et la spécialisation des points de contrôle au moment de l'exécution et prend des décisions en fonction des pannes de courant passées et des chemins d'exécution empruntés avant chaque panne de courant. Les deux solutions proposées garantissent une progression vers l'avant ainsi que le maintien de la cohérence de la mémoire. En outre, elles visent à accroître la portabilité en n'utilisant aucune caractéristique matérielle des systèmes IoT. En outre, elles sont transparentes pour le programmeur.

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

As embedded systems are more and more present in our lives, it is necessary to protect the personal data stored in such systems. Application developers can unintentionally introduce vulnerabilities that can be exploited by attackers to compromise the confidentiality or integrity of the system. One of the solutions to prevent this is to use reactive mechanisms to monitor the behavior of the system while it is running. In this thesis, we propose a generic anomaly detection approach combining hardware and software aspects, based on dynamic information flow tracking (DIFT). DIFT consists of attaching labels representing security levels to information containers, for example files, and specifying an information flow policy to describe the authorized flows. To implement such an approach, we first developed a DIFT monitor which is flexible and non-invasive for the processor, using ARM CoreSight trace components. To take into account the information flows that occur in the different layers, from the operating system to the processor instructions, we have developed different static analysis into the compiler. These analyses generate annotations, used by the DIFT monitor, that describe the dissemination of data in the system at run-time. We also developed a Linux security module to handle information flows involving files. The proposed approach can thus be used to detect different kinds of attacks.; Les systèmes embarqués étant de plus en plus présents dans nos vies, il est nécessaire de protéger les données personnelles qui y sont stockées. En effet, les concepteurs d’applications peuvent involontairement introduire des vulnérabilités pouvant être exploitées par un attaquant pour compromettre la confidentialité ou l’intégrité du système. Un des moyens de s’en prémunir est l’utilisation d’outils réactifs permettant de surveiller le comportement du système lors de son fonctionnement. Dans le cadre de cette thèse, nous proposons une approche générique de détection d'anomalies combinant des aspects matériels et logiciels et qui repose sur le suivi de flux d’information dynamique (DIFT). Le DIFT consiste à attacher des étiquettes représentant des niveaux de sécurité à des conteneurs d'information, par exemple des fichiers, et à spécifier une politique de flux d'information permettant de décrire les flux autorisés. Pour cela, nous avons tout d’abord développé un moniteur DIFT, flexible et non invasif pour le processeur, en utilisant les composants de traces ARM CoreSight. Pour prendre en compte les flux d’information qui se produisent dans les différentes couches, du système d’exploitation aux instructions processeur, nous avons élaboré des analyses statiques dans le compilateur. Ces analyses génèrent des annotations qui décrivent la dissémination des données dans le système lors de son exécution et qui sont utilisées par le moniteur DIFT. Nous avons également développé un module de sécurité pour le noyau Linux afin de prendre en compte les flux d’information à destination ou en provenance des fichiers. L’approche proposée permet ainsi de détecter un large spectre d'attaques de natures différentes.

In this thesis, we consider several of the most classical and fundamental problems in static analysis and formal verification, including invariant generation, reachability analysis, termination analysis of probabilistic programs, data-flow analysis, quantitative analysis of Markov chains and Markov decision processes, and the problem of data packing in cache management.We use techniques from parameterized complexity theory, polyhedral geometry, and real algebraic geometry to significantly improve the state-of-the-art, in terms of both scalability and completeness guarantees, for the mentioned problems. In some cases, our results are the first theoretical improvements for the respective problems in two or three decades.; Dans cette thèse, nous considérons plusieurs des problèmes les plus classiques et fondamentaux de l'analyse statique et de la vérification formelle, y compris la génération d'invariants, l'analyse d'accessibilité, l'analyse de terminaison de programmes probabilistes et l'analyse quantitative des chaînes de Markov et des processus de décision de Markov.Nous utilisons des techniques issues de la théorie de la complexité paramétrée, de la géométrie polyédrique et de la géométrie algébrique réelle. Dans certains cas, nos résultats sont les premières améliorations théoriques des problèmes respectifs en deux ou trois décennies.

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.

When users employ a screen reader to navigate within an application user interface, they need to perceive the context of the currently-focused widget. For entries notably, they need to be sure what information should be typed in which entry. Ideally, the very programmatic structure of the user interface would be conveying this information, and be exposed as such to screen readers. In practice however, the programmatic structure expresses the layout of the visual rendering, which does not necessarily match the semantic that should be perceived by the user. In such a situation, explicit labelling is needed to provide the screen reader with the correct context information to be presented to users. The label would typically already be present in the user interface (for sighted people to understand the context) but the relation between the label and the focused widget is often only conveyed through visual proximity only, and programmers are often unaware that an explicit relation needs to be written for screen readers to express the relation for users employing a screen reader. Such missing relations can however be detected relatively accurately, by tracking widgets which do not have context information, and labels which have no relation with widgets. Simple detection heuristics applied on the LibreOffice interface emit around 8 000 lines of warnings over around 1 000 glade .ui files. Refining these heuristics reduces this down to 2 000 lines of warnings, with very few false positives and false negatives. This was assembled into the gla11y tool, now integrated in the LibreOffice build infrastructure, thus allowing LibreOffice programmers to automatically get compilation-time warnings about missing relations and guarantee a level of accessibility of the LibreOffice user interface. This document describes the principles of the heuristics and can thus be used as a guide for implementing the same kind of labelling checks over other user interface frameworks.

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.

The goal of scalable parallel programming is to program computer architectures composed of multiple processing units so that increasing the number of processing units leads to an increase in performance. Bulk Synchronous Parallel (BSP) is a widely used model for scalable parallel programming with predictable performance. BSPlib is a library for BSP programming in C. In BSPlib, parallel algorithms are expressed by intermingling instructions that control the global parallel structure, and instructions that express the local computation of each processing unit. This lets the programmer fine-tune synchronization, but also implement programs whose diverging parallel control flow obscures the underlying BSP structure. In practice however, the majority of BSPlib program are textually aligned, a property that ensures parallel control flow convergence. We examine three core aspects of BSPlib programs through the lens of textual alignment: synchronization, performanceandcommunication.First,wepresentastaticanalysisthatidentifiestextuallyalignedstatements and use it to verify safe synchronization. This analysis has been implemented in Frama-C and certified in Coq. Second, we exploit textual alignment to develop a static performance analysis for BSPlib programs, based on classic cost analysis for sequential programs. Third, we develop a textual alignment-based sufficient condition for safe registration. Registration in BSPlib enables communication by Direct Remote Memory Access but is error prone. This development forms the basis for a future static analysis of registration.; La programmation parallèle consiste à utiliser des architectures à multiples unités de traitement, de manière à ce que le temps de calcul soit inversement proportionnel au nombre d’unités matérielles. Le modèle de BSP (Bulk Synchronous Parallel) permet de rendre le temps de calcul prévisible. BSPlib est une bibliothèque pour la programmation BSP en langage C. En BSPlib on entrelace des instructions de contrôle de la structure parallèle globale, et des instructions locales pour chaque unité de traitement. Cela permet des optimisations fines de la synchronisation, mais permet aussi l’écriture de programmes dont les calculs locaux divergent et masquent ainsi l’évolution globale du calcul BSP. Toutefois, les programmes BSPlib réalistes sont syntaxiquement alignés, une propriété qui garantit la convergence du flot de contrôle parallèle. Dans ce mémoire nous étudions les trois dimensions principales des programmes BSPlib du point de vue de l’alignement syntaxique : la synchronisation, le temps de calcul et la communication. D’abord nous présentons une analyse statique qui identifie les instructions syntaxiquement alignées et les utilise pour vérifier la sûreté de la synchronisation globale. Cette analyse a été implémentée en Frama-C et certifiée en Coq. Ensuite nous utilisons l’alignement syntaxique comme base d’une analyse statique du temps de calcul. Elle est fondée sur une analyse classique du coût pour les programmes séquentiels. Enfin nous définissons une condition suffisante pour la sûreté de l’enregistrement des variables. L’enregistrement en BSPlib permet la communication par accès aléatoire à la mémoire distante (DRMA) mais est sujet à des erreurs de programmation. Notre développement technique est la base d’une future analyse statique de ce mécanisme.

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.

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.

The last years have known an unprecedented growth in the use of mobile devices especially smartphones. They became omnipresent in our daily life because of the features they offer. They allow the user to install third-party apps to achieve numerous tasks. Smartphones are mostly governed by the Android operating system. It is today installed on more than 80% of the smartphones. Mobile apps collect a huge amount of data such as email addresses, contact list, geolocation, photos and bank account credentials. Consequently, Android has become a favorable target for cyber criminals. Thus, understanding the issue, i.e., how Android malware operates and how to detect it, became an important research challenge. Android malware frequently tries to bypass static analysis using multiple techniques such as code obfuscation and dynamic code loading. To overcome these limitations, many analysis techniques have been proposed to execute the app and monitor its behavior at runtime. Nevertheless, malware developers use time and logic bombs to prevent the malicious code from executing except under certain circumstances. Therefore, more actions are needed to trigger it and monitor its behavior. Recent approaches try to automatically characterize the malicious behavior by identifying the most suspicious locations in the code and forcing them to execute. They strongly rely on the computation of application global control flow graphs (CFGs). However, these CFGs are incomplete because they do not take into consideration all types of execution paths. These approaches solely analyze the application code and miss the execution paths that occur when the application calls a framework method that in turn calls another application method. We propose in this dissertation a tool, GPFinder, that automatically exhibits execution paths towards suspicious locations in the code by computing global CFGs that include edges representing explicit and implicit interprocedural calls. It also gives key information about the analyzed application in order to understand how the suspicious code was injected into the application. To validate our approach, we use GPFinder to study a collection of 14,224 malware samples, and we evaluate that 72.69% of the samples have at least one suspicious code location which is only reachable through implicit calls. Triggering approaches mainly use one of the following strategies to run a specific portion of the application's code: the first approach heavily modifies the app to launch the targeted code without keeping the original behavioral context. The second approach generates the input to force the execution flow to take the desired path without modifying the app's code. However, it is sometimes hard to launch a specific code location just by fuzzing the input. For instance, when the application performs a hash on the input data and compares the result to a fixed string to decide which branch of the condition to take, the fuzzing program should reverse the hashing function, which is obviously a hard problem. We propose in this dissertation a tool, TriggerDroid, that has a twofold goal: force the execution of the suspicious code and keep its context close to the original one. It crafts the required framework events to launch the right app component and satisfies the necessary triggering conditions to take the desired execution path. To validate our approach, we led an experiment on a dataset of 135 malware samples from 71 different families. Results show that our approach needs more refinement and adaptation to handle special cases due to the highly diverse malware dataset that we analyzed. Finally, we give a feedback on the experiments we led on different malware datasets, and we explain our experimental process. Finally, we present the Kharon dataset, a collection of well documented Android malware that can be used to understand the malware landscape.; Les smartphones sont devenus omniprésents dans notre vie quotidienne à cause des options qu'ils proposent. Aujourd'hui, Android est installé sur plus de 80% des smartphones. Les applications mobiles recueillent une grande quantité d'informations sur l'utilisateur. Par conséquent, Android est devenu une cible préférée des cybercriminels. Comprendre le fonctionnement des malwares et comment les détecter est devenu un défi de recherche important. Les malwares Android tentent souvent d'échapper à l'analyse statique en utilisant des techniques telles que l'obfuscation et le chargement dynamique du code. Des approches d'analyse ont été proposées pour exécuter l'application et surveiller son comportement. Néanmoins, les développeurs des malwares utilisent des bombes temporelles et logiques pour empêcher le code malveillant d'être exécuté sauf dans certaines circonstances. Par conséquent, plus d'actions sont requises pour déclencher et surveiller leurs comportements. Des approches récentes tentent de caractériser automatiquement le comportement malveillant en identifiant les endroits du code les plus suspicieux et en forçant leur exécution. Elles se basent sur le calcul des graphes de flot de contrôle (CFG) qui sont incomplets, car ils ne prennent pas en considération tous les types de chemins d'exécution. Ces approches analysent seulement le code d'application et ratent les chemins d'exécution générés quand l'application appelle une méthode du framework, qui appelle à son tour une autre méthode applicative. Nous proposons GPFinder, un outil qui extrait automatiquement les chemins d'exécution qui mènent vers les endroits suspicieux du code, en calculant des CFG qui incluent les appels interprocéduraux explicites et implicites. Il fournit aussi des informations clés sur l'application analysée afin de comprendre comment le code suspicieux a été injecté dans l'application. Pour valider notre approche, nous utilisons GPFinder pour étudier une collection de 14224 malwares Android. Nous évaluons que 72,69% des échantillons ont au moins un endroit suspicieux du code qui n'est atteignable qu'à travers des appels implicites. Les approches de déclenchement actuelles utilisent principalement deux stratégies pour exécuter une partie du code applicatif. La première stratégie consiste à modifier l'application excessivement pour lancer le code ciblé sans faire attention à son contexte originel. La seconde stratégie consiste à générer des entrées pour forcer le flot de contrôle à prendre le chemin désiré sans modifier le code d'application. Cependant, il est parfois difficile de lancer un endroit spécifique du code seulement en manipulant les entrées. Par exemple, quand l'application fait un hachage des données fournies en entrée et compare le résultat avec une chaîne de caractères fixe pour décider quelle branche elle doit prendre. Clairement, le programme de manipulation d'entrée devrait inverser la fonction de hachage, ce qui est presque impossible. Nous proposons TriggerDroid, un outil qui a deux buts : forcer l'exécution du code suspicieux et garder le contexte originel de l'application. Il fournit les événements framework requis pour lancer le bon composant et satisfait les conditions nécessaires pour prendre le chemin d'exécution désiré. Pour valider notre approche, nous avons fait une expérience sur 135 malwares Android de 71 familles différentes. Les résultats montrent que notre approche nécessite plus de raffinement et d'adaptation pour traiter les cas spéciaux dus à la grande diversité des échantillons analysés. Finalement, nous fournissons un retour sur les expériences que nous avons conduites sur différentes collections, et nous expliquons notre processus expérimental. Nous présentons le dataset Kharon, une collection de malwares Android bien documentés qui peuvent être utilisés pour comprendre le panorama des malwares Android.

Side-channel attacks are an especially dangerous form of attack. In this thesis, we focus on the timing side-channel. A program is said to be constant-time if it is not vulnerable to timing attacks. We present in this thesis two methods relying on static analysis in order to ensure that a program is constant-time. These methods use formal verification in order to gain the highest possible level of assurance by relying on a verified compilation toolchain made up of the CompCert compiler and the Verasco static analyzer. We also propose a proof methodology in order to ensure that a compiler preserves constant-time security during compilation.; Les attaques par canaux cachés sont une forme d'attaque particulièrement dangereuse. Dans cette thèse, nous nous intéressons au canal caché temporel. Un programme est dit ''constant-time'' lorsqu'il n'est pas vulnérable aux attaques par canal caché temporel. Nous présentons dans ce manuscrit deux méthodes reposant sur l'analyse statique afin de s'assurer qu'un programme est constant-time. Ces méthodes se placent dans le cadre de vérification formelle afin d'obtenir le plus haut niveau d'assurance possible en s'appuyant sur une chaîne de compilation vérifiée composée du compilateur CompCert et de l'analyseur statique Verasco. Nous proposons aussi une méthode de preuve afin de s'assurer qu'un compilateur préserve la propriété de constant-time lors de la compilation d'un programme.

Verifying distributed systems is a difficult problem on both theoretical and practice levels, in particular when systems are capable of local numerical computations. The goal of this thesis is to provide a formal verification method of such systems. We present a general model, based on abstract interpretation, allowing the construction of static analyses for systems of communicating processes. Our methodology is inspired by Regular Model Checking where the set of program states are represented as lattice automata and the program semantics are encoded using rewriting systems applied on the language recognized by the automata. This model offers the possiblity of expressing communications between processes as well as dynamic creation/destruction of process. Using the abstract interpretation methodology, we are able to provide a sound over-approximation of the reachability set of programs allowing us to verify numerical safety properties. We implemented this method allowing us to automatically analyse programs that use the distributed computation library MPI/C.; La vérification de systèmes distribués est un problème complexe pour de nombreuses raisons tant théoriques que pratiques, en particulier lorsque ces systèmes sont capables d'effectuer localement des calculs numériques. Le but de cette thèse est de proposer une méthode de vérification formelle de tels systèmes. Nous présentons un modèle général, basé sur l'interprétation abstraite, permettant de construire des analyses statiques pour des systèmes de processus communiquants. Notre méthodologie s'inspire du Regular Model Checking en représentant des ensembles d'états de programmes concurrents sous la forme d'automates de treillis et la sémantique de ces programmes comme la réécriture des langages reconnus par ces automates. Ce modèle nous permet notamment d'exprimer des communications entre processus et des créations/destructions dynamiques de processus. L'utilisation de l'interprétation abstraite nous permet d'obtenir une sur-approximation sûre de l'espace d'atteignabilité des programmes nous permettant ainsi de vérifier des propriétés de sûreté numériques. Nous avons implanté cette méthode permettant d'analyser automatiquement des programmes utilisant la bibliothèque logicielle de calculs distribués MPI/C.

Verifying distributed systems is a difficult problem on both theoretical and practice levels, in particular when systems are capable of local numerical computations. The goal of this thesis is to provide a formal verification method of such systems. We present a general model, based on abstract interpretation, allowing the construction of static analyses for systems of communicating processes. Our methodology is inspired by Regular Model Checking where the set of program states are represented as lattice automata and the program semantics are encoded using rewriting systems applied on the language recognized by the automata. This model offers the possiblity of expressing communications between processes as well as dynamic creation/destruction of process. Using the abstract interpretation methodology, we are able to provide a sound over-approximation of the reachability set of programs allowing us to verify numerical safety properties. We implemented this method allowing us to automatically analyse programs that use the distributed computation library MPI/C.; La vérification de systèmes distribués est un problème complexe pour de nombreuses raisons tant théoriques que pratiques, en particulier lorsque ces systèmes sont capables d'effectuer localement des calculs numériques. Le but de cette thèse est de proposer une méthode de vérification formelle de tels systèmes. Nous présentons un modèle général, basé sur l'interprétation abstraite, permettant de construire des analyses statiques pour des systèmes de processus communiquants. Notre méthodologie s'inspire du Regular Model Checking en représentant des ensembles d'états de programmes concurrents sous la forme d'automates de treillis et la sémantique de ces programmes comme la réécriture des langages reconnus par ces automates. Ce modèle nous permet notamment d'exprimer des communications entre processus et des créations/destructions dynamiques de processus. L'utilisation de l'interprétation abstraite nous permet d'obtenir une sur-approximation sûre de l'espace d'atteignabilité des programmes nous permettant ainsi de vérifier des propriétés de sûreté numériques. Nous avons implanté cette méthode permettant d'analyser automatiquement des programmes utilisant la bibliothèque logicielle de calculs distribués MPI/C.

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.

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.

Data structured in the Resource Description Framework (RDF) are increasingly available in large volumes. This leads to a major need and research interest in novel methods for query analysis and compilation for making the most of RDF data extraction. SPARQL is the widely used and well supported standard query language for RDF data. In parallel to query language evolutions, schema languages for expressing constraints on RDF datasets also evolve. Shape Expressions (ShEx) are increasingly used to validate RDF data, and to communicate expected graph patterns. Schemas in general are important for static analysis tasks such as query optimisation and containment. Our purpose is to investigate the means and methodologies for SPARQL query static analysis and optimisation in the presence of ShEx schema constraints.Our contribution is mainly divided into two parts. In the first part we consider the problem of SPARQL query containment in the presence of ShEx constraints. We propose a sound and complete procedure for the problem of containment with ShEx, considering several SPARQL fragments. Particularly our procedure considers OPTIONAL query patterns, that turns out to be an important feature to be studied with schemas. We provide complexity bounds for the containment problem with respect to the language fragments considered. We also propose alternative method for SPARQL query containment with ShEx by reduction into First Order Logic satisfiability, which allows for considering SPARQL fragment extension in comparison to the first method. This is the first work addressing SPARQL query containment in the presence of ShEx constraints.In the second part of our contribution we propose an analysis method to optimise the evaluation of conjunctive SPARQL queries, on RDF graphs, by taking advantage of ShEx constraints. The optimisation is based on computing and assigning ranks to query triple patterns, dictating their order of execution. The presence of intermediate joins between the query triple patterns is the reason why ordering is important in increasing efficiency. We define a set of well-formed ShEx schemas, that possess interesting characteristics for SPARQL query optimisation. We then develop our optimisation method by exploiting information extracted from a ShEx schema. We finally report on evaluation results performed showing the advantages of applying our optimisation on the top of an existing state-of-the-art query evaluation system.; La disponibilité de gros volumes de données structurées selon le modèle Resource Description Framework (RDF) est en constante augmentation. Cette situation implique un intérêt scientifique et un besoin important de rechercher de nouvelles méthodes d’analyse et de compilation de requêtes pour tirer le meilleur parti de l’extraction de données RDF. SPARQL est le plus utilisé et le mieux supporté des langages de requêtes sur des données RDF. En parallèle des langages de requêtes, les langages de définition de schéma d’expression de contraintes sur des jeux de données RDF ont également évolués. Les Shape Expressions (ShEx) sont de plus en plus utilisées pour valider des données RDF et pour indiquer les motifs de graphes attendus. Les schémas sont importants pour les tâches d’analyse statique telles que l’optimisation ou l’injection de requêtes. Notre intention est d’examiner les moyens et méthodologies d’analyse statique et d’optimisation de requêtes associés à des contraintes de schéma.Notre contribution se divise en deux grandes parties. Dans la première, nous considérons le problème de l’injection de requêtes SPARQL en présence de contraintes ShEx. Nous proposons une procédure rigoureuse et complète pour le problème de l’injection de requêtes avec ShEx, en prenant en charge plusieurs fragments de SPARQL. Plus particulièrement, notre procédure gère les patterns de requêtes OPTIONAL, qui s’avèrent former un important fonctionnalité à étudier avec les schémas. Nous fournissons ensuite les limites de complexité de notre problème en considération des fragments gérés. Nous proposons également une méthode alternative pour l’injection de requêtes SPARQL avec ShEx. Celle-ci réduit le problème à une satisfiabilité de Logique de Premier Ordre, qui permet de considérer une extension du fragment SPARQL traité par la première méthode. Il s’agit de la première étude traitant l’injection de requêtes SPARQL en présence de contraintes ShEx.Dans la seconde partie de nos contributions, nous proposons une méthode d’analyse pour optimiser l’évaluation de requêtes SPARQL groupées, sur des graphes RDF, en tirant avantage des contraintes ShEx. Notre optimisation s’appuie sur le calcul et l’assignation de rangs aux triple patterns d’une requête, permettant de déterminer leur ordre d’exécution. La présence de jointures intermédiaires entre ces patterns est la raison pour laquelle l’ordonnancement est important pour gagner en efficicacité. Nous définissons un ensemble de schémas ShEx bien- formulés, qui possède d’intéressantes caractéristiques pour l’optimisation de requêtes SPARQL. Nous développons ensuite notre méthode d’optimisation par l’exploitation d’informations extraites d’un schéma ShEx. Enfin, nous rendons compte des résultats des évaluations effectuées, montrant les avantages de l’application de notre optimisation face à l’état de l’art des systèmes d’évaluation de requêtes.

Data structured in the Resource Description Framework (RDF) are increasingly available in large volumes. This leads to a major need and research interest in novel methods for query analysis and compilation for making the most of RDF data extraction. SPARQL is the widely used and well supported standard query language for RDF data. In parallel to query language evolutions, schema languages for expressing constraints on RDF datasets also evolve. Shape Expressions (ShEx) are increasingly used to validate RDF data, and to communicate expected graph patterns. Schemas in general are important for static analysis tasks such as query optimisation and containment. Our purpose is to investigate the means and methodologies for SPARQL query static analysis and optimisation in the presence of ShEx schema constraints.Our contribution is mainly divided into two parts. In the first part we consider the problem of SPARQL query containment in the presence of ShEx constraints. We propose a sound and complete procedure for the problem of containment with ShEx, considering several SPARQL fragments. Particularly our procedure considers OPTIONAL query patterns, that turns out to be an important feature to be studied with schemas. We provide complexity bounds for the containment problem with respect to the language fragments considered. We also propose alternative method for SPARQL query containment with ShEx by reduction into First Order Logic satisfiability, which allows for considering SPARQL fragment extension in comparison to the first method. This is the first work addressing SPARQL query containment in the presence of ShEx constraints.In the second part of our contribution we propose an analysis method to optimise the evaluation of conjunctive SPARQL queries, on RDF graphs, by taking advantage of ShEx constraints. The optimisation is based on computing and assigning ranks to query triple patterns, dictating their order of execution. The presence of intermediate joins between the query triple patterns is the reason why ordering is important in increasing efficiency. We define a set of well-formed ShEx schemas, that possess interesting characteristics for SPARQL query optimisation. We then develop our optimisation method by exploiting information extracted from a ShEx schema. We finally report on evaluation results performed showing the advantages of applying our optimisation on the top of an existing state-of-the-art query evaluation system.; La disponibilité de gros volumes de données structurées selon le modèle Resource Description Framework (RDF) est en constante augmentation. Cette situation implique un intérêt scientifique et un besoin important de rechercher de nouvelles méthodes d’analyse et de compilation de requêtes pour tirer le meilleur parti de l’extraction de données RDF. SPARQL est le plus utilisé et le mieux supporté des langages de requêtes sur des données RDF. En parallèle des langages de requêtes, les langages de définition de schéma d’expression de contraintes sur des jeux de données RDF ont également évolués. Les Shape Expressions (ShEx) sont de plus en plus utilisées pour valider des données RDF et pour indiquer les motifs de graphes attendus. Les schémas sont importants pour les tâches d’analyse statique telles que l’optimisation ou l’injection de requêtes. Notre intention est d’examiner les moyens et méthodologies d’analyse statique et d’optimisation de requêtes associés à des contraintes de schéma.Notre contribution se divise en deux grandes parties. Dans la première, nous considérons le problème de l’injection de requêtes SPARQL en présence de contraintes ShEx. Nous proposons une procédure rigoureuse et complète pour le problème de l’injection de requêtes avec ShEx, en prenant en charge plusieurs fragments de SPARQL. Plus particulièrement, notre procédure gère les patterns de requêtes OPTIONAL, qui s’avèrent former un important fonctionnalité à étudier avec les schémas. Nous fournissons ensuite les limites de complexité de notre problème en considération des fragments gérés. Nous proposons également une méthode alternative pour l’injection de requêtes SPARQL avec ShEx. Celle-ci réduit le problème à une satisfiabilité de Logique de Premier Ordre, qui permet de considérer une extension du fragment SPARQL traité par la première méthode. Il s’agit de la première étude traitant l’injection de requêtes SPARQL en présence de contraintes ShEx.Dans la seconde partie de nos contributions, nous proposons une méthode d’analyse pour optimiser l’évaluation de requêtes SPARQL groupées, sur des graphes RDF, en tirant avantage des contraintes ShEx. Notre optimisation s’appuie sur le calcul et l’assignation de rangs aux triple patterns d’une requête, permettant de déterminer leur ordre d’exécution. La présence de jointures intermédiaires entre ces patterns est la raison pour laquelle l’ordonnancement est important pour gagner en efficicacité. Nous définissons un ensemble de schémas ShEx bien- formulés, qui possède d’intéressantes caractéristiques pour l’optimisation de requêtes SPARQL. Nous développons ensuite notre méthode d’optimisation par l’exploitation d’informations extraites d’un schéma ShEx. Enfin, nous rendons compte des résultats des évaluations effectuées, montrant les avantages de l’application de notre optimisation face à l’état de l’art des systèmes d’évaluation de requêtes.

In this technical report we dene an encoding from Lustre programs to Array HornClauses.; Dans ce rapport nous étudions l'analyse statique de programmes Lustre via unencodage vers des clauses de Horn à Tableaux.

We look forward to improving the implementations of information flow control mechanisms in Linux Operating Systems. Information Flow Control aims at monitoring how information disseminates in a system once it is out of its original container, unlike access control which can merely apply rule on how the containers are accessed. We met several scientific and technical challenges. First of all, the Linux codebase is big, over fifteen millions lines of code spread over thirty three thousand files. The first contribution of this thesis is a plugin for the GCC compiler able to extract and let a user easily visualize the control flow graphs of the Linux kernel functions. Secondly, the Linux Security Modules framework which is used to implement the information flow trackers we have reviewed (Laminar, KBlare, and Weir) was designed in the first place to implement access control, rather than information flow control. One issue is thus left open: is the framework implemented in such a way that all flows generated by system calls can be captured? We have created and implemented static analysis to address this problem and proved its correction with the Coq proof assistant system. This analysis is implemented as a GCC plugin and have allowed us to improve the LSM framework in order to capture all flows. Finally, we have noted that current information flow trackers are vulnerable to race conditions between flows and are unable to cover some overt channels of information such as files mapping to memory and shared memory segments between processes. We have implemented Rfblare, a new algorithm of flow tracking, for KBlare. The correction of this algorithm has been proved with Coq. We have showed that LSM can be used successfully to implement information flow control, and that only formal methods, leading to reusable methodology, analysis, tools, etc., are a match for the complexity and the fast-paced evolution of the Linux kernel.; Nous cherchons à améliorer l'état de l'art des implémentations de contrôle de flux d'information dans les systèmes Linux. Le contrôle de flux d'information vise à surveiller la façon dont l'information se dissémine dans le système une fois hors de son conteneur d'origine, contrairement au contrôle d'accès qui ne peut permettre d'appliquer des règles que sur la manière dont les conteneurs sont accédés. Plusieurs défis scientifiques et techniques se sont présentés. Premièrement, la base de code Linux est particulièrement grande, avec quinze millions de lignes de code réparties dans trente-mille fichiers. La première contribution de cette thèse a été un plugin pour le compilateur GCC permettant d'extraire et visualiser aisément les graphes de flot de contrôle des fonctions du noyau. Ensuite, le framework des Linux Security Modules qui est utilisé pour implémenter les moniteurs de flux d'information que nous avons étudiés (Laminar [1], KBlare [2] et Weir [3]) a été conçu en premier lieu pour le contrôle d'accès, et non de flux. La question se pose donc de savoir si le framework est implémenté de telle sorte à permettre la capture de tous les flux produits par les appels système. Nous avons créé et implémenté une analyse statique permettant de répondre à ce problème. Cette analyse statique est implémenté en tant que plugin GCC et nous a permis d'améliorer le framework LSM pour capturer tous les flux. Enfin, nous avons constaté que les moniteurs de flux actuels n'étaient pas résistants aux conditions de concurrence entre les flux et ne pouvaient pas traiter certains canaux ouverts tels que les projections de fichiers en mémoire et les segments de mémoire partagée entre processus. Nous avons implémenté Rfblare, un nouvel algorithme de suivi de flux, pour KBlare, dont nous avons prouvé la correction avec Coq. Nous avons ainsi montré que LSM pouvait être utilisé avec succès pour implémenter le contrôle de flux d'information, et que seules les méthodes formelles, permettant la mise en œuvre de méthodologie, d'analyses ou d'outils réutilisables, permettaient de s'attaquer à la complexité et aux rapides évolutions du noyau Linux.

This thesis was motivated by the emergence of massively parallel processing and supercomputingthat tend to make computer programming extremely performing. Speedup, the power consump-tion, and the efficiency of both software and hardware are nowadays the main concerns of theinformation systems community. Handling memory in a correct and efficient way is a step towardless complex and more performing programs and architectures. This thesis falls into this contextand contributes to memory analysis and compilation fields in both theoretical and experimentalaspects.Besides the deep study of the current state-of-the-art of memory analyses and their limitations,our theoretical results stand in designing new algorithms to recover part of the imprecisionthat published techniques still show. Among the present limitations, we focus our research onthe pointer arithmetic to disambiguate pointers within the same data structure. We develop ouranalyses in the abstract interpretation framework. The key idea behind this choice is correctness,and scalability: two requisite criteria for analyses to be embedded to the compiler construction.The first alias analysis we design is based on the range lattice of integer variables. Given a pair ofpointers defined from a common base pointer, they are disjoint if their offsets cannot have valuesthat intersect at runtime. The second pointer analysis we develop is inspired from the Pentagonabstract domain. We conclude that two pointers do not alias whenever we are able to build astrict relation between them, valid at program points where the two variables are simultaneouslyalive. In a third algorithm we design, we combine both the first and second analysis, and enhancethem with a coarse grained but efficient analysis to deal with non related pointers.We implement these analyses on top of the LLVM compiler. We experiment and evaluate theirperformance based on two metrics: the number of disambiguated pairs of pointers compared tocommon analyses of the compiler, and the optimizations further enabled thanks to the extraprecision they introduce; La rapidité, la consommation énergétique et l'efficacité des systèmes logiciels et matériels sont devenues les préoccupations majeures de la communauté informatique de nos jours. Gérer de manière correcte et efficace les problématiques mémoire est essentiel pour le développement des programmes de grande tailles sur des architectures de plus en plus complexes. Dans ce contexte, cette thèse contribue aux domaines de l'analyse mémoire et de la compilation tant sur les aspects théoriques que sur les aspects pratiques et expérimentaux. Outre l'étude approfondie de l'état de l'art des analyses mémoire et des différentes limitations qu'elles montrent, notre contribution réside dans la conception et l'évaluation de nouvelles analyses qui remédient au manque de précision des techniques publiées et implémentées. Nous nous sommes principalement attachés à améliorer l'analyse de pointeurs appartenant à une même structure de données, afin de lever une des limitations majeures des compilateurs actuels. Nous développons nos analyses dans le cadre général de l'interprétation abstraite « non dense ». Ce choix est motivé par les aspects de correction et d'efficacité : deux critères requis pour une intégration facile dans un compilateur. La première analyse que nous concevons est basée sur l'analyse d'intervalles des variables entières ; elle utilise le fait que deux pointeurs définis à l'aide d'un même pointeur de base n'aliasent pas si les valeurs possibles des décalages sont disjointes. La seconde analyse que nous développons est inspirée du domaine abstrait des Pentagones ; elle génère des relations d'ordre strict entre des paires de pointeurs comparables. Enfin, nous combinons et enrichissons les deux analyses précédentes dans un cadre plus général. Ces analyses ont été implémentées dans le compilateur LLVM. Nous expérimentons et évaluons leurs performances, et les comparons aux implémentations disponibles selon deux métriques : le nombre de paires de pointeurs pour lesquelles nous inférons le non-aliasing et les optimisations rendues possibles par nos analyses

In the field of software verification, the frame problem refers to establishing the boundaries within which program elements operate. It has notoriously tedious consequences on the specification of frame properties, which indicate the parts of the program state that an operation is allowed to modify, as well as on their verification, i.e. proving that operations modify only what is specified by their frame properties. In the context of interactive formal verification of complex systems, such as operating systems, much effort is spent addressing these consequences and proving the preservation of the systems' invariants. However, most operations have a localized effect on the system and impact only a limited number of invariants at the same time. In this thesis we address the issue of identifying those invariants that are unaffected by an operation and we present a solution for automatically inferring their preservation. Our solution is meant to ease the proof burden for the programmer. It is based on static analysis and does not require any additional frame annotations. Our strategy consists in combining a dependency analysis and a correlation analysis. We have designed and implemented both static analyses for a strongly-typed, functional language that handles structures, variants and arrays. The dependency analysis computes a conservative approximation of the input fragments on which functional properties and operations depend. The correlation analysis computes a safe approximation of the parts of an input state to a function that are copied to the output state. It summarizes not only what is modified but also how it is modified and to what extent. By employing these two static analyses and by subsequently reasoning based on their combined results, an interactive theorem prover can automate the discharching of proof obligations for unmodified parts of the state. We have applied both of our static analyses to a functional specification of a micro-kernel and the obtained results demonstrate both their precision and their scalability.; Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites constituent les propriétés de frame (frame properties en anglais). Elles sont habituellement spécifiées manuellement par le programmeur et leur validité doit être vérifiée: il est nécessaire de prouver que les opérations du programme n'outrepassent pas les limites ainsi déclarées. Dans le contexte de la vérification formelle interactive de systèmes complexes, comme les systèmes d'exploitation, un effort considérable est investi dans la spécification et la preuve des propriétés de frame. Cependant, la plupart des opérations ont un effet très localisé et ne menacent donc qu'un nombre limité d'invariants. Étant donné que la spécification et la preuve de propriétés de frame est une tache fastidieuse, il est judicieux d'automatiser l'identification des invariants qui ne sont pas affectés par une opération donnée. Nous présentons dans cette thèse une solution inférant automatiquement leur préservation. Notre solution a pour but de réduire le nombre de preuves à la charge du programmeur. Elle est basée sur l'analyse statique, et ne nécessite aucune annotation de frame. Notre stratégie consiste à combiner une analyse de dépendances avec une analyse de corrélations. Nous avons conçu et implémenté ces deux analyses statiques pour un langage fonctionnel fortement typé qui manipule structures, variants et tableaux. Typiquement, une propriété fonctionnelle ne dépend que de quelques fragments de l'état du programme. L'analyse de dépendances détermine quelles parties de cet état influent sur le résultat de la propriété fonctionnelle. De même, une fonction ne modifiera que certaines parties de ses arguments, copiant le reste à l'identique. L'analyse de corrélations détecte quelles parties de l'entrée d'une fonction se retrouvent copiées directement (i.e. non modifiés) dans son résultat. Ces deux analyses calculent une approximation conservatrice. Grâce aux résultats de ces deux analyses statiques, un prouveur de théorèmes interactif peut inférer automatiquement la préservation des invariants qui portent sur la partie non affectée par l’opération concernée. Nous avons appliqué ces deux analyses statiques à la spécification fonctionnelle d'un micro-noyau, et obtenu des résultats non seulement d'une précision adéquate, mais qui montrent par ailleurs que notre approche peut passer à l'échelle.

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.

Critical software based on floating-point arithmetic requires rigorous verification and validation process to improve our confidence in their reliability and their safety. Unfortunately available techniques for this task often provide overestimates of the round-off errors. We can cite Arian 5, Patriot rocket as well-known examples of disasters. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their numerical accuracy and, in this work, we go one step further by automatically transforming larger pieces of code containing assignments, control structures and functions. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve, by re-parsing, the numerical accuracy of the program results. We use abstract interpretation based static analysis techniques to over-approximate the round-off errors in programs and during the transformation of expressions. A tool has been implemented and experimental results are presented concerning classical numerical algorithms and algorithms for embedded systems.; Les systèmes critiques basés sur l’arithmétique flottante exigent un processus rigoureux de vérification et de validation pour augmenter notre confiance en leur sureté et leur fiabilité. Malheureusement, les techniques existentes fournissent souvent une surestimation d’erreurs d’arrondi. Nous citons Arian 5 et le missile Patriot comme fameux exemples de désastres causés par les erreurs de calculs. Ces dernières années, plusieurs techniques concernant la transformation d’expressions arithmétiques pour améliorer la précision numérique ont été proposées. Dans ce travail, nous allons une étape plus loin en transformant automatiquement non seulement des expressions arithmétiques mais des programmes complets contenant des affectations, des structures de contrôle et des fonctions. Nous définissons un ensemble de règles de transformation permettant la génération, sous certaines conditions et en un temps polynômial, des expressions pluslarges en appliquant des calculs formels limités, au sein de plusieurs itérations d’une boucle. Par la suite, ces larges expressions sont re-parenthésées pour trouver la meilleure expression améliorant ainsi la précision numérique des calculs de programmes. Notre approche se base sur les techniques d’analyse statique par interprétation abstraite pour sur-rapprocher les erreurs d’arrondi dans les programmes et au moment de la transformation des expressions. Cette approche est implémenté dans notre outil et des résultats expérimentaux sur des algorithmes numériques classiques et des programmes venant du monde d’embarqués sont présentés.

Biological Regulatory Networks (BRNs) are usually used in systems biology for modelling, understanding and controlling the dynamics of different biological functions (differentiation, proliferation, proteins synthesis, apoptose) inside cells. Those networks are enhanced with experimental data that are nowadays more available which give an idea on the dynamics of BRNs components. Formal analysis of such models fails in front of the combinatorial explosion of generated behaviours despite the fact that BRNs provide abstract representation of biological systems. This thesis handles hybrid modelling, the simulation, the formal verification and control of Large Biological Regulatory Networks. This modelling is done thanks to stochastic automata networks, thereafter to Process Hitting by integrating time-series data. Firstly, this thesis proposes a refining of the dynamics by estimation of stochastic and temporal (delay) parameters from time-series data and integration of those parameters in automata networks models. This integration allows the parametrisation of the transitions between the states of the system. Then, a statistical analysis of the traces of the stochastic simulation is proposed to compare the dynamics of simulations with the experimental data. Secondly, this thesis develops static analysis by abstract interpretation in the automata networks allowing efficient under- and over-approximation of quantitative (probability and delay) reachability properties. This analysis enables to highlight the critical components to satisfy these properties. Finally, taking advantage from the previous developed static analyses for the reachability properties in the qualitative point of view, and from the power of logic programming (Answer Set Programming), this thesis addresses the domain of control of system by proposing the identification of bifurcation transitions. Bifurcations are transitions after which the system can no longer reach a state that was previously reachable.; Les Réseaux de Régulation biologique (RRB) sont couramment utilisés en biologie des systèmes pour modéliser, comprendre et contrôler les dynamiques des différentes fonctions biologiques (différenciation, synthèse protéique, apoptose) au sein des cellules. Ces réseaux sont enrichis des données expérimentales de plus en plus nombreuses et disponibles qui renseignent sur les dynamiques des composants des RRB. L'analyse formelle de tels modèles se heurte rapidement à l'explosion combinatoire des comportements engendrés malgré le fait que les RRB offrent une représentation abstraite des systèmes biologiques. Cette thèse traite de la modélisation hybride, de la simulation, de la vérification formelle et du contrôle des grands Réseaux de Régulation Biologique. Cette modélisation est effectuée grâce aux réseaux d'automates stochastiques, puis aux Frappes de Processus qui en sont une restriction, en intégrant des données de séries temporelles. En premier lieu, cette thèse propose un raffinement des dynamiques par l'estimation des paramètres stochastiques et temporels (délais) à partir des données de séries temporelles et l'intégration de ces paramètres dans les modèles en réseaux d'automates. Cette intégration permet de paramétrer les transitions entre les états du système. Puis, une analyse statistique des traces des simulations stochastiques est proposée afin de comparer les dynamiques des simulations à celles des données expérimentales. En deuxième lieu, cette thèse développe une analyse statique par interprétation abstraite dans les réseaux d'automates permettant des approximations inférieures et supérieures très efficaces des propriétés d'accessibilité d'un point de vue quantitatif (probabilité et délai). Cette analyse permet de faire apparaître des composants critiques pour la satisfaction de ces propriétés. Enfin, tirant avantage des analyses statiques développées pour l'accessibilité dans les réseaux d'automates, et de la puissance de la programmation logique (ASP), cette thèse aborde le domaine du contrôle des systèmes en proposant l'identification des transitions de bifurcation. Les bifurcations sont des transitions après lesquelles le système ne peut plus atteindre un état précédemment accessible.

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