Le chapitre 2 présente la première partie importante de nos travaux : l'approche pour la détection que nous proposons. Nous avons tout d'abord expliqué les caractéristiques des attaques contre les données de calcul et en quoi ces dernières se distinguent des autres types d'attaque. Ceci nous a notamment permis de montrer que pour perpétuer une intrusion, un utilisateur malveillant va chercher à cibler un ensemble bien précis de données de calcul. À l'aide de la logique de Hoare, nous avons ensuite expliqué que le code source des applications peut contenir des informations qui peuvent être utilisées pour détecter ce type bien précis d'attaque. Nous avons détaillé cela sur un exemple d'exploitation de vulnérabilité. Puis, nous avons présenté notre modèle de détection. Nous l'avons tout d'abord présenté empiriquement sur un cas réel d'attaques contre les données de calcul. Pour cela, nous avons détaillé la vulnérabilité utilisée dans notre exemple ainsi que les différents scénarios d'attaque et comment des invariants portant sur certaines variables permettent de détecter ces attaques. Enfin, nous avons présenté formellement notre modèle de détection. Celui-ci correspond à l'ensemble des domaines de variation des variables qui influencent l'exécution des appels de fonction. Ces domaines de variation sont calculés juste avant les appels de fonction et uniquement pour les variables qui sont atteignables à ces endroits du code source. Nous avons ensuite présenté une méthode pour construire un tel modèle. Premièrement, nous proposons d'utiliser le graphe de dépendance du programme pour déterminer pour chaque appel de fonction l'ensemble des variables qui influencent son exécution. Deuxièmement, nous proposons d'utiliser l'interprétation abstraite pour calculer pour chacun de ces ensembles de variables leur domaine de variation. Pour finir, nous présentons une implémentation de notre approche que nous avons réalisée pour les programmes écrits en langage C. Nous détaillons d'abord la phase de construction du modèle qui repose sur un outil d'analyse statique existant, Frama-C. Nous détaillons ensuite la phase d'instrumentation, celle-ci ayant pour contrainte de ne pas modifier le processus original de compilation. Le chapitre 3 présente la seconde partie importante de nos travaux : l'approche pour l'évaluation que nous proposons. Nous commençons par aborder la problématique de la simulation des erreurs engendrées par les attaques contre les données de calcul. Pour cela, nous présentons d'abord le modèle de faute que nous proposons pour simuler ce type bien particulier d'attaques. Nous étudions les caractéristiques qui doivent être simulées, quel sera leur impact sur le programme et dans quel cas ces dernières peuvent être détectées. Nous expliquons ensuite comment nous proposons de construire notre modèle de simulation. La principale problématique ici est de savoir comment déterminer l'ensemble des cibles potentielles. Il s'agit du même ensemble de variables que pour la détection. Nous proposons donc à nouveau de nous reposer sur le graphe de dépendance du programme et d'embarquer les mécanismes d'injection au sein des applications. Nous expliquons ensuite comment notre modèle de faute peut être utilisé pour l'évaluation d'un système de détection d'intrusion. Nous posons comme objectif que le résultat obtenu doit être une sur-approximation du taux de faux négatifs réel. Cela implique que nous voulons placer le système de détection d'intrusion à évaluer dans la situation la moins favorable possible. Pour respecter cette contrainte, nous montrons que notre modèle de faute doit être utilisé pour simuler une intrusion qui ne nécessite qu'une seule exploitation de la vulnérabilité, que la vulnérabilité donne accès à l'ensemble de l'espace mémoire du processus et que l'exploitation ne vise qu'une seule variable. Nous présentons enfin les modifications que nous avons apportées à notre outil afin qu'il instrumente aussi les programmes pour l'injection et comment les mécanismes d'injection ainsi ajoutés doivent être utilisés. Le chapitre 4 présente la dernière partie de nos travaux : l'évaluation de notre système de détection d'intrusion, notamment à l'aide de notre modèle de simulation d'attaque. Nous commençons par présenter la plateforme de tests que nous avons développée autour de nos mécanismes d'injection. Il s'agit d'une plateforme qui automatise la réalisation de tests ainsi que l'analyse des résultats obtenus. Nous abordons tout d'abord les problématiques d'écriture des scénarios d'exécution et de collecte des informations. Les scénarios doivent permettre de couvrir suffisamment le code des programmes utilisés pour les tests. Nous avons choisi de mesurer ce taux de couverture en fonction des appels de fonction. Les informations collectées sont utilisées pour produire deux résultats : une sur-approximation du taux réel de faux négatifs et une évaluation du taux de détection pour les injections ayant provoqué une déviation comportementale. Pour finir, nous présentons les résultats de l'évaluation de notre système de détection d'intrusion. Nous commençons par donner les performances de l'analyse. On note que la durée d'analyse peut être très grande, notamment en fonction de la taille du code à analyser, mais qu'en fonction de la sémantique du code, deux programmes de taille similaire peuvent présenter des durées d'analyse complètement différentes. Puis, nous donnons le niveau de surcharge à l'exécution. On note que la surcharge induite par nos mécanismes de détection est très faible, toujours inférieure à 1%. Nous continuons avec les performances de la détection. Nous pouvons voir que les résultats de la détection varient grandement d'un programme à l'autre, malgré un taux d'instrumentation similaire. Ce qui change, c'est le nombre d'invariants vérifiés. On voit ici la limite de notre approche : si la sémantique du code original ne permet pas de calculer suffisamment d'invariants, l'efficacité de notre approche sera alors limitée. De plus, la propagation de l'erreur n'apporte que peu d'aide à notre modèle de détection. Dans tous les cas, nous avons pu vérifier que notre approche ne génère bien pas de faux positif.

