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
Publications
- [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.