Ce projet de recherche doctorale est publié a été réalisé par LAURENT PAUTET

Description d'un projet de recherche doctoral

Intégration de politiques de sécurité et de sûreté de fonctionnement pour la modèlisation, la vérification et la génération de systèmes critiques

Mots clés :

Résumé du projet de recherche (Langue 1)

1 Introduction Le travail de thèse a lieu dans l’équipe S3 (System, Software and Services), au sein du département « Informatique et Réseaux» de Telecom ParisTech. S3 se compose actuellement de 8 enseignants-chercheurs permanents (dont 3 habilités à diriger des recherches), 12 doctorants. L’équipe S3 s’intéresse à la modélisation, la conception et la vérification des systèmes répartis et en particulier des systèmes Temps Réel Répartis Embarqués (TR2E). Notre objectif est de développer des techniques de modélisation, des outils de vérification, des platesformes d’exécution et des générateurs de code permettant à des ingénieurs de développer sans risque des systèmes TR2E. En particulier, S3 a acquis une expertise reconnue internationalement dans l’architecture d’intergiciels hautement configurables en fonction des propriétés requises par le système. Ces cinq dernières années, S3 a également développé une forte compétence dans la modélisation et la génération automatique des systèmes TR2E par le biais d’ADL et notamment d’AADL. 2 Contexte L’usage des systèmes Temps Réel Répartis Embarqués (TR2E) s’est aujourd’hui généralisé, tant auprès du grand public (téléphonie mobile, PDA, ...) qu’au sein de systèmes complexes (issus du domaine aérospatial, automobile, énergétique). Le recours à ces systèmes dans de nombreuses activités critiques (aéronautique, spatial, transport, médical, bancaire) ajoute une contrainte forte en termes de sûreté de fonctionnement : une erreur peut avoir un impact économique, industriel voire humain important. Il est donc crucial d’intégrer la sécurité et la sûreté de fonctionnement au processus de construction de l’application afin d’évaluer et limiter tout risque d’erreurs. Ceci passe autant par l’application d’éléments formels et théoriques (étude stochastique) que techniques de conception (DO-178B, IMA, OMG DDS, MILS). En parallèle, la complexité croissante du logiciel a conduit à la définition de couches d’abstraction et de méthodes de conception. Ainsi l’industrie s’oriente vers des environnements de modélisation et des infrastructures logicielles d’exécution à base de composants logiciels permettant d’améliorer le processus de développement par le biais d’une rationalisation de la gestion de projet (réutilisation, intégration, maintenance évolutive), d’une séparation entre les préoccupations fonctionnelles et celles purement techniques (adaptation aux couches sous-jacentes, communication, auto-observation, intégrité ...), et d’un outillage permettant de valider ou analyser le couple application/environnement d’exécution (évaluation des taux de pannes, de l’ordonnancement, etc.). Les environnements de modélisation et de conception ainsi que les intergiciels qui les accompagnent doivent donc intégrer des préoccupations de vérification formelle des composants comme leur isolation en fonction de leur niveau de sécurité ou de criticité. 3 Positionnement du travail Le logiciel et son environnement d’exécution doivent fournir des éléments permettant de valider finement son bon fonctionnement, dans des contextes où la certification (avionique) ou la validation (spatial) sont cruciaux pour autoriser l’utilisation du système. Se posent alors de multiples questions lors de la construction du couple logiciel/environnement d’exécution : quelles sont les propriétés à tester ? Quelles sont les techniques de validation associées ? Quelles sont les processus et les outils à mettre en oeuvre pour guider l’ingénieur dans ces choix de conception et lors de la réalisation ? La variété des besoins impose la définition d’un processus intégré reposant sur des standards, combinés et intégrés et sa mise en oeuvre. La sécurité et la sûreté de fonctionnement imposent la définition de politiques, leur validation (e.g. théorème de Bell-Lapadula) et leur mise en oeuvre dans le cadre de standards (OMG DDS, RT-CORBA, ARINC 653, etc). La prise en compte simultanée de ces deux aspects pose pour le moment de nombreux problèmes théoriques visant à terme la suppression des méthodes ad hoc employées aujourd’hui et son remplacement par un processus fiable autorisant séparation des préoccupations, analyse guidée, configuration de l’environnement d’exécution. 4 Problématique de la thèse L’hétérogénéité des besoins tant théoriques que pratiques amène de nouveaux problèmes pour l’ingénierie logicielle, qui doit pouvoir s’adapter à une large variété de théories (model checking classique, stochastique, temporisé, preuves) et technologies (intergiciels, noyaux temps réel), sans pour autant en maîtriser tous les aspects. Il devient alors nécessaire d’abstraire l’architecture du système pour permettre son analyse, et la définition de ces environnements. Une architecture comme celle proposée dans les specifications de MILS permet d’effectuer des vérifications mathématiques (sur l’ordonnancement par exemple) en réduisant et isolant de manière significative les portions de code critiques. La description de l’architecture vise à traiter de plusieurs problèmes difficiles. Tout d’abord, de pouvoir vérifier que certaines contraintes de sécurité et de sûreté de fonctionnement peuvent être vérifiées hors ligne. La problématique est d’autant plus grande que ces deux aspects peuvent s’entre-mêler voire se composer par une approche hierarchique. Or jusqu’à présent ces deux aspects ne sont modèlisés ni de manière commune ni selon une approche composite. Par ailleurs, s’il existe de nombreuses démarches de générations de code, peu visent à produire un code déterministe. Cependant, on conçoit bien que pour assurer des propriétés de sécurité et de sûreté, il faut garantir une certaine confiance dans le code généré. Au regard des efforts déployés dans le cadre de SCADE, il convient d’adopter des solutions pragmatiques pour assurer une confiance suffisamment forte. Enfin, toutes les contraintes de sécurité et de sûreté ne peuvent être vérifiées hors ligne et certaines devront se faire en ligne. Le code généré devra donc se charger de ces vérifications à l’exécution avec les problèmes de dualité et de hierarchie des aspects sécurité et sûreté déjà exposé. Il conviendra également de produire du code déterministe vers un intergiciel adapté. De nombreux problèmes méthodologiques se posent : des problèmes tant d’ingénierie logicielle, que d’implantation et validation ; et leur traitement nécessite des outils dédiés afin d’aider l’ingénieur dans sa phase de conception pour à la fois valider et déployer l’application sur l’environnement configuré. 5 Sujet L’objectif de cette thèse vise à faire des propositions autour de l’intégration des politiques de sécurité et de sûreté de fonctionnement dans le cadre de la modélisation, de la vérification et de la génération de systèmes critiques. L’approche proposée pour atteindre ces objectifs consistera à : – Élaborer une typologie des standards existants ou en cours de définition pour la sûreté de fonctionnement et la sécurité ; des éléments théoriques les supportant et les outils associés. On s’interessera en particulier aux initiatives MILS, IMA et aux standards D0-178B/C et OMG DDS ; on s’intéressera également dans la validation des générateurs de code ; – Définir des formalismes pour la prise en compte simultanée des propriétés de sécurité et de sûreté de fonctionnement. Au travers d’un langage comme AADL, cela pourra s’effectuer au travers d’annexes qu’il conviendra de rendre compatible pour assurer l’utilisation simultanée de ces aspects. – Produire automatiquement les composants logiciels de telle manière que l’on assure une certaine confiance dans la partie générée. Dans un premier temps, cela pourra s’effectuer par génération d’annotations qui seront par la suite analysées. Le code généré s’appuyera sur des intergiciels dédiés intégrant des fonctionnalités de sécurité et de sûreté de fonctionnement. – Vérifier la cohérence des modèles exprimées en fonction des formalismes précédemment définis ainsi que la conformité du code généré. Il faut noter que, dans le cas de hierarchie de partitions intégrant simultanément des aspects de sécurité et de sûreté de fonctionnement, la coérence peut s’avérer complexe à réaliftware, ETAPS 2003. Proceedings, number 2619 in Lecture notes in computer science, pages 379–393, Warsaw, Poland, April 7-1 2003. Springer Verlag. [3] Edmund M. Clarke, Somesh Jha, and Wilfredo R. Marrero. Partial order reductions for security protocol verification. In Tools and Algorithms for Construction and Analysis of Systems, pages 503–518, 2000. [4] J-M. Couvreur and Y. Thierry-Mieg. Hierarchical decision diagrams to exploit model structure. In Proc. of the 25th IFIP WG 6.1 Int. Conf. on Formal Techniques for Networked and Distributed Systems (FORTE’05), volume 3731 of LNCS, Taipei, Taiwan, October 2005. Springer. [5] Orna Grumberg, Tamir Heyman, and Assaf Schuster. A work-efficient distributed algorithm for reachability analysis. In CAV, pages 54–66, 2003. [6] Elsa L. Gunter and Doron Peled. Model checking, testing and verification working together. Formal Asp. Comput., 17(2) :201–221, 2005. [7] Rahul Kumar and Eric G. Mercer. Load balancing parallel explicit state model checking. Electr. Notes Theor. Comput. Sci., 128(3) :19–34, 2005. [8] Karen Laster and Orna Grumberg. Modular model checking of software. Lecture Notes in Computer Science, 1384 :20– ? ?, 1998. [9] W. Marrero, E. Clarke, and S. Jha. Model checking for security protocols, 1997. [10] Yann Thierry-Mieg. Techniques pour le Model-Checking de spécifications de Haut Niveau. thèse de doctorat, Université Paris VI, Laboratoire LIP6, France, Décembre 2004. [11] Yann Thierry-Mieg, Soheib Barrir, Alexandre Duret-Lutz, and Fabrice Kordon. Nouvelles techniques de Model Checking pour la vérification de systèmes complexes. Génie Logiciel, 69 :17–23, 2004.

