Traditionnellement, dans le domaine avionique les logiciels utilisés à bord de l’avion sont totalement séparés des logiciels utilisés au dehors afin d’éviter toutes interaction qui pourrait corrompre les systèmes critiques à bord de l’avion. Cependant, les nouvelles générations d’avions exigent plus d’interactions avec le monde ouvert avec pour objectif de proposer des services étendu, générant ainsi un flux d’information potentiellement dangereux. Dans une précédente étude, nous avons proposé l’utilisation de la virtualisation pour assurer la sûreté de fonctionnement d’applications critiques assurant des communications bidirectionnelles entre systèmes critiques et systèmes non sûr. Dans cette thèse nous proposons deux contributions.La première contribution propose une méthode de comparaison d’hyperviseur. Nous avons développé un banc de test permettant de mesurer les performances d’un système virtualisé. Dans cette étude, différentes configurations ont été expérimentées, d’un système sans OS à une architecture complète avec un hyperviseur et un OS s’exécutant dans une machine virtuelle. Plusieurs tests (processeur, mémoire et réseaux) ont été mesurés et collectés sur différents hyperviseurs.La seconde contribution met l’accent sur l’amélioration d’une architecture de sécurité existante. Un mécanisme de comparaison basé sur l’analyse des traces d’exécution est utilisé pour détecter les anomalies entre instances d’application exécutées sur diverse machines virtuelles. Nous proposons de renforcer le mécanisme de comparaison à l’exécution par l’utilisation d’un modèle d’exécution issu d’une analyse statique du bytecode Java.Afin de valider notre approche, nous avons développé un prototype basé sur un cas d’étude identifié avec Airbus qui porte sur l’utilisation d’un ordinateur portable dédié à la maintenance / Traditionally, in avionics, on-board aircraft software used to be totally separated from open-world software in order to avoid any interaction that could corrupt critical on-board systems. However, new aircraft generations require more interaction with off-board systems to provide extended services, which makes these information flows potentially dangerous.In a previous work, we have proposed the use of virtualization to ensure dependability of critical applications despite bidirectional communication between critical on-board systems and untrusted off-board systems. In this thesis, we propose two contributions.The first contribution concerns the establishment of a benchmark of hypervisors. We have developed a test bed to assess the performance impact induced by the use of virtualization. In this work, various configurations have been experimented ranging from a basic machine without an OS up to the complete architecture featuring a hypervisor and an OS running in a virtual machine. Several tests (computation, memory, and network) are carried out, and timing measures are collected on different hypervisors.The second contribution focuses on the improvement of an existing security architecture. A comparison mechanism based on the analysis of execution traces is used to detect discrepancies between replicas supported by diverse virtual machines. We proposeto strengthen the comparison mechanism at runtime by the use of an execution model, derived from a static analysis of the java bytecode

L'objectif de cette thèse est la proposition de nouvelles solutions dans le domaine des systèmes de test et de simulation avioniques et ce, à plusieurs niveaux. Dans un premier temps, nous avons proposé un modèle d'exécution dynamique permettant d'unifier les métiers du test et de la simulation, de répondre aux contraintes imposées, d'apporter de nouvelles possibilités et ainsi d'accélérer le cycle de développement des futurs équipements embarqués. Ensuite, un support matériel basé sur une architecture hétérogène CPU-FPGA a été défini afin de répondre à la problématique proposée et aux contraintes imposées par le domaine d'application telles que le respect du temps-réel et la capacité de reconfiguration dynamique hétérogène. A ce support matériel, est venue s'ajouter une méthodologie de développement permettant une meilleure prise en charge du code "legacy" de l'industriel. Enfin, un environnement unifié temps réel mou pour le test et la simulation avionique a été mis en avant, permettant de diminuer les coûts liés à la maîtrise et à la maintenance d'un nouvel environnement. Finalement, une étude de cas a permis de mettre en avant les capacités de reconfiguration dynamique et les performances de l'environnement développé.

