Résumé technique : Exécution Multi-Version Divergente (DME)

Énoncé du problème

Les mécanismes de redondance traditionnels, tels que l'exécution en pas-à-pas et la Redondance Modulaire Triple (TMR), reposent sur l'exécution de binaires identiques avec des agencements mémoire identiques. Bien qu'efficaces contre les pannes indépendantes, ces systèmes sont vulnérables aux pannes corrélées. Des études expérimentales (par exemple, Dutertre et al.) ont démontré que des perturbations physiques, telles que l'injection de fautes par champ électromagnétique, peuvent induire des perturbations identiques (par exemple, un $\Delta PC$ spécifique) sur toutes les répliques simultanément. Dans les systèmes conventionnels, de telles perturbations corrélées redirigent toutes les répliques vers le même chemin d'exécution incorrect, entraînant une corruption silencieuse des données qui reste indétectée car toutes les répliques produisent des états erronés identiques. De plus, la redondance conventionnelle échoue souvent à détecter des classes spécifiques de bogues logiciels (par exemple, des pointeurs non initialisés, des écrasements d'adresses de retour) ou des défauts de compilation/lien qui se manifestent de manière identique sur toutes les répliques.

Méthodologie

L'article propose l'Exécution Multi-Version Divergente (DME), un vérificateur de cohérence sémantique temps réel conçu pour détecter les pannes corrélées en garantissant que des perturbations numériques identiques entraînent des chemins d'exécution sémantiquement divergents.

Principes fondamentaux

La DME fonctionne selon quatre principes fondamentaux appliqués lors de la compilation :

1. Compilation indépendante : $N$ répliques sont compilées indépendamment à partir du même code source. Cela produit des agencements physiques de code et de données distincts tout en préservant des sémantiques au niveau des opcodes identiques et des graphes de flot de contrôle isomorphes.
2. Décorrélation à grain grossier : Les fonctions et les blocs de base sont placés à des adresses différentes entre les répliques en utilisant des motifs de déplacement de branches complémentaires (par exemple, des branches avant dans une réplique deviennent des branches arrière dans une autre). Cela garantit que des perturbations de flot de contrôle identiques mappent vers des chemins sémantiquement différents.
3. Décorrélation à grain fin : Des instructions NOP périodiques sont insérées à des décalages spécifiques à la réplique ($offset_r = \frac{l}{N} \cdot r$). Cela crée une séparation spatiale minimale entre les instructions logiques correspondantes, permettant la détection de perturbations du Compteur de Programme (PC) de faible amplitude.
4. Décorrélation des adresses de données : Les variables globales, les trames de pile et les allocations de tas se voient attribuer des adresses de base absolues uniques pour chaque réplique.

Mécanismes de détection de pannes

La DME emploie une stratégie de détection à double couche :

