.

La représentation symbolique des masques de circuits intégrés est connue depuis environ quinze ans, mais n'est développée que depuis quelques années. Presque tous les systèmes de CAO développés récemment font usage d'une représentation symbolique des masques de circuits afin de simplifier la conception. Dans cette thèse, un système symbolique hiérarchique de dessin des masques est décrit. Un langage de description et un environnement graphique sont présentés. L'environnement graphique est utilise pour l'édition de cellules et de blocs, hiérarchiquement. Le langage textuel peut être considéré comme le langage cible de tous les outils de synthèse ou de compilation qui sont développés dans le cadre d'un système intégré de CAO VLSI. Une représentation métrique des circuits est donnée, et un "assembleur de silicium" qui permet le dessin hiérarchique de cellules fonctionnelles en accord avec les structures d'interconnexions de base, est décrit. Par un programme Lisp le concepteur définit comment les cellules feuilles doivent être assemblées pour réaliser la fonction désirée. Ainsi des cellules fonctionnelles peuvent être générées, avec une représentation symbolique et une fonctionnalité déterminée.

Cette thèse s'intéresse à la sécurité des programmes embarqués face aux attaques par injection de fautes. La prolifération des composants embarqués et la simplicité de mise en œuvre des attaques rendent impérieuse l'élaboration de contre-mesures.Un modèle de fautes par l'expérimentation basé sur des attaques par impulsion électromagnétique a été élaboré. Les résultats expérimentaux ont montré que les fautes réalisées étaient dues à la corruption des transferts sur les bus entre la mémoire Flash et le pipeline du processeur. Ces fautes permettent de réaliser des remplacements ou des saut d'instructions ainsi que des modifications de données chargées depuis la mémoire Flash. Le remplacement d'une instruction par une autre bien spécifique est très difficile à contrôler ; par contre, le saut d'une instruction ciblée a été observé fréquemment, est plus facilement réalisable, et permet de nombreuses attaques simples. Une contre-mesure empêchant ces attaques par saut d'instruction, en remplaçant chaque instruction par une séquence d'instructions, a été construite et vérifiée formellement à l'aide d'outils de model-checking. Cette contre-mesure ne protège cependant pas les chargements de données depuis la mémoire Flash. Elle peut néanmoins être combinée avec une autre contre-mesure au niveau assembleur qui réalise une détection de fautes. Plusieurs expérimentations de ces contre-mesures ont été réalisées, sur des instructions isolées et sur des codes complexes issus d'une implémentation de FreeRTOS. La contre-mesure proposée se révèle être un très bon complément pour cette contre-mesure de détection et permet d'en corriger certains défauts. / This thesis focuses on the security of embedded programs against fault injection attacks. Due to the spreadings of embedded systems in our common life, development of countermeasures is important.First, a fault model based on practical experiments with a pulsed electromagnetic fault injection technique has been built. The experimental results show that the injected faults were due to the corruption of the bus transfers between the Flash memory and the processor’s pipeline. Such faults enable to perform instruction replacements, instruction skips or to corrupt some data transfers from the Flash memory.Although replacing an instruction with another very specific one is very difficult to control, skipping an instruction seems much easier to perform in practice and has been observed very frequently. Furthermore many simple attacks can carried out with an instruction skip. A countermeasure that prevents such instruction skip attacks has been designed and formally verified with model-checking tool. The countermeasure replaces each instruction by a sequence of instructions. However, this countermeasure does not protect the data loads from the Flash memory. To do this, it can be combined with another assembly-level countermeasure that performs a fault detection. A first experimental test of these two countermeasures has been achieved, both on isolated instructions and complex codes from a FreeRTOS implementation. The proposed countermeasure appears to be a good complement for this detection countermeasure and allows to correct some of its flaws.

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.

Le compilateur de parties opératives Apollon qui est présenté dans cette thèse, génère automatiquement le dessin des masques de parties opératives de circuits VLSI de type microprocesseur à partir d'une description comportementale de niveau transfert de registres constituée d'un ensemble non ordonné d'instructions opératives. Une instruction opérative est formée d'un ensemble d'actions opératives dont le format est prédéfini (transferts - opérations unaires ou binaires et entrées-sorties) devant se dérouler en parallèle en au plus deux cycles opératifs. Un cycle opératif comprend 4 phases qui correspondent aux 4 phases d'exécution d'un transfert entre 2 registres. Apollon est basé sur un modèle dérivé de la partie opérative du MC68000. Ce modèle fournit à la fois: un modèle architectural: la partie opérative est formée d'un ensemble de sous parties opératives alignées à deux bus qui traversent tous les éléments d'une sous partie opérative; un modèle temporel: une opération prend 2 cycles, un transfert un seul; un modèle électrique: les bus sont complémentés et à précharge; un modèle topologique: le plan de masse est basé sur la structure en tranches appelée communément bis slice. Le compilateur génère d'abord l'architecture de la partie opérative, puis les spécification des masques à partir de cette architecture. Pour générer l'architecture de la partie opérative en un temps raisonnable, le compilateur doit recourir à des heuristiques. Pour générer le dessin des masques, le compilateur utilise l'assembleur de silicium Lubrick qui permet d'assembler et de connecter automatiquement les cellules de base des éléments fonctionnels de la partie opérative. Les spécifications des masques sont générées à partir des spécifications des cellules prédéfinies d'une bibliothèque NMOS.

Cette thèse présente des contributions dans les domaines de l'architecture des ordinateurs réalisés sous la forme d'un Circuit Intégré. Un assembleur de silicium, appelé LUBRICK, permet de décrire, dans un langage de programmation, la constitution d'un assemblage hiérarchisé de cellules pour réaliser la description complète des masques d'un Circuit Intégré. La compilation du silicium, discipline qui consiste à déduire les masques d'un circuit en partant d'une description fonctionnelle, est ici abordée sous un angle pratique, avec la présentation d'un compilateur prototype d'une forme de partie contrôle et des présentations de modèles topologiques de parties opératives et de parties contrôle qui servent de cible au compilateur

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.