Lors de la conception des avions, il est courant que les constructeurs évaluent la sûreté de fonctionnement en utilisant des modèles stochastiques, mais l'évaluation de la fiabilité opérationnelle à l'aide de modèles en ligne, pendant la réalisation des missions, reste rarement effectuée. Souvent, l'évaluation stochastique concerne la sécurité des avions. Cette thèse porte sur la modélisation de la fiabilité opérationnelle des avions, pour aider à la planification des activités de maintenance et des missions, ainsi qu'à la bonne réalisation de ces dernières. Nous avons développé une approche de modélisation, basée sur un méta-modèle qui sert de base i) de structuration des informations nécessaires à l'évaluation de la fiabilité opérationnelle d'un avion et ii) pour la construction de modèles stochastiques pouvant être mis à jour dynamiquement. La mise à jour concerne l'état courant des systèmes avion, un profil de mission et les moyens de maintenance disponibles dans les diverses escales incluses dans le profil de la mission. L'objectif est de permettre l'évaluation de la fiabilité opérationnelle en ligne. Deux cas d'études, basés sur des sous-systèmes avion, sont considérés à titre d'illustration. Nous présentons des exemples de résultats qui montrent le rôle important de l'évaluation de la fiabilité opérationnelle pendant une mission d'avion.

L'évolution actuelle des systèmes embarqués à bord des systèmes complexes (avions, satellites, navires, automobiles, etc.) les rend de plus en plus vulnérables à des attaques, en raison de : (1) la complexité croissante des applications ; (2) l'ouverture des systèmes vers des réseaux et systèmes qui ne sont pas totalement contrôlés ; (3) l'utilisation de composants sur étagère qui ne sont pas développés selon les méthodes exigées pour les systèmes embarqués critiques ; (4) le partage de ressources informatiques entre applica- tions, qui va de pair avec l'accroissement de puissance des processeurs. Pour faire face aux risques de malveillances ciblant les systèmes embarqués, il est nécessaire d'appli- quer ou d'adapter les méthodes et techniques de sécurité qui ont fait leurs preuves dans d'autres contextes : Méthodes formelles de spécification, développement et vérification ; Mécanismes et outils de sécurité (pare-feux, VPNs, etc.) ; Analyse de vulnérabilités et contre-mesures. C'est sur ce dernier point que portent nos travaux de thèse. En effet, cet aspect de la sécurité a peu fait l'objet de recherche, contrairement aux méthodes formelles. Cependant, il n'existe pas actuellement de modèle formel capable de couvrir à la fois des niveaux d'abstraction suffisamment élevés pour permettre d'exprimer les propriétés de sécurité désirées, et les détails d'implémentation où se situent la plupart des vulnérabilités susceptibles d'être exploitées par des attaquants : fonctions des noyaux d'OS dédiées à la protection des espaces d'adressage, à la gestion des interruptions et au changement de contextes, etc. ; implémentation matérielle des mécanismes de protection et d'autres fonctions ancillaires. C'est sur ces vulnérabilités de bas niveau que se focalise notre étude. Nos contributions sont résumées par la suite. Nous avons proposé une classification des attaques possibles sur un système temps-réel. En nous basant sur cette classification, nous avons effectué une analyse de vulnérabilité sur un système réaliste : une plateforme avionique expérimentale fournie par Airbus. Il s'agit d'un noyau temps-réel critique or- donnancé avec plusieurs autres applications, le tout exécuté sur une plateforme Freescale QorIQ P4080. C'est à travers une application dite " malveillante ", présente parmi l'en- semble des applications, que nous essayons de modifier le comportement des autres appli- cations ou du système global pour détecter des vulnérabilités. Cette méthode d'analyse de vulnérabilités a permis de détecter plusieurs problèmes concernant les accès mémoire, la communication entre applications, la gestion du temps et la gestion des erreurs qui pouvaient conduire à la défaillance du système global. Enfin, nous avons proposé des contre-mesures spécifiques à certaines attaques et des contre-mesures génériques pour le noyau temps-réel qui permet d'empêcher une application d'obtenir des accès privilégiés ou encore de perturber le comportement du système.

