Analyse du Secure Monitor de OP-TEE

Description

OP-TEE ([10]) est un projet open source qui propose une implémentation complète d'un environnement d'exécution sûre (TEE : Trusted Execution Environment), basé sur les 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.

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. [12]). 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 sécurisé et non-sécurisé (lors d'appels systèmes, de retour d'appels, et pour le traitement de certaines interruptions). Notre étude se concentrera sur ce secure monitor, nous tenterons de montrer, à l'aide de méthodes formelles, que l'implémentation du secure monitor ne permet pas la fuite d'information sensible du monde sécurisé vers le monde non sécurisé.

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 [4]. Dans le cadre de ce stage, nous sommes intéressés par des propriétés de confidentialité de l'information, c'est à dire que nous voulons montrer qu'une information ne peut pas être connu par des tiers non autorisés : une donnée du monde sécurisé ne peut être connue du monde non-sécurisé.

Ce type d'analyse peut se faire en capturant les dépendances de données des calculs réalisés lors de l'exécution de l'application au travers des différentes couches logicielles et mondes de OP-TEE. Cette analyse de dépendences peut être réalisée à partir d'une analyse de teintes (taint analysis), et d'un calcul d'accessibilité ([1]). Dans ce stage nous allons mettre en place l'analyse du flot d'information d'un secure monitor par analyse de teinte à l'aide d'un model checker.

Objectif du stage

L'objectif du stage est la vérification de confidentialité du Secure Monitor de OP-TEE par analyse de teinte et calcul d'accessibilité. Dans un premier temps, un modèle opérationnel de l'environnement OP-TEE sera décrit, se focalisant sur le secure monitor et les éléments architecturaux essentiels pour représenter la commutation de monde. L'analyse de teinte sera d'abord implantée de manière ad hoc par ajout d'instructions directement dans le modèle du secure monitor et le calcul d'accessibilité se fera à l'aide du model checker CPA\textsc{checker} ([2]). La deuxième phase du stage se concentrera sur l'automatisation de notre méthode et l'intégration de l'analyse de teinte dans CPA\textsc{checker}.

Déroulement du stage envisagé

Etude bibliographique sur les Secure Element, OP-TEE, analyse de teinte.
Analyse du code du \emph{secure monitor} de OP-TEE
Proposition d'un modèle opérationnel du \emph{secure monitor} et analyse des instructions à risque
Enrichissement du modèle avec suivi de teintes
Prise en main de CPA\textsc{checker} côté utilisateur
Vérification de propriétés de confidentialité du secure monitor
Prise en main de CPA\textsc{checker} côté développeur
Automatisation de l'analyse de teinte.

Pre-requis :

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

Encadrement

Cécile Braunstein et Emmanuelle Encrenaz

Lieu

Laboratoire Informatique de Paris 6

Contact

cecile.braunstein@lip6.fr / emmanuelle.encrenaz@lip6.fr

Rémunération

Indemnités de stage fixées par décret (environ 600 euros/mois)

References

[1]	G. Bai, Q. Ye, Y. Wu, H. Merwe, J. Sun, Y. Liu, J. S. Dong, and W. Visser. Towards Model Checking Android Applications. IEEE Transactions on Software Engineering, PP(99):1--1, 2017. [DOI ]
[2]	Dirk Beyer and M. Erkan Keremoglu. Cpachecker: A tool for configurable software verification. In CAV. LNCS, volume 6806, pages 184--190. Springer, 2011. [http ]
[4]	Onur Demir, Wenjie Xiong, Faisal Zaghloul, and Jakub Szefer. Survey of approaches for security verification of hardware/software systems. Cryptology ePrint Archive, 2016. [pdf ]
[10]	Linaro. optee_os: Trusted side of the TEE, December 2017. original-date: 2014-05-26T17:18:57Z. [http ]
[12]	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. [DOI \| http ]