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

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués.

Malgré les progrès importants effectués en matière de conception de logiciels et l'existence de méthodes de développement éprouvées, il faut reconnaître que les défaillances de systèmes causées par des logiciels restent fréquentes. Il arrive même que ces défaillances concernent des logiciels critiques et provoquent des dommages significatifs. Considérant l'importance des intérêts en jeu, et le fait que la garantie de logiciel "zéro défaut" est hors d'atteinte, il est donc important de pouvoir déterminer en cas de dommages causés par des logiciels les responsabilités des différentes parties. Pour établir ces responsabilités, un certain nombre de conditions doivent être réunies: (i) on doit pouvoir disposer d'éléments de preuve fiables, (ii) les comportements attendus des composants doivent avoir été définis préalablement et (iii) les parties doivent avoir précisé leurs intentions en matière de répartition des responsabilités. Dans cette thèse, nous apportons des éléments de réponse à ces questions en proposant un cadre formel pour spécifier et établir les responsabilités en cas de dysfonctionnement d'un logiciel. Ce cadre formel peut être utilisé par les parties dans la phase de rédaction du contrat et pour concevoir l'architecture de logs du système. Notre première contribution est une méthode permettant d'intégrer les définitions formelles de responsabilité et d'éléments de preuves dans le contrat juridique. Les éléments de preuves sont fournis par une architecture de logs dite "acceptable" qui dépend des types de griefs considérés par les parties. La seconde contribution importante est la définition d'une procédure incrémentale, qui est mise en ?uvre dans l'outil LAPRO, pour l'analyse incrémentale de logs distribués. / Despite the effort made to define methods for the design of high quality software, experience shows that failures of IT systems due to software errors remain very common and one must admit that even critical systems are not immune from that type of errors. One of the reasons for this situation is that software requirements are generally hard to elicit precisely and it is often impossible to predict all the contexts in which software products will actually be used. Considering the interests at stake, it is therefore of prime importance to be able to establish liabilities when damages are caused by software errors. Essential requirements to define these liabilities are (1) the availability of reliable evidence, (2) a clear definition of the expected behaviors of the components of the system and (3) the agreement between the parties with respect to liabilities. In this thesis, we address these problems and propose a formal framework to precisely specify and establish liabilities in a software contract. This framework can be used to assist the parties both in the drafting phase of the contract and in the definition of the architecture to collect evidence. Our first contribution is a method for the integration of a formal definition of digital evidence and liabilities in a legal contract. Digital evidence is based on distributed execution logs produced by "acceptable log architectures". The notion of acceptability relies on a formal threat model based on the set of potential claims. Another main contribution is the definition of an incremental procedure, which is implemented in the LAPRO tool, for the analysis of distributed logs.

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'augmentation de la complexité des systèmes hétérogènes a conduit à l'apparition d'une nouvelle méthode de conception et de validation. Cette approche qui s'appuie sur un flot de conception descendant s'inspire des méthodes utilisées dans le domaine numérique. Dans cette thèse, nous avons développé une approche permettant de qualifier le plan de vérification utilisé lors de la validation de conception et d'améliorer le test matériel des systèmes AMS&RF. L'originalité de notre approche est d'utiliser une description comportementale du système pour la qualification et la génération des stimuli de test. En effet, les méthodes de test actuelles utilisant les descriptions niveau composant ne sont pas adaptées au test de systèmes complexes. En utilisant ce concept, au cours de cette thèse la plateforme PLASMA, PLAteforme pour la qualification et la génération de stimuli pour test de Systèmes Mixtes et Analogiques, a été développée. Cette plateforme est en particulier conçue pour le test des systèmes AMS&RF. PLASMA a été validée sur un émetteur/récepteur W-CDMA intégré conçu par ST Microelectronics.