Traditionnellement, dans le domaine avionique les logiciels utilisés à bord de l'avion sont totalement séparés des logiciels utilisés au dehors afin d'éviter toutes interaction qui pourrait corrompre les systèmes critiques à bord de l'avion. Cependant, les nouvelles générations d'avions exigent plus d'interactions avec le monde ouvert avec pour objectif de proposer des services étendu, générant ainsi un flux d'information potentiellement dan- gereux. Dans une précédente étude, nous avons proposé l'utilisation de la virtualisation pour assurer la sûreté de fonctionnement d'applications critiques assurant des communi- cations bidirectionnelles entre systèmes critiques et systèmes non sûr. Dans cette thèse nous proposons deux contributions. La première contribution propose une méthode de comparaison d'hyperviseur. Nous avons développé un banc de test permettant de mesurer les performances d'un système virtualisé. Dans cette étude, différentes configurations ont été expérimentées, d'un système sans OS à une architecture complète avec un hyperviseur et un OS s'exécutant dans une machine virtuelle. Plusieurs tests (processeur, mémoire et réseaux) ont été mesurés et collectés sur différents hyperviseurs. La seconde contribution met l'accent sur l'amélioration d'une architecture de sécurité existante. Un mécanisme de comparaison basé sur l'analyse des traces d'exécution est utilisé pour détecter les anomalies entre instances d'application exécutées sur diverse ma- chines virtuelles. Nous proposons de renforcer le mécanisme de comparaison à l'exécution par l'utilisation d'un modèle d'exécution issu d'une analyse statique du bytecode Java. Afin de valider notre approche, nous avons développé un prototype basé sur un cas d'étude identifié avec Airbus qui porte sur l'utilisation d'un ordinateur portable dédié à la maintenance.