Résumé du projet de recherche (Langue 2)

L’hétérogénéité des besoins tant théoriques que pratiques amène de nouveaux problèmes pour l’ingénierie
logicielle, qui doit pouvoir s’adapter à une large variété de théories (model checking classique, stochastique,
temporisé, preuves) et technologies (intergiciels, noyaux temps réel), sans pour autant en maîtriser
tous les aspects.

Il devient alors nécessaire d’abstraire l’architecture du système pour permettre son analyse, et la définition
de ces environnements. Une architecture comme celle proposée dans les specifications de MILS
permet d’effectuer des vérifications mathématiques (sur l’ordonnancement par exemple) en réduisant et isolant
de manière significative les portions de code critiques. La description de l’architecture vise à traiter de
plusieurs problèmes difficiles.

Tout d’abord, de pouvoir vérifier que certaines contraintes de sécurité et de sûreté de fonctionnement
peuvent être vérifiées hors ligne. La problématique est d’autant plus grande que ces deux aspects peuvent
s’entre-mêler voire se composer par une approche hierarchique. Or jusqu’à présent ces deux aspects ne sont
modèlisés ni de manière commune ni selon une approche composite.

Par ailleurs, s’il existe de nombreuses démarches de générations de code, peu visent à produire un
code déterministe. Cependant, on conçoit bien que pour assurer des propriétés de sécurité et de sûreté, il
faut garantir une certaine confiance dans le code généré. Au regard des efforts déployés dans le cadre de
SCADE, il convient d’adopter des solutions pragmatiques pour assurer une confiance suffisamment forte.

Enfin, toutes les contraintes de sécurité et de sûreté ne peuvent être vérifiées hors ligne et certaines
devront se faire en ligne. Le code généré devra donc se charger de ces vérifications à l’exécution avec les
problèmes de dualité et de hierarchie des aspects sécurité et sûreté déjà exposé. Il conviendra également de
produire du code déterministe vers un intergiciel adapté.

De nombreux problèmes méthodologiques se posent : des problèmes tant d’ingénierie logicielle, que
d’implantation et validation ; et leur traitement nécessite des outils dédiés afin d’aider l’ingénieur dans sa
phase de conception pour à la fois valider et déployer l’application sur l’environnement configuré.