💻 computer science

Formal Verification of Secure Encrypted Virtualization

Cet article présente un cadre formel qui abstrait et vérifie les garanties de sécurité d'AMD Secure Encrypted Virtualization (SEV) afin d'assurer rigoureusement la confidentialité, l'intégrité et la disponibilité des environnements d'exécution de confiance.

Auteurs originaux : Hansika Weerasena, Amitabh Das, Prabhat Mishra

Publié 2026-06-02

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Hansika Weerasena, Amitabh Das, Prabhat Mishra

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez un gratte-ciel massif et bouillonnant (le Cloud) où des centaines d'entreprises différentes (les Locataires) louent des étages de bureaux. Dans un bâtiment normal, le gestionnaire du bâtiment (l'Hyperviseur) possède une clé maîtresse qui peut ouvrir n'importe quelle porte, jeter un coup d'œil dans n'importe quel coffre et lire n'importe quel document sur n'importe quel bureau. Si le gestionnaire est honnête, tout le monde est tranquille. Mais que se passe-t-il si le gestionnaire est un espion ou s'il est piraté ? Soudain, les secrets de chaque entreprise sont en péril.

Pour résoudre ce problème, les entreprises ont commencé à construire des Salles Sécurisées à l'intérieur du bâtiment. On les appelle des Environnements d'Exécution de Confiance (TEE). Plus précisément, cet article se concentre sur une version de haute technologie de ces salles appelée AMD SEV (Secure Encrypted Virtualization).

Voici ce que les chercheurs ont fait, expliqué simplement :

1. Le Problème : « Faites-moi confiance » ne suffit pas

