Master 2018 2019
Stages de la spécialité SAR
Analyse fonctionnelle du Secure Monitor de OP-TEE


Site : ALSOC
Lieu : Laboratoire de Paris 6 (LIP6)
Encadrant : Cécile Braunstein et Emmanuelle Encrenaz
Dates :du 01/02/2019 au 01/08/2019
Rémunération :Indemnités de stage fixées par décret (environ 600 euros/mois)
Mots-clés : Master SAR, autre qu’ATIAM

Description

Description ========

Aujourd’hui, les exigences des utilisateurs en matière de sécurité sont devenues incontournables. En outre, les systèmes sont de plus en plus complexes, ouverts et connectés. Pouvoir garantir la sécurité des systèmes et des données manipulées, souvent sensibles, est un enjeu majeur du développement des systèmes embarqués et autres objets connectés (IOT). Dans ce contexte, les environnements d’exécution de confiance (TEE :Trusted Execution Environment) ont été conçus pour tirer partie des architectures sûres tel l’architecture TrustZone de ARM. Ces plates-formes sécurisées permettent la coexistence de systèmes offrant différents niveaux de sécurité sur la même architecture. Par exemple sur un smartphone, le TEE peut être utilisé pour sécuriser les services de paiements comme la gestion de portefeuille électronique ou manipuler des données sensibles comme lors de l’authentification biométrique. OP- TEE ([6]) est un projet open source qui propose une implémentation complète d’un environnement d’exécution de confiance. Le TEE doit donc être capable de garantir l’authenticité du code qui s’exécute en mode sécurisé, l’intégrité de l’état d’exécution (état des registres, de la mémoire . . . ) et la confidentialité du code, des données qu’il manipule (cf. [8]). OP-TEE distingue deux mondes, l’un non sécurisé, utilisé pour les applications courantes et un autre sécurisé, dans lequel s’exécutent les services ayant recours à des données sensibles. On se propose dans ce stage d’étudier la présence ou l’absence propagation de donnée du monde sécurisé au monde non sécurisé. Un des éléments clé d’un TEE est le Secure Monitor. C’est le programme qui est appelé à chaque commutation entre le monde non-sécurisé et sécurisé au travers d’appels systèmes spécifiques induit par l’appel de services déployés dans des applications sécurisées. A la suite du stage de Maxime Ayrault nous avons un modèle du secure monitor de OP-TEE [7]. Notre étude vise l’enrichissement de ce modèle (notamment par le mécanisme d’interruption) et la vérification fonctionnelle du modèle. Les méthodes formelles offrent la possibilité de vérifier de façon automatique (ou partiellement automatique) des propriétés sur le code analysé (pour des systèmes de tailles moyennes). Ces méthodes sont généralement utilisées pour vérifier le bon fonctionnement de portions de programmes applicatifs ou de code système. Plus récemment, des approches émergent pour se concentrer sur les propriétés de sécurité des systèmes [3]. Dans le cadre de ce stage, nous sommes intéressés d’une part par la vérification fonctionnelle du modèle de OP-TEE à partir de la spécification des TEE [4, 5]. Cette spécification est développée par Global Platform qui regroupe un ensemble d’industriels, travaillant sur la standardisation des interfaces logiciels des TEE. D’autre part, nous souhaiterions vérifier des propriétés de sécurité, pour garantir la confidentialité de l’information : nous voulons montrer qu’une information ne peut pas être connue par des tiers non autorisés : une donnée du monde sécurisé ne peut être connue du monde non-sécurisé. Le model checker CPAchecker ([1]) est un outil de vérification qui implémente un grand nombre d’algorithmes de model checking [2]. Un objectif du stage sera aussi d’évaluer les différentes stratégie de vérification et de trouver la ou les plus adaptées à notre modèle.

Objectif du stage ===========

L’objectif du stage est la modélisation et la vérification d’une partie d’un TEE. Dans un premier temps, un modèle de Secure Monitor et de son environnement opérationnel devront être enrichis. Ensuite, en partant de la spécification du TEE, des propriétés fonctionnelles seront vérifiées sur le modèle au moyen du model-checker CPAChecker. Les algorithmes de model checking seront alors comparés. Enfin, la spécification pourra être complétée par l’ajout de propriétés de sécurité et des stratégies pour les vérifier. Déroulement du stage envisagé • Etude bibliographique sur OP-TEE et la spécification TEE • Analyse du code du secure monitor de Maxime Ayrault • Proposition d’ajout de comportements dans le modèle • Proposition de propriétés fonctionnelles • Etude des algorithmes de model checking implémentés dans CPAchecker • Analyse des performances du model checking • Réflexion sur la modélisation des propriétés de sécurité

Pre-requis : ========

Connaissance de la programmation assembleur, programmation C/C++/Java, structure des systèmes d’exploitation, algorithmes de model checking

Bibliographie

[1] Dirk Beyer and M. Erkan Keremoglu. CPAchecker : A Tool for Configurable Software Verification. In Com- puter Aided Verification, Lecture Notes in Computer Science, pages 184–190. Springer, Berlin, Heidelberg, July 2011.

[2] Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer International Publishing, Cham, 2018.

[3] Onur Demir, Wenjie Xiong, Faisal Zaghloul, and Jakub Szefer. Survey of approaches for security verification of hardware/software systems. IACR Cryptology ePrint Archive, 2016:846, 2016.

[4] GlobalPlatform Device Technology. TEE Internal Core API Specification. Technical Report 1.1.2, Glob- alPlatform Inc, 2016.

[5] GlobalPlatform Device Technology. TEE Architecture specification. Technical Report 1.1, GlobalPlatform Inc, 2017.

[6] Linaro. optee_os : Trusted side of the TEE, December 2017. original-date : 2014-05-26T17:18:57Z.

[7] Maxime Ayrault. Analyse et modélisation du Secure Monitor de OP-TEE. Stage de recherche fin de Master,Sorbonne Université, 2018.

[8] Mohamed Sabt, Mohammed Achemlal, and Abdelmadjid Bouabdallah. Trusted Execution Environment : What It is, and What It is Not. In 14th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, Helsinki, Finland, August 2015.