Dans cette thèse, nous étudions l’adéquation de l’architecture distribuée des processeurs pluricoeurs avec les besoins des concepteurs de systèmes temps réels avioniques. Nous proposons d’abord une analyse détaillée d’un processeur sur étagère (COTS), le KALRAY MPPA®-256, et nous identifions certaines de ses ressources partagées comme étant les goulots d’étranglement limitant à la fois la performance et la prédictibilité lorsque plusieurs applications s’exécutent. Pour limiter l’impact de ces ressources sur les WCETs, nous définissons formellement un modèle d’exécution isolant temporellement les applications concurrentes. Son implantation est réalisée au sein d’un hyperviseur offrant à chaque application un environnement d’exécution isolé et assurant le respect des comportements attendus en ligne. Sur cette base, nous formalisons la notion de partition comme l’association d’une application avec un budget de ressources matérielles. Dans notre approche, les applications s’exécutant au sein d’une partition sont garanties d’être temporellement isolées des autres applications. Ainsi, étant donné une application et son budget associé, nous proposons d’utiliser la programmation par contraintes pour vérifier automatiquement si les ressources allouées à l’application sont suffisantes pour permettre son exécution de manière satisfaisante. Dans le même temps, dans le cas où un budget est effectivement valide, notre approche fournit un ordonnancement et un placement complet de l’application sur le sous-ensemble des ressources du processeurallouées à sa partition. / In this thesis, we study the suitability of the distributed architecture of many-core processors for the design of highly constrained real-time systems as is the case in avionics. We firstly propose a thorough analysis of an existing COTS processor, namely the KALRAY MPPA®-256, and we identify some of its shared resources to be paths of interference when shared among several applications. We provide an execution model to restrict the access to these resources in order to mitigate their impact on WCETs and to temporally isolate co-running applications. We describe in detail how such an execution model can be implemented with a hypervisor which practically provides the expected property of temporal isolation at run-time. Based on this, we formalize a notion of partition which represents the association of an application with a resource budget. In our approach, an application placed in a partition is guaranteed to be temporally isolated from applications placed in other partitions. Then, assuming that applications and resource budgets are given,we propose to use constraint programming in order to verify automatically whether the amount of resources requested by a budget is sufficient to meet all of the application’s constraints. Simultaneously, when a budget is valid, our approach computes a schedule of the application on the subset of the processor’s resources allocated to it.

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Nous nous intéressons dans cette thèse à la maîtrise de processeurs multi-cœurs COTS dans le but de les rendre utilisables dans des équipements avioniques, qui ont des exigences temps réelles dures. L’objectif est de permettre l'application de méthodes connues d’évaluation de pire temps d’exécution (WCET) sur un ensemble de tâches représentatif d’applications avioniques. Au cours de leur exécution, les tâches exécutées sur différents cœurs vont accéder simultanément à des ressources matérielles qui sont partagées entre les cœurs, en particulier la mémoire principale. Cela pourra entraîner des mises en attente de certains accès que l'on qualifie d'interférences. Ces interférences peuvent avoir un impact élevé sur le temps d'exécution du logiciel embarqué. Sur un processeur COTS, qui est acheté dans le commerce et vise un marché plus large que l'avionque, cet impact n'est pas borné. Nous cherchons à garantir l'absence d'interférences grâce à des moyens logiciels, dans la mesure où les processeurs COTS ne proposent pas de mécanismes adéquats au niveau matériel. Nous cherchons à étendre des concepts de logiciel déterministe de telle sorte à les rendre compatibles avec un objectif de réutilisation de logiciel existant. A cet effet, nous introduisons la notion de logiciel de contrôle, qui est un élément fonctionnellement neutre, répliqué sur tous les cœurs, et qui contrôle les dates des accès des cœurs aux ressources communes de telle sorte à offrir une isolation temporelle entre ces accès. Nous étudions dans cette thèse le problème de faisabilité d'un logiciel de contrôle sur un processeur COTS, et de son efficacité vis à vis d'applications avioniques. / We focus in this thesis on issues related to COTS multi-core processors mastering, especially regarding hard real-time constraints, in order to enable their usage in future avionics equipment. We aim at applying existing Worst Case Execution Time (WCET) evaluation methods on a set of tasks similar to those we can find in avionics software. At runtime, tasks executed among different cores are likely to access hardware resources at the same time, e.g. the main memory. It may lead to additional delays due to hardware contention, called “interferences”. Interferences slow down embedded software within ranges that may be important. Additionnally, no bound has been established for their impact on WCET when using COTS processors, that target larger markets than avionics. We try to provide guarantees that all interferences are eliminated through software, as COTS processors do not provide adequate mechanisms at hardware level. We extend deterministic software concepts that have been developed in the state of the art, in order to make them compliant with the use of legacy software. We introduce the concept of "control software", which is functionnaly neutral, is replicated among all cores, and performs active control of core's accesses to shared resources, so that concurrent accesses are temporally isolated. We formalize and study in this thesis the problem of control software feasibility on COTS processors, and questions of efficiency with regard to legacy avionics software.

