Analyse fonctionnelle du Secure Monitor de OP-TEE

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 (\emph{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 ([14]) 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 \ldots{}) et la confidentialité du code, des données qu'il manipule (cf. [20]). 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 \emph{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 \emph{secure monitor} de OP-TEE [15]. 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 [7]. 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 [10,11]. 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 CPA\textsc{checker} ([3]) est un outil de vérification qui implémente un grand nombre d'algorithmes de model checking [6]. 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.

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 enrichit. Ensuite, en partant de la spécification du TEE, des propriétés fonctionnelles seront vérifiées sur le modèle. 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.

• Etude bibliographique sur OP-TEE et la spécification TEE
• Analyse du code du \emph{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 cheking implémenté dans CPA\textsc{checker}
• Analyse des performances du model checking
• Réflexion sur la modélisation des propriétés de sécurité

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

Cécile Braunstein et Emmanuelle Encrenaz