Travaux de thèse

Préambule

J'effectue ma thèse à l'ENST, au sein du département INFRES. La thèse est dirigée conjointement par l'ENST et le LIP6. Je navigue donc entre ces deux laboratoires pendant toute la durée de la thèse. Je développe le projet pok, découpé en trois parties : un outil de vérification de modèles qui s'occupe de vérifier la sécurité du système, un générateur de code qui créé le code utilisateur et configure les services du noyau pour respecter la politique de sécurité décrite dans le modèle et un noyau conforme aux normes/initiatives des noyaux partitionés (ARINC653, MILS, ...).

Sujet de thèse

Version courte

Intégration de la sécurité et la sûreté de fonctionnement pour la construction d'intergiciels pour systèmes embarqués critiques.

Version longue

Le sujet s'interesse à la sécurité et sûreté d'exécution dans la construction d'intergiciels pour les systèmes critiques. Plus globalement, les systèmes distribués sont de plus en plus durs à configurer et il est très difficile de prouver leur bon fonctionnement. De nombreuses techniques ont été expérimentées, mais prouver le bon fonctionnement d'un programme reste une tâche compliquée. De plus, nous souhaitons ajouter des fonctions de sécurité au sein des intergiciels et des noyaux afin de pouvoir offrir des garanties au concepteur de système. Ces enjeux sont particulièrement importants dans les systèmes critiques, car un bug dans leur conception peut avoir de très lourdes conséquences (perte d'argent, morts, etc ...).

Une première idée consiste à apporter la notion de partitionnement au sein du noyau et à fournir de l'isolation temporelles et spatiale. Ces notions ont déjà été abordée par des standards comme ARINC 653 ou MILS. Une partition représente une unité d'exécution logique où plusieurs flux d'exécution sont présents. Chaque partition est isolée spatialement (une partition n'a aucun accès aux données d'une autre partition) et temporellement (le temps d'exécution d'une partition ne déborde par sur celui d'une autre). On apporte également des garanties de sécurité et de sûreté au sein de l'ensemble noyau, intergiciel et application. Ainsi, à l'inverse de la majorité des systèmes actuels, il est nécessaire de coupler fortement l'intergiciel et le noyau afin que les fonctionnalités de sécurité soient fortement liées entre ces deux parties du systèmes.

A l'issue de ces trois ans de thèse, mes travaux devraient pouvoir déboucher sur la proposition d'éléments suivans :

  • La proposition d'une architecture d'intergiciel et de noyau
  • La définition d'une méthodologie assurant des propriétés de sécurité et de sûreté pour la construction de systèmes critiques

Mon sujet de thèse pour les nuls

Etant donné que nombre de personnes ne comprennent pas tout ce qui est écrit (qu'ils se rassurent : je les comprends ...), voici une description de ma thèse "pour les nuls". C'est à dire vulgarisée, simplifiée, rendue accessible au pekin moyen ayant un minimum de culture informatique (c'est à dire pas grand chose).

L'idée principale est d'intégrer sécurité et sûreté de fonctionnement dans les systèmes embarqués critiques (que l'on retrouve dans des voitures ou des avions par exemple). Cette intégration a principalement deux avantages. Premièrement, le respect de la sûreté de fonctionnement assure que le système fait ce qu'il doit faire, et uniquement ce qu'il doit faire (et croyez moi, ce n'est pas si simple malgré ce que Jean-Kevin, votre neuveu de douze ans vous dit). Par ailleurs, l'intégration d'une politique de sécurité (mais surtout son respect) assure que les échanges de données au sein du système sont toujours légitimes et que le caractère confidentiel des données n'est pas remis en question au cours de la vie du système. Pour intégrer sûreté et sécurité au sein de systèmes critiques, on s'attaque à plusieurs niveaux de la construction de systèmes.

D'abord, il nous faut un système d'exploitation spécifique, adapté aux systèmes embarqués critiques intègrant une politique de sécurité et de sûreté. Une fois qu'on a écrit un tel système, on est très content, mais rien ne nous prouve qu'il est correct. Il faut donc également prouver le système et ses propriétés (ce qui encore, n'est vraiment pas trivial). C'est ce que je fais au travers du projet pok, qui fournit un OS temps-réel dédié à l'embarqué et inclut des services de sécurité et de sûreté.

Une fois le système d'exploitation vérifié, il faut pouvoir aider le développeur dans la construction de son système. L'idée principale est de réduire le code que les développeurs écrivent. Pour deux raisons essentielles. La première, c'est que le code écrit dans des langages traditionnels est très difficilement vérifiable (la sémantique de ces langages est très peu adaptée). La seconde, c'est que les développeurs (même les meilleurs) introduisent de nombreuses erreurs et autres bugs dans leur code. Pour éviter tous les inconvénients de cette méthode de programmartion dite "traditionnelle", nous modélisons les systèmes critiques à l'aide d'un langage adapté, nous vérifions le modèle et nous générons automatiquement le code. Au final, on analyse le système à travers son modèle, on vérifie sa conformité au regard de plusieurs propriétés (la sécurité est-elle respectée ? et la sureté ? le système modélisé est-il conforme aux systèmes critiques ?) et on créé automatiquement le code.

A l'arrivée, on obtient une chaîne complète pour créer des systèmes sécurisés, sûrs et fiables. On réduit l'importance du programmeur, on assure les propriétés de ces systèmes. Le processus de développement est donc plus rapide, plus fiable et aussi indéniablement moins coûteux. Au final, tout le monde est content: le responsable du projet a moins de chances d'avoir des bugs (et donc, de se faire virer pour une erreur bien cachée dans le code source du projet qu'il dirige depuis quelques années), les designers n'ont plus à vérifier eux-mêmes leur système et l'ANPE a plus de développeurs à caser dans les SSII.

Publications

  • [DPK08] J. Delange, L. Pautet, and F. Kordon. Code Generation Strategies for Partitioned Systems. In 29th IEEE Real-Time Systems Symposium (RTSS'08) Work In Progress, IEEE Computer Society, December 2008. PDF
  • [DHPZ08] J. Delange, J. Hugues, L. Pautet, and B. Zalila. Code Generation Strategies from AADL Architectural Descriptions Targeting the High Integrity Domain. In 4th European Congress ERTS, Toulouse, Paris, jan 2008. PDF.

Présentations

  • Code Generation Strategies for Partitioned Systems. In 29th IEEE Real-Time Systems Symposium (RTSS'08) Work In Progress, IEEE Computer Society, December 2008. PDF.
  • Modeling Domains of Safety and Security using AADL. AADL meeting, 2008. PDF
  • Code Generation Strategies from AADL Architectural Descriptions Targeting the High Integrity Domain. In 4th European Congress ERTS, Toulouse, Paris, jan 2008. PDF

Posters

  • Code Generation Strategies for Partitioned Systems. In 29th IEEE Real-Time Systems Symposium (RTSS'08), IEEE Computer Society, December 2008. JPEG.