La criticité des programmes dépasse constamment de nouvelles frontières car ils sont de plus en plus utilisés dans la prise de décision (voitures autonomes, robots chirurgiens, etc.). Le besoin de développer des programmes sûrs et de vérifier les programmes existants émerge donc naturellement.Pour prouver formellement la correction d'un programme, il faut faire face aux défis de la mise à l'échelle et de la décidabilité. Programmes composés de millions de lignes de code, complexité de l'algorithme, concurrence, et même de simples expressions polynomiales font partis des problèmes que la vérification formelle doit savoir gérer. Pour y arriver, les méthodes formelles travaillent sur des abstractions des états des programmes étudiés afin d'analyser des approximations de leur comportement. L'analyse des boucles est un axe entier de la vérification formelle car elles sont encore aujourd'hui peu comprises. Bien que certaines d'entre elles peuvent facilement être traitées, il existe des exemples apparemment très simples mais dont le comportement n'a encore aujourd'hui pas été résolu (par exemple, on ne sait toujours pas pourquoi la suite de Syracuse, simple boucle linéaire, converge toujours vers 1).L'approche la plus commune pour gérer les boucles est l'utilisation d'invariants de boucle, c'est à dire de relations sur les variables manipulées par une boucle qui sont vraies à chaque fois que la boucle recommence. En général, les invariants utilisent les mêmes expressions que celles utilisées dans la boucle : si elle manipule explicitement la mémoire par exemple, on s'attend à utiliser des invariants portant sur la mémoire. Cependant, il existe des boucles contenant uniquement des affectations linéaires qui n'admettent pas d'invariants linéaires, mais polynomiaux.Les boucles linéaires sont elles plus expressives que ce qu'il paraîtrait ?Cette thèse présente de nouvelles propriétés sur les boucles linéaires et polynomiales. Il est déjà connu que les boucles linéaires sont polynomialement expressives, au sens ou si plusieurs variables évoluent linéairement dans une boucle, alors n'importe quel monôme de ces variables évolue linéairement. La première contribution de cette thèse est la caractérisation d'une sous classe de boucles polynomiales exactement aussi expressives que des boucles linéaires, au sens où il existe une boucle linéaire avec le même comportement. Ensuite, deux nouvelles méthodes de génération d'invariants sont présentées.La première méthode est basée sur l'interprétation abstraite et s'intéresse aux filtres linéaires convergents. Ces filtres jouent un rôle important dans de nombreux systèmes embarqués (dans l'avionique par exemple) et requièrent l'utilisation de flottants, un type de valeurs qui peut mener à des erreurs d'imprécision s'ils sont mal utilisés. Aussi, la présence d'affectations aléatoires dans ces filtres rend leur analyse encore plus complexe.La seconde méthode traite d'une approche différente basée sur la génération d'invariants pour n'importe quel type de boucles linéaires. Elle part d'un nouveau théorème présenté dans cette thèse qui caractérise les invariants comme étant les vecteurs propres de la transformation linéaire traitée. Cette méthode est généralisée pour prendre en compte les conditions, les boucles imbriquées et le non déterminisme dans les affectations.La génération d'invariants n'est pas un but en soi, mais un moyen. Cette thèse s'intéresse au genre de problèmes que peut résoudre les invariants générés par la seconde méthode. Le premier problème traité est problème de l'orbite (Kannan-Lipton Orbit problem), dont il est possible de générer des certificats de non accessibilité en utilisant les vecteurs propres de la transformation considerée. En outre, les vecteurs propres sont mis à l'épreuve en pratique par leur utilisation dans le model-checker CaFE basé sur la verification de propriétés temporelles sur des programmes C. / The criticality of programs constantly reaches new boundaries as they are relied on to take decisions in place of the user (autonomous cars, robot surgeon, etc.). This raised the need to develop safe programs and to verify the already existing ones.Anyone willing to formally prove the soundness of a program faces the two challenges of scalability and undecidability. Million of lines of code, complexity of the algorithm, concurrency, and even simple polynomial expressions are part of the issues formal verification have to deal with. In order to succeed, formal methods rely on state abstraction to analyze approximations of the behavior of the analyzed program.The analysis of loops is a full axis of formal verification, as this construction is still today not well understood. Though some of them can be easily handled when they perform simple operations, there still exist some seemingly basic loops whose behavior has not been solved yet (the Syracuse sequence for example is suspected to be undecidable).The most common approach for the treatment of loops is the use of loop invariants, i.e. relations on variables that are true at the beginning of the loop and after every step. In general, invariants are expected to use the same set of expressions used in the loop: if a loop manipulates the memory on a structure for example, invariants will naturally use expressions involving memory operations. However, there exist loops containing only linear instructions that admit only polynomial invariants (for example, the sum on integers $sumlimits_{i=0}^n i$ can be computed by a linear loop and is a degree 2 polynomial in n), hence using expressions that are syntacticallyabsent of the loop. Is the previous remark wrong then ?This thesis presents new insights on loops containing linear and polynomial instructions. It is already known that linear loops are polynomially expressive, in the sense that if a variable evolves linearly, then any monomial of this variable evolves linearly. The first contribution of this thesis is the extraction of a class of polynomial loops that is exactly as expressive as linear loops, in the sense that there exist a linear loop with the exact same behavior. Then, two new methods for generating invariants are presented.The first method is based on abstract interpretation and is focused on a specific kind of linear loops called linear filters. Linear filters play a role in many embedded systems (plane sensors for example) and require the use of floating point operations, that may be imprecise and lead to errors if they are badly handled. Also, the presence of non deterministic assignments makes their analysis even more complex.The second method treats of a more generic subject by finding a complete set of linear invariants of linear loops that is easily computable. This technique is based on the linear algebra concept of eigenspace. It is extended to deal with conditions, nested loops and non determinism in assignments.Generating invariants is an interesting topic, but it is not an end in itself, it must serve a purpose. This thesis investigates the expressivity of invariantsgenerated by the second method by generating counter examples for the Kannan-Lipton Orbit problem.It also presents the tool PILAT implementing this technique and compares its efficiency technique with other state-of-the-art invariant synthesizers. The effective usefulness of the invariants generated by PILAT is demonstrated by using the tool in concert with CaFE, a model-checker for C programs based on temporal logics.

Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes, et plus particulièrement des propriétés numériques. L'utilisation de la technique d'Analyse des Relations Linéaires, une interprétation abstraite fondée sur une approximation des états numériques par des polyèdres convexes, a fait ses preuves dans le domaine. Il s'agit de générer des surapproximations polyédriques de l'ensemble des valuations associées à chaque point de contrôle, l'introduction d'un opérateur d'élargissement assurant la convergence des analyses. Cependant dans certains cas les invariants générés ne sont pas assez précis, et l'amélioration de la précision via le retardement du moment d'application de l'élargissement est trop via le retardement du moment d'application de l'élargissement est trop coûteux. Nous nous sommes donc intéressés aux méthodes dites d'accélération, qui consistent à calculer exactement l'effet d'une ou plusieurs boucles (sous la forme de formules de Presburger), le principal inconvénient de ces méthodes étant qu'elles ne s'appliquent qu'à une classe restreinte de programmes.<br />Dans cette thèse nous proposons une approche combinant l'Analyse des Relations Linéaires classique (avec élargissement) et la notion d'Accélération abstraite utile pour calculer une surapproximation précise de l'application itérée de certains types de boucles, dans le but d'améliorer la précision des analyses tout en garantissant toujours la terminaison. Les premiers résultats expérimentaux obtenus grâce à l'implémentation de l'analyseur Aspic ont permis de valider la méthode, qui a le principal avantage de combiner amélioration de la précision et efficacité.

On introduit une nouvelle structure algébrique qui formalise bien les problèmes de reconstruction, assortie d'une conjecture qui permettrait de traiter directement des symétries. Le cadre fournit par cette étude permet de plus d'engendrer des relations qui ont lieu entre les nombres de sous-structures, et d'une certaine façon, la conjecture formulée affirme qu'on les obtient toutes. De plus, la généralisation des résultats précédemment obtenus pour la reconstruction permet de chercher 'a en apprécier les limites en recherchant des cas où ces relations sont optimales. Ainsi, on montre que les théorèmes de V.Müller et de L.Lovasz sont les meilleurs possibles en exhibant des cas limites. Cette généralisation aux algèbres d'invariants, déjà effectuée par P.J.Cameron et V.B.Mnukhin, permet de placer les problèmes de reconstruction en tenaille entre d'une part des relations (fournies) que l'on veut exploiter, et des exemples qui établissent l'optimalité du résultat. Ainsi, sans aucune donnée sur le groupe, le résultat de L.Lovasz est le meilleur possible, et si l'on considère l'ordre du groupe, le résultat de V.Müller est le meilleur possible.