La technologie AMD SEV est comme un bureau ultra-sécurisé dont les murs sont faits de verre invisible et incassable. Même le gestionnaire du bâtiment (l'Hyperviseur) ne peut ni voir l'intérieur, ni toucher à quoi que ce soit. Le matériel informatique lui-même chiffre les données afin que, si quelqu'un tente de voler le disque dur, il n'obtienne qu'un tas de données brouillées et incompréhensibles.

Cependant, les personnes qui ont construit ces pièces ont écrit un manuel (la spécification) expliquant comment elles fonctionnent. Mais un manuel n'est que des mots sur une page. Cela ne prouve pas que la pièce est réellement sécurisée. Il pourrait y avoir une minuscule fissure dans le verre, ou une porte secrète que les architectes ont oublié de mentionner. Dans le monde de la sécurité, « nous pensons que c'est sûr » ne suffit pas ; il faut une preuve mathématique.

2. La Solution : Le « Plan Mathématique »

Les auteurs de cet article ont décidé d'arrêter de deviner pour commencer à prouver. Ils ont construit un cadre de vérification formelle.

Voyez cela comme un architecte qui ne se contente pas de dessiner un plan du bâtiment, mais crée une simulation mathématique parfaite de celui-ci. Ils effectuent ensuite un « test de résistance numérique » sur cette simulation pour voir si elle casse sous n'importe quelle attaque possible.

Ils ont procédé de deux manières principales :

Abstraction de la Conception : Ils ont traduit le manuel technique complexe et désordonné d'AMD SEV en un modèle mathématique propre et simplifié. C'est comme transformer un livre d'instructions de 500 pages en un schéma clair.
Vérification de Propriétés : Ils ont écrit une liste de « règles » (propriétés) que la pièce doit respecter pour être considérée comme sûre. Ensuite, ils ont utilisé un programme informatique (appelé Rosette) pour vérifier si le modèle mathématique enfreint parfois ces règles.

### 3. Les Trois Règles du Jeu (CIA)

Les chercheurs ont vérifié la sécurité des salles AMD SEV par rapport à trois objectifs principaux, connus sous le nom de CIA (Confidentialité, Intégrité, Disponibilité) :

Confidentialité (Le « Gardien des Secrets ») :
- La Règle : Personne, pas même le gestionnaire du bâtiment, ne doit pouvoir lire ce qui se passe à l'intérieur de la pièce.
- Le Test : Ils ont simulé un espion tentant de regarder à l'intérieur. Ils ont vérifié si l'espion pouvait un jour voir la « mémoire privée » ou les « registres du CPU » (le cerveau de l'ordinateur) de l'invité.
- Le Résultat : Ils ont vérifié 14 règles différentes. Les mathématiques ont prouvé que tant que le matériel AMD fonctionne comme prévu, l'espion ne peut pas voir les secrets.
Intégrité (Le « Sceau Anti-Altération ») :
- La Règle : Personne ne doit pouvoir modifier discrètement les documents à l'intérieur de la pièce ou les remplacer par des faux.
- Le Test : Ils ont simulé un saboteur essayant de réécrire le code de l'invité ou de tromper le système en lui faisant croire qu'une ancienne version vulnérable du logiciel est la version actuelle.
- Le Résultat : Ils ont vérifié 7 règles. Les mathématiques ont montré que le système possède une « table de correspondance inversée » (comme un journal de sécurité strict) qui empêche quiconque de remplacer des pages ou de revenir en arrière dans le temps vers un état non sécurisé.
Disponibilité (L' « Interrupteur ») :
- La Règle : La pièce doit fonctionner quand vous en avez besoin, et le gestionnaire du bâtiment doit pouvoir l'éteindre s'il le doit.
- Le Test : Ils ont vérifié deux choses :
  1. Le gestionnaire peut-il toujours reprendre le contrôle ? Oui. Les mathématiques ont prouvé que le gestionnaire peut toujours mettre l'invité en pause ou l'arrêter.
  2. L'invité peut-il toujours fonctionner sans être privé de temps ? Non. Les mathématiques ont prouvé que si le gestionnaire est malveillant, il peut choisir de ne jamais laisser l'invité s'exécuter. Le système garantit que le gestionnaire peut vous arrêter, mais il ne garantit pas que le gestionnaire vous laissera fonctionner. C'est une limitation connue de la technologie.

4. Les « Mises à Niveau » qu'ils ont testées

L'article n'a pas seulement examiné la version de base d'AMD SEV. Ils ont également testé deux mises à niveau plus récentes et plus robustes :

SEV-ES : Ajoute une couche de protection pour le « cerveau » de l'ordinateur (les registres du CPU). Auparavant, le gestionnaire pouvait voir ce que l'ordinateur pensait lorsqu'il faisait une pause. Désormais, même les pensées sont chiffrées.
SEV-SNP : Ajoute un système de « notaire » pour les pages de mémoire. Cela garantit qu'une page de mémoire appartient à la bonne personne et n'a pas été remplacée ou altérée.

5. Le Verdict

Les chercheurs ont réussi à construire un jumeau numérique du système AMD SEV et l'ont soumis à un parcours du combattant de 23 tests de sécurité différents.

Confidentialité : A réussi tous les tests.
Intégrité : A réussi tous les tests.
Disponibilité : A réussi le test pour le contrôle du gestionnaire, mais a correctement identifié que l'invité ne peut pas forcer le gestionnaire à le laisser fonctionner (ce qui est une caractéristique de conception, pas un bug).

En Résumé

Cet article est comme une équipe d'ingénieurs forensiques qui ont pris un coffre-fort de haute technologie, ont construit un modèle mathématique parfait de celui-ci, et ont prouvé au monde entier que, selon les lois des mathématiques, le coffre-fort ne peut pas être ouvert par le gestionnaire du bâtiment. Ils n'ont pas seulement dit : « Il semble sûr ». Ils ont dit : « Nous avons calculé toutes les façons possibles de le briser, et nous avons prouvé qu'il ne peut pas l'être ».

Cela donne aux utilisateurs du cloud un niveau de confiance bien plus élevé quant à la sécurité de leurs données, même si le propre logiciel du fournisseur de cloud est piraté.

Résumé Technique : Vérification Formelle de la Virtualisation Sécurisée Chiffrée

Énoncé du Problème

Les environnements de cloud computing modernes hébergent des locataires mutuellement non approuvés sur une infrastructure physique partagée, ce qui crée des risques importants d'attaques entre locataires et d'attaques basées sur l'hyperviseur. Bien que les environnements d'exécution de confiance (TEE), en particulier les TEE basés sur des machines virtuelles (VM) comme l'AMD Secure Encrypted Virtualization (SEV), offrent une isolation assistée par le matériel pour protéger la confidentialité et l'intégrité du code et des données, leur documentation architecturale manque souvent de garanties de sécurité formelles. La complexité de ces conceptions et le potentiel de failles d'implémentation subtiles nécessitent une vérification formelle rigoureuse pour garantir que les VM clientes restent confidentielles et non modifiées tout au long de leur cycle de vie, même en présence d'un hyperviseur malveillant ou d'un logiciel système compromis. Les efforts de vérification existants pour d'autres TEE (par exemple, Intel SGX, ARM TrustZone) ne sont pas directement applicables aux TEE basés sur des VM en raison de différences architecturales fondamentales dans les modèles de confiance, les mécanismes d'application et les interactions système.

Méthodologie

Les auteurs proposent un cadre de vérification formelle qui utilise l'abstraction au niveau de la conception et de la propriété pour modéliser et vérifier les VM confidentielles d'AMD SEV. La méthodologie procède comme suit :

Stratégie d'Abstraction :
- Abstraction basée sur la conception : Capture tous les comportements définis par l'architecture et les transitions d'état de la spécification SEV pour former un modèle opérationnel de base.
- Abstraction basée sur la propriété : Simplifie le système en se concentrant uniquement sur les composants et les comportements pertinents pour des propriétés de sécurité spécifiques (Confidentialité, Intégrité, Disponibilité).
Modélisation Formelle :
- L'architecture AMD SEV (incluant SEV-base, SEV-ES et SEV-SNP) est modélisée à l'aide du langage Rosette, un langage de programmation assisté par solveur.
- Le modèle incorpore des variables symboliques, des assertions et des fonctions assistées par solveur pour représenter des structures de données d'état (ex: Table de Contexte de l'Invité, Table ASID, Table de Carte Inverse) et des fonctions d'interface binaire d'application (ABI) (ex: LAUNCH_START, ACTIVATE, DECOMMISSION).
- Le modèle de menace suppose un adversaire privilégié (hyperviseur) capable de suspendre, de terminer et de manipuler les états du système, mais contraint par des mécanismes d'isolation imposés par le matériel.
Définition et Vérification des Propriétés :
- Le cadre définit des modèles formels pour la Confidentialité (empêcher l'observation non autorisée de la mémoire/des registres), l'Intégrité (empêcher la modification ou le rejeu non autorisé de données/d'état) et la Disponibilité (assurer la vivacité tant pour l'hôte que pour l'invité).
- La vérification est effectuée à l'aide du moteur d'exécution symbolique de Rosette couplé au solveur SMT Z3. Le système explore les chemins d'exécution pour valider les contraintes et rechercher des contre-exemples.

Principales Contributions

Le document apporte les contributions spécifiques suivantes :

Modèle Formel Complet : Un modèle formel définissant les frontières de sécurité des VM confidentielles, considérant explicitement des adversaires ayant accès à des vecteurs d'attaque avancés.
Définitions CIA Formelles : Modélisation formelle des notions de Confidentialité, d'Intégrité et de Disponibilité (CIA) spécifiquement adaptées aux TEE basés sur des VM.
Implémentation AMD SEV : Un modèle formel détaillé de l'architecture AMD SEV (couvrant SEV-base, SEV-ES et SEV-SNP) développé en Rosette, incluant les structures de données d'état et les transitions de cycle de vie.
Analyse Comparative : Une évaluation critique des mesures de sécurité d'AMD SEV par rapport à d'autres TEE basés sur des VM comme Intel TDX, mettant en évidence les divergences architecturales dans la racine de confiance, l'attestation et la gestion des clés.
Résultats de Vérification Formelle : Vérification formelle réussie d'AMD SEV par rapport à 23 propriétés de sécurité dérivées des notions de sécurité CIA.

Résultats Expérimentaux

Les auteurs ont implémenté le modèle et vérifié 23 propriétés sur un environnement CPU Apple M2 (16 Go de RAM) :

Confidentialité : 14 propriétés ( $CP_1$ – $CP_{14}$ ) ont été vérifiées. Elles couvrent l'application du chiffrement de la mémoire, l'isolation ASID, le chiffrement de l'état des registres (SEV-ES) et la validation des pages (SEV-SNP). Toutes les propriétés ont réussi.
Intégrité : 7 propriétés ( $IP_1$ – $IP_7$ ) ont été vérifiées. Elles assurent les transitions d'état de cycle de vie valides, l'atomicité, la prévention des attaques par rollback et la gestion correcte des secrets lors de la migration. Toutes les propriétés ont réussi.
Disponibilité : 2 propriétés ( $AP_1$ $A P_{1}$ – $AP_2$ $A P_{2}$ ) ont été modélisées.
- $AP_1$ (Vivacité côté hôte) : Vérifiée. Le modèle confirme que l'hyperviseur peut toujours reprendre le contrôle.
- $AP_2$ (Vivacité côté invité) : Non Vérifiée. Le modèle confirme que la vivacité côté invité (garantir la progression face à un hyperviseur malveillant) ne peut pas être garantie dans les technologies SEV actuelles, car l'hyperviseur conserve le contrôle de l'ordonnancement.

Métriques de Vérification :

Temps de vérification des propriétés de confidentialité : ~20,52 secondes.
Temps de vérification des propriétés d'intégrité : ~12,45 secondes.
Temps de vérification des propriétés de disponibilité : ~3,67 secondes.

Signification et Revendications

Le document affirme fournir une base rigoureuse pour définir et vérifier les attributs de sécurité clés pour la protection des environnements d'exécution. En établissant des définitions formelles de la CIA dans le contexte des TEE basés sur des VM et en vérifiant avec succès l'architecture AMD SEV, ce travail démontre que les méthodes formelles peuvent être efficacement appliquées à des systèmes complexes conçus conjointement par le matériel et le logiciel.

Les auteurs affirment que leur approche offre l'assurance la plus forte que l'architecture impose correctement les garanties d'isolation et de protection, comblant ainsi une lacune critique là où les méthodes basées sur la simulation échouent à couvrir les cas limites. Le travail souligne que si AMD SEV fournit de solides garanties de confidentialité et d'intégrité (vérifiées par le modèle), il manque intrinsèquement de garanties de disponibilité côté invité face à un hyperviseur malveillant. Le document conclut que ce cadre formel ouvre la voie à de futures recherches pour sécuriser les environnements TEE virtualisés et offre une solution évolable pour valider la posture de sécurité des services cloud.