1. Couche sémantique (Trace d'instructions canonique) :

   • Le système compare les « traces canoniques » entre les répliques. Une trace canonique inclut les opcodes, les identifiants de registres, les opérandes immédiats, les valeurs chargées/stockées et les résultats calculés.
   • Crucialement, les adresses absolues sont exclues de la trace.
   • En l'absence de faute, toutes les répliques produisent des traces canoniques identiques. Toute faute altérant la sémantique d'exécution (par exemple, l'exécution d'une instruction différente ou le calcul d'un résultat différent) provoque une divergence de trace.

2. Couche structurelle (Décorrélation de l'espace d'adressage et non-aliasing) :

   • La DME traite l'égalité des adresses physiques (par exemple, $PC_1 = PC_2 = \dots = PC_N$) entre les répliques comme une violation de l'indépendance structurelle, plutôt que comme un état acceptable.
   • Invariant de non-aliasing d'adresse : Le système impose que les accès mémoire sémantiquement correspondants (données ou instructions) doivent cibler des adresses effectives différentes entre les répliques.
   • Si une faute (par exemple, un débordement de tampon ou une déréférenciation de pointeur nul) amène toutes les répliques à calculer la même adresse erronée, le système déclenche immédiatement une erreur. Cela permet de détecter les corruptions de pointeurs et les écrasements d'adresses de retour avant qu'une divergence sémantique ne se produise.

Modèles de pannes et régimes de détection

L'article catégorise les garanties de détection en fonction de la nature de la perturbation :

• Détection déterministe :

  • S'applique aux pannes entièrement corrélées où $\Delta PC$ est identique sur toutes les répliques.
  • Si $|\Delta PC| \geq l/N$ (où $l$ est l'espacement d'insertion des NOP), la perturbation garantit qu'au moins une réplique exécutera une instruction logique différente, entraînant une divergence de trace immédiate.
  • L'effondrement de l'espace d'adressage (PC ou pointeurs identiques) est détecté immédiatement comme une violation structurelle.

• Détection probabiliste :

  • S'applique aux pannes partiellement corrélées (où $\Delta PC$ diffère entre les répliques) ou aux pannes où $|\Delta PC| < l/N$.
  • La détection repose sur la faible probabilité que les répliques s'alignent accidentellement sur la même instruction logique et produisent des résultats identiques.
  • La probabilité de rester indétecté pendant $k$ étapes est bornée par $(\frac{C}{|S|} \cdot \epsilon)^k$, où $C$ est le nombre d'instructions canoniquement équivalentes, $|S|$ est l'espace total d'instructions, et $\epsilon$ est la probabilité de résultats identiques. Pour des architectures d'instructions (ISA) 32 bits typiques, cette probabilité décroît exponentiellement (par exemple, $\epsilon \leq 2^{-52}$).

Contributions clés

1. Décorrélation structurelle de l'espace d'adressage : L'article introduit une méthode pour transformer des perturbations de bas niveau corrélées en une divergence sémantique observable en diversifiant activement les agencements mémoire et les déplacements de branches lors de la compilation.
2. Surveillance de trace canonique : Il définit une représentation de trace indépendante de l'agencement qui capture l'exécution sémantique (opcodes, registres, résultats) tout en éliminant les informations dépendantes de l'adresse, permettant une comparaison robuste entre des binaires divers.
3. Détection à double couche : La DME combine la comparaison de traces sémantiques avec la surveillance structurelle des adresses. Cela permet la détection immédiate d'événements d'« effondrement d'adresse » (par exemple, des adresses de retour identiques) que la redondance traditionnelle pourrait manquer si le chemin d'exécution résultant se trouvait être identique.
4. Modèle de correction formelle : L'article distingue entre la correction sémantique temps réel (égalité des traces) et la correction au niveau système (égalité sémantique + indépendance structurelle). Il prouve formellement que l'indépendance structurelle est une condition suffisante pour garantir l'observabilité des pannes corrélées.

Résultats et affirmations

L'article affirme que la DME fournit :

• Une détection déterministe pour les pannes de PC corrélées où l'amplitude de la perturbation dépasse l'espacement de décorrélation ($|\Delta PC| \geq l/N$).
• Une détection probabiliste avec une décroissance exponentielle pour les autres types de pannes, bornée par l'espace d'état de l'architecture d'instructions.
• Une détection immédiate des violations de sémantique de pointeur (par exemple, pointeurs nuls, erreurs de valeur-comme-pointeur) via l'Invariance de non-aliasing d'adresse, souvent avant la divergence sémantique.
• Une faisabilité pratique : Les auteurs citent une implémentation prototype sur un processeur logiciel 32 bits (3o|||sheet) fonctionnant sur un FPGA Altera Cyclone IV, et une implémentation de Machine Virtuelle sur un cœur Cortex-M, démontrant que la surcharge est gérable (par exemple, 3000 LUT et 16 Ko de BRAM par réplique).

Importance

L'article positionne la DME comme une redéfinition de la redondance pour les systèmes embarqués critiques pour la sécurité. Contrairement aux Environnements d'Exécution Multi-Variants (MVEE), qui utilisent principalement la diversification pour entraver la portabilité des exploits, la DME utilise la décorrélation structurelle comme une invariance formelle de correction temps réel pour détecter les corruptions au niveau des bits causées par des perturbations physiques.

Les auteurs soulignent que la DME comble une lacune spécifique dans la tolérance aux pannes existante : l'incapacité de la redondance conventionnelle à détecter les perturbations corrélées au niveau des instructions qui préservent l'égalité d'état mais violent la sémantique du programme. En imposant une indépendance structurelle, la DME garantit que des pannes numériques identiques ne peuvent pas aboutir à des comportements logiques identiques, transformant ainsi les risques de corruption silencieuse des données en événements détectables. Ce travail est présenté comme un mécanisme indépendant du matériel, analysable formellement, adapté aux environnements où l'injection de fautes électromagnétiques ou environnementales constitue une menace réaliste.