Master 2013 2014
Stages de la spécialité SAR
Formalisation des propriétés de sécurité d’applications embarquées


Lieu :Oberthur Colombes au sein de l’équipe + 1 journée par semaine au LIP6
Encadrant : Fabien Deboyser – responsable des certifications sécuritaires – encadrant Karine Heydemann et Mathieu Jaume (LIP6)
Dates :5 à 6 mois
Rémunération :1100 euros par mois
Mots-clés : Parcours SAR autre qu’ATIAM, rech./prof., Parcours SAR autre qu’ATIAM, recherche, Parcours SAR, aussi pour STL

Description

Contexte du stage La carte à puce est un élément sécurisé présent au quotidien. Fournissant des fonctionnalités de sécurité cryptographique, il permet en outre de sécuriser le paiement, l’identification, la signature, la téléphonie et bien d’autres domaines. Les nouvelles technologies sont connectées et évolutives. Il est dorénavant possible d’installer des fonctionnalités de sécurité tout au long du cycle de vie du produit. Exemple notable, le développement des smartphones (2 milliards d’unités vendus en 2013) est au centre de toutes ces technologies, grâce notamment à la technologie des plateformes ouvertes et sécurisées. Le sujet du stage s’inscrit dans les besoins de sécurité des nouvelles technologies au regard de la confidentialité et/ou de l’intégrité des données, de l’isolation entre applications, du fonctionnement correct des applications et du système de sécurité. Ces besoins sont exprimés sous la forme de propriétés que les applications et le système de sécurité doivent vérifier. La garantie de ces propriétés est nécessaire pour obtenir la certification d’un produit avant sa mise sur le marché. Il y a plusieurs possibilités pour garantir des propriétés en vue de la certification : la relecture de code, le test ou la preuve reposant sur des méthodes formelles. Les plus hauts niveau de certification ne sont obtenus qu’avec des preuves formelles.

Problématique L’ensemble des propriétés de sécurité d’un produit est exprimé en langage naturel sous la forme d’une exigence fonctionnelle de sécurité ou SFR. Par exemple : !

La politique de sécurité (SFP) associée à l’import des données de signature (SVD) assure que les fonctions de sécurité du produit (TSF) doivent assurer l’import du SVD de manière intègre. Un mécanisme de détection de modifications d’intégrité doit être présent.

Selon les produits, les exigences de sécurité, et donc les propriétés de sécurité, varient. De plus, les produits sont soumis à un ensemble de menaces, également identifiées en langage naturel, pour lesquelles leur comportement est spécifié, une fois encore en langage naturel. La vérification des propriétés ou la garantie des comportements face aux menaces spécifiés en langage naturel pour une application/un système est une tâche difficile. Ceci provient principalement des natures différentes des langages utilisés : le langage naturel pour les exigences de sécurité et un langage de programmation (C ou Java) pour l’implantation du système considéré. Par ailleurs, les systèmes étant complexes car composés d’une ou plusieurs applications contenant plusieurs modules, il faut vérifier que l’ensemble du système respecte bien les propriétés de sécurité ou les comportements spécifiés. La vérification de propriétés globales par composition de propriétés locales ou la garantie du comportement global à partir de comportements locaux n’est pas triviale non plus et est aussi au cœur du sujet de stage. L’objectif du stage est d’étudier les besoins sécuritaires et les menaces tels qu’indiqué dans les normes pour la certification des produits afin de proposer un cadre formel pour leur expression ainsi que pour leur vérification.

Déroulement du stage

Pour le stage, un exemple d’architecture logicielle modulaire sera considéré. Par exemple, l’application composée des 3 modules gestion du PIN, messagerie sécurisée et cryptographie pourra être choisie. Chacun des modules doit vérifier des propriétés de sécurité dites « locales ». Il est aussi nécessaire de vérifier la cohérence des propriétés de sécurité entre les modules et de vérifier la sécurité globale du système (propriété « globale »). Cela nécessite de comprendre comment l’interaction est gérée/comment les modules interagissent. Les modules étant configurés, cela revient à garantir qu’une certaine configuration d’un produit est conforme à la sécurité globale.

Durant le stage, il sera nécessaire d’étudier d’une part les propriétés de sécurité et comportements face aux menaces exprimés en langage naturel et d’autre part l’exemple d’application afin de déterminer la formalisation adéquate au problème. En parallèle, il sera nécessaire de faire un état de l’art des formalismes déjà proposés, notamment concernant les flots d’information. Une importante littérature existe aujourd’hui concernant l’analyse des flots d’information engendrés lors de l’exécution d’un programme dans le but de garantir des propriétés de sécurité. La définition de flots d’information formalise l’idée que les programmes, et les systèmes d’exploitation, manipulent des données qui représentent de l’information et que les opérations faites par ces programmes permettent de transmettre l’information d’un programme à un autre, d’une variable à une autre. Cette formalisation déjà utilisée pour garantir l’intégrité ou la confidentialité des données sera envisagée dans un premier temps pour déterminer si elle convient, modulo extension ou adaptation, à la problématique. Le stage devra donner lieu à une proposition de formalisation, issue ou non des flots d’information, pour la modélisation des propriétés de sécurité/comportements face aux menaces ainsi que leur vérification pour l’exemple choisi.

En fonction de l’avancement, d’autres applications exemples pourront être considérées ou le développement d’un outil d’automatisation pourra être envisagé.

Perspectives du stage

Les systèmes critiques sont soumis à évaluation de conformité à des normes applicables dans le domaine considéré. Ces normes décrivent des exigences qui peuvent porter sur différents aspects d’un système : exigences fonctionnelles, exigences de sécurité, exigences sur l’architecture, etc. Le sujet de stage est un premier par vers l’élaboration d’une méthodologie et d’un cadre formel permettant d’exprimer de telles exigences, afin de pouvoir vérifier la cohérence de ces exigences, ainsi que la conformité d’un développement à ces exigences. Le cadre plus large recherché doit pouvoir rendre compte des différentes entités contraintes par les exigences, des éventuelles informations dont dépendent les exigences, et enfin de la nature des exigences (s’agitil d’exigences sur les états d’un système ? sur les transitions d’un système ?). Ce cadre doit :

- permettre d’identifier précisément, de structurer, et de formaliser un ensemble d’exigences exprimées dans une norme,

- être accompagné de procédures permettant l’analyse statique d’un ensemble de spécifications formelles exprimant des exigences afin de vérifier la cohérence de cet ensemble (les exigences sont-elles compatibles ?) et de détecter d’éventuels problèmes de « sous-spécification », mais aussi afin de vérifier qu’un développement satisfait ces exigences.

Il s’agit donc de faciliter non seulement la conception d’un système critique, mais aussi son développement et son évaluation au regard d’une norme. Ces perspectives pourront faire l’objet d’une thèse en fonction de l’avancement du stage et du candidat retenu.