Method and models for formal verification of remote attestation on microprocessors
Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur
Résumé
In this thesis, we deal with how to secure the execution of an algorithm in a complex environment. We consider that it is impossible to verify that this execution is secure at every instant, even if the adversary accesses the system remotely. Nevertheless, it is possible to detect an intrusion, an alteration of this algorithm, at a specific instant: this allows to establish a dynamic root of trust. To do so, we rely on the remote attestation protocol. To secure the execution of this protocol, a static root of trust must be established, according to the threat model. This static root of trust, when formally verified, has formerly been established for simple embedded devices, such has microcontrollers from the MSP430 family. Obtaining it on these systems requires dedicated hardware support, with enough simplicity so that formal verification remains possible. In order to allow formal verification to scale and to be able to target more complex hardware systems, we propose an automated formal verification approach that is compatible with the industrial requirements. The purpose of this approach is to minimize the abstraction effort and then to reduce the impact of the state-space explosion problem. Then, we take advantage of modern SoC: we leverage the architecture to extend formally verified remote attestation to more complex devices. Our case study aims at establishing a static root of trust for a of-the-shelf microprocessor: the ARM Cortex-A9. To do so, we must provide secure execution for an attesting function and maintain confidentiality for a secret. We propose a definition for the security when targeting this family of systems, taking into account the rise of attack surface and capabilities of an adversary with high privileges. We separate these capabilities into uncorrelated problems, so that we can deal with them independently during formal verification. We propose a design that we implement, and we confront our definition of security to this design and prove that it is verified. The solution we verify does not require any hardware modification: it is simply an extension for the microprocessor, a trusted peripheral, that is implemented in a field-programmable gate array. Although, targeting proprietary architectures comes with an issue: with no access to the source, we cannot formally model their behaviour. Also, according to our strong threat model, we do not consider that the microprocessor represent a secure environment for the execution of the attesting function. As a consequence, we propose to enforce access controls and secure execution from outside the microprocessor: in the trusted peripheral. This mechanism relies on some hypothesis regarding the behaviour of the microprocessor, which we audit so that a reasonable amount of trust can be achieved.
Dans ce manuscrit, nous considérons comme problématique la sécurisation de l'exécution d'un algorithme dans un environnement complexe. Nous partons du principe que nous ne pouvons pas vérifier qu'à tout instant, cette exécution est sécurisée, même dans le cadre d'un adversaire distant. Néanmoins, il est possible de détecter une intrusion, une compromission de cet algorithme, à un instant donné et d'établir une racine de confiance dynamique. Pour cela, il existe le protocole d'attestation à distance. Sécuriser l'exécution du protocole nécessite d'établir une racine de confiance statique, vis-à-vis des capacité d'un adversaire. Cette racine de confiance statique, lorsqu'elle est accompagnée d'une vérification formelle, a jusqu'à présent été établie sur des microcontrôleurs simples, tels que la famille des MSP430. L'obtenir sur ces systèmes nécessite des composants matériels dédiés, suffisamment simples pour que la vérification formelle reste possible. Afin de permettre la vérification formelle de système matériels plus complexes, nous proposons une approche de vérification formelle automatique et industrialisable. L'objectif de cet approche est de minimiser l'effort d'abstraction et ainsi réduire l'impact de l'explosion combinatoire. Ensuite, en nous appuyant sur les architectures des SoC modernes, nous envisageons d'étendre le domaine d'application de l'attestation à distance vérifiée formellement. Notre cas d'étude vise à établir une racine de confiance statique sur un microprocesseur pris sur étagère: le ARM Cortex-A9. Pour cela, nous devons sécuriser l'exécution d'une fonction d'attestation et maintenir la confidentialité d'un secret. Nous proposons une définition de la sécurité sur cette famille de systèmes, en tenant compte de l'augmentation de la surface d'attaque et des capacités d'un adversaire privilégié. Nous décomposons ces capacités en des problématiques décorrélées, que nous pouvons traiter indépendamment pour permettre la vérification formelle. Nous réalisons une implémentation, que nous confrontons à notre définition de la sécurité et apportons la preuve que celle-ci est vérifiée. La solution que nous proposons ne nécessite pas de modification matérielle, mais simplement d'une extension sous forme d'un périphérique de confiance, implémenté dans un circuit de logique programmable. Considérer les architectures propriétaires apporte cependant une problématique: sans accès aux sources, nous ne pouvons pas modéliser formellement leur comportement. Également, vis-à-vis de notre modèle de menace fort, nous ne considérons pas que le microprocesseur constitue un environnement sûr. Nous proposons donc de reconstruire un mécanisme de gestion des privilèges externe à celui-ci, dans la partie matérielle de notre périphérique de confiance. Ce mécanisme s'appuie sur des hypothèses émises vis-à-vis du comportement du microprocesseur, que nous auditons pour pouvoir y accorder un fort degré de confiance.
Origine : Version validée par le jury (STAR)