L’évolution actuelle des systèmes embarqués à bord des systèmes complexes (avions,satellites, navires, automobiles, etc.) les rend de plus en plus vulnérables à des attaques,en raison de : (1) la complexité croissante des applications ; (2) l’ouverture des systèmes vers des réseaux et systèmes qui ne sont pas totalement contrôlés ; (3) l’utilisation de composants sur étagère qui ne sont pas développés selon les méthodes exigées pour les systèmes embarqués critiques ; (4) le partage de ressources informatiques entre applications, qui va de pair avec l’accroissement de puissance des processeurs. Pour faire face aux risques de malveillances ciblant les systèmes embarqués, il est nécessaire d’appliquer ou d’adapter les méthodes et techniques de sécurité qui ont fait leurs preuves dans d’autres contextes : Méthodes formelles de spécification, développement et vérification ;Mécanismes et outils de sécurité (pare-feux, VPNs, etc.) ; Analyse de vulnérabilités et contre-mesures. C’est sur ce dernier point que portent nos travaux de thèse.En effet, cet aspect de la sécurité a peu fait l’objet de recherche, contrairement aux méthodes formelles. Cependant, il n’existe pas actuellement de modèle formel capable de couvrir à la fois des niveaux d’abstraction suffisamment élevés pour permettre d’exprimer les propriétés de sécurité désirées, et les détails d’implémentation où se situent la plupart des vulnérabilités susceptibles d’être exploitées par des attaquants : fonctions des noyaux d’OS dédiées à la protection des espaces d’adressage, à la gestion des interruptions et au changement de contextes, etc. ; implémentation matérielle des mécanismes de protection et d’autres fonctions ancillaires. C’est sur ces vulnérabilités de bas niveau que se focalise notre étude.Nos contributions sont résumées par la suite. Nous avons proposé une classification des attaques possibles sur un système temps-réel. En nous basant sur cette classification,nous avons effectué une analyse de vulnérabilité sur un système réaliste : une plateforme avionique expérimentale fournie par Airbus. Il s’agit d’un noyau temps-réel critique ordonnancé avec plusieurs autres applications, le tout exécuté sur une plateforme Freescale QorIQ P4080. C’est à travers une application dite « malveillante », présente parmi l’en-semble des applications, que nous essayons de modifier le comportement des autres applications ou du système global pour détecter des vulnérabilités. Cette méthode d’analyse de vulnérabilités a permis de détecter plusieurs problèmes concernant les accès mémoire,la communication entre applications, la gestion du temps et la gestion des erreurs qui pouvaient conduire à la défaillance du système global. Enfin, nous avons proposé des contre-mesures spécifiques à certaines attaques et des contre-mesures génériques pour le noyau temps-réel qui permet d’empêcher une application d’obtenir des accès privilégiés ou encore de perturber le comportement du système. / Security is becoming a major concern for embedded computing systems in variouscritical industrial sectors (aerospace, satellites, automotive, etc.). Indeed, recent trendsin the development and operation of such systems, have made them more and morevulnerable to potential attacks, for the following reasons : 1) increasing complexity of theapplications ; 2) openness to applications and networks that are note completely undercontrol ; 3) Use Commercial-Off-The-Shelf (COTS) hardware and software components ;4) Resource sharing among different applications, driven by the increase of processorscapabilities.To improve the security of such systems, it is necessary to apply or adapt methodsand techniques that have proven their efficiency in other contexts : Formal methods forspecification, development and verification ; Security mechanisms and tools (firewalls,VPNs, etc.) ; Vulnerability assessment and countermeasure provision.The research carried out in this thesis adresses the latter technique. This aspect ofsecurity analysis cannot be easily covered by current formal methods, since no exist-ing model is able to cover both high-level abstractions, where security properties canbe defined, and low-level implementation details, where most vulnerabilities that couldbe exploited by attackers lie : OS kernel implementation of address space protection,interrupt management, context switching, etc. ; hardware implementation of protectionmechanisms and other ancillary functions. Very few research projects are addressing thisaspect of security, which is the main objective of this thesis. In particular, our researchfocuses on low-level vulnerabilities, but contrarily with common practice, we aim todiscover and analyze them during the development process.Our contributions are summarized as follows. We elaborated a classification of low-level vulnerabilities for different implementations of real-time embedded systems. Basedon this classification, we carried out a vulnerability analysis study on a realistic system :An experimental avionic platform provided by Airbus. It consists of a critical real-timekernel scheduling the execution of different applications on a freescale QorIQ P4080platform. The identification and analysis of vulnerabilities is carried out based on a“malicious” application hosted on the platform that attempts to corrupt the behavior ofthe other applications or the global system considering different types of low level attacks.Such experiments allowed us to identify some problems related to the management ofmemory accesses, the communication between applications, time management and errorhandling that could lead to the global system failure.We have also proposed genericcounter measures to protect the real-time kernel against specific attacks, and to preventa given application from escalating its privileges or trying to compromise the systembehavior

Le travail présenté dans cette thèse est une contribution à la commande de la Machine Synchrone à Double Excitation (MSDE) pour des applications embarquées. La MSDE allie les avantages de la machine synchrone à aimants permanents et la machine synchrone à rotor bobiné. Le flux d'excitation dans cette machine est généré par deux sources : les aimants permanents et un enroulement qui est placé au stator afin d'éviter les contacts glissants. Cette dernière source permet de régler le flux dans l'entrefer. Le modèle de la machine est basé sur un modèle de Park et prend en considération les pertes fer et la saturation des circuits magnétiques. Les paramètres du prototype existant au laboratoire ont été identifiés. La commande de la MSDE est effectuée en deux modes : générateur et moteur. En génératrice, l'application visée est la génération électrique en avionique. Deux réseaux de distribution sont traités : Réseau à haute tension et à fréquence variable et réseau haute tension DC. Dans ce dernier cas, la MSDE est associée à un pont redresseur à diodes. Dans les deux cas, la commande est élaborée dans le but de maintenir l'amplitude de la tension constante via le control du courant d'excitation uniquement. Le control est scalaire. L'approche est validée par simulation avec Matlab/Simulink et par expérimentation. Pour le mode moteur, l'application visée est la propulsion dans un véhicule électrique. Une commande optimale des courants est étudiée en vue de minimiser les pertes. Les pertes joules sont considérées premièrement. Ensuite, les pertes fer sont ajoutées. Finalement, le problème de minimisation est étendu pour inclure les pertes dues à l'onduleur et au hacheur. L'optimisation par la méthode des multiplicateurs de Lagrange (Kuhn-Tucker conditions) est utilisée pour trouver des expressions analytiques des courants statoriques et inducteur optimaux. Des simulations avec Matlab/Simulink prouvent que la solution obtenue est celle qui assure les pertes minimales tout au long du nouveau cycle de conduite européen. / This thesis is a contribution to the control of the Hybrid Excitation Synchronous Machine (HESM) in embedded applications. The HESM combines the advantages of the Permanent Magnets (PM) machine and the wound rotor machine. The excitation flux in this machine is produced by two different sources: the PMs and a DC field winding that is placed at the stator to preserve a brushless structure. The latter source is used to control the flux in the air gap. The machine model is based on a Park model and takes into account the iron losses and the magnetic circuit saturation effect. The electric parameters of the laboratory prototype are identified. The machine is controlled in generator mode and motor mode. In power generation system, the study treats in particular the aircraft power supply in more electric aircrafts. Two distribution networks are studied: High voltage variable frequency network and high voltage DC network. In the latter case, the HESM is coupled to a diode bridge rectifier. In both cases, the control aims to maintain the output voltage magnitude equal to its reference via action on the field current only. The control is scalar. Simulation with Matlab/Simulink and experiments validate the approach. For the motor mode, the attention is paid to the electric propulsion in an electric vehicle. An optimal current control with minimal losses is elaborated. The copper losses are considered in a first place. Iron losses are added next. Finally, the optimization problem is extended and it includes the losses due to the inverter and the chopper. Analytical expressions of the reference armature and field currents are computed using extended Lagrange multiplier method (Kuhn-Tucker conditions). Simulation with Matlab/Simulink software proves that the analytical solution yields indeed to the current combination that guarantees the minimal losses over the New European Driving Cycle.