💻 computer science

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL

Cet article présente une preuve mécanisée dans Isabelle/HOL établissant à la fois des garanties de sûreté et de vivacité pour la préservation de l'état réglementaire transdomaine sous des fautes byzantines, en utilisant un cadre réutilisable de sept localités génériques instanciées par rapport à un modèle complet d'exigences de régulation financière mondiale.

Auteurs originaux : Jinwook Kim

Publié 2026-06-01

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Jinwook Kim

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 monde où les actifs numériques (comme les actions ou l'immobilier tokenisés) peuvent circuler librement entre différents « quartiers » (blockchains) et « registres papier » (systèmes hors-chaîne). Le problème est le suivant : si un juge du Quartier A gèle un actif, ce gel doit se produire instantanément et parfaitement dans le Quartier B, le Quartier C et sur le registre papier également. Si ce n'est pas le cas, des acteurs malveillants pourraient pratiquer l'« arbitrage réglementaire », en cachant des actifs dans des endroits où les règles ne sont pas appliquées.

Ce document est une preuve mathématique qu'un système spécifique de transfert de ces actifs est à la fois sûr (il ne fait jamais d'erreurs) et vivant (il ne reste jamais bloqué), même si certains participants tentent de le saboter.

Voici la décomposition utilisant des analogies simples :

1. L'Objectif : La « Course de relais parfaite »

Considérez le système comme une course de relais où le témoin est un « statut réglementaire » (comme « Gelé » ou « Actif »).

Le Défi : Lorsqu'un coureur (une blockchain) change la couleur du témoin, tous les autres coureurs de l'équipe doivent instantanément voir la même couleur.
Le Risque : Si un coureur ment, oublie ou reste bloqué, toute la course pourrait s'arrêter, ou le témoin pourrait prendre deux couleurs différentes en même temps.

2. Les Deux Grandes Victoires (Sécurité et Vivacité)

Les auteurs ont prouvé deux choses concernant leur système :

A. Sécurité : Le « Miroir Incassable »

Ce que cela signifie : Si le système fonctionne, le résultat est toujours cohérent. Si la Chaîne A dit « Geler », la Chaîne B doit dire « Geler ». Il n'y a aucune ambiguïté.
L'Analogie : Imaginez un ensemble de miroirs magiques. Si vous placez une balle rouge devant le Miroir A, le Miroir B, le Miroir C et le registre papier montreront tous une balle rouge. Ils ne montreront jamais une balle bleue, et ils ne seront jamais en désaccord.
La Preuve : Les auteurs ont construit une « carte » (appelée locale) qui prouve que ce miroitement se produit parfaitement, même si les chaînes parlent des langues différentes (vocabulaire technique différent) ou si l'actif circule entre une blockchain et un document papier. Ils ont prouvé que peu importe l'ordre des opérations, l'image finale est toujours la même.

**B. Vivacité : Le « Mécanisme Anti-Blocage »

Ce que cela signifie : Le système ne se fige jamais, même si certains participants sont « Byzantins » (un mot sophistiqué pour désigner des nœuds malveillants ou défaillants qui mentent, retardent les messages ou refusent de lâcher des actifs).
L'Analogie : Imaginez un groupe de personnes essayant de faire passer une boîte lourde à travers un couloir étroit.
- Le Problème : Un acteur malveillant pourrait saisir la boîte et refuser de la lâcher, bloquant ainsi tout le monde.
- La Solution : Le système possède un « délai d'expiration » intégré (comme une trappe à ressort). Si quelqu'un retient la boîte trop longtemps, le système la déloge automatiquement de ses mains et la transmet à la personne suivante.
- La Preuve : Ils ont mathématiquement prouvé que même si jusqu'à 1/3 des personnes essaient de bloquer le couloir, la boîte finira toujours par passer. Aucun actif ne sera jamais verrouillé indéfiniment.

3. Le « Tour de Magie » : Combiner les deux

Habituellement, les preuves de sécurité supposent que tout le monde est honnête. Les preuves de vivacité supposent que certaines personnes sont mauvaises.

L'Astuce du Document : Ils ont combiné les deux. Ils ont montré que le « Mécanisme Anti-Blocage » (Vivacité) est si puissant qu'il corrige l'hypothèse de « Personnes Honnêtes » requise pour le « Miroir Incassable » (Sécurité).
Le Résultat : Vous n'avez pas besoin de faire confiance à qui que ce soit. Même avec des acteurs malveillants, le système est garanti d'être cohérent et en mouvement.

4. La Boîte à Outils : Des « Briques de Lego » pour les Mathématiques

Les auteurs n'ont pas seulement prouvé cela pour une blockchain spécifique. Ils ont construit 7 briques réutilisables (appelées locales dans Isabelle/HOL).

Comment cela fonctionne : Ces briques sont génériques. Vous pouvez les assembler sur n'importe quel système (une banque, une chaîne d'approvisionnement, un jeu) pour obtenir instantanément les mêmes garanties de sécurité et de vivacité.
Tests en conditions réelles : Ils n'ont pas laissé les briques dans la boîte. Ils les ont assemblées sur trois scénarios très différents du monde réel pour prouver leur efficacité :
1. Langages Différents : Une chaîne qui ne parle que « Geler » contre une chaîne qui parle « Geler » et « Décongeler ».
2. Mondes Différents : Une blockchain contre un document juridique complexe hors-chaîne (DAML).
3. Le Moteur de Consensus : Le mécanisme de vote spécifique utilisé pour décider qui passe à l'étape suivante.

5. Ce que ceci N'EST PAS

Pour être clair sur les limites du document :

Il ne vérifie pas si un juge spécifique a réellement le droit légal de geler un actif. Il vérifie seulement que si un gel est ordonné, il se produit correctement partout.
Il ne prouve pas que le code informatique (Rust/Solidity) est exempt de bogues ; il prouve que le modèle mathématique du système est sain.
Il ne gère pas le chaos d'un réseau qui ajoute ou supprime constamment de nouvelles chaînes pendant son fonctionnement (cela relève de travaux futurs).

Résumé

Ce document est un certificat de confiance mathématique. Il dit : « Nous avons construit un système où les règles réglementaires (comme le gel des actifs) sont appliquées parfaitement à travers différents mondes. Même si certains participants tentent de le briser, le système possède un mécanisme d'autocorrection qui garantit que les règles sont suivies et que le système ne reste jamais bloqué. »

Ils ont réalisé cela en écrivant 3 215 lignes de code dans un assistant de preuve (Isabelle/HOL) qu'un ordinateur a vérifié étape par étape pour s'assurer qu'il n'existe aucune faille logique.

Résumé Technique : Sûreté et Vivacité de la Préservation d'État Cross-Domaine sous Fautes Byzantines

1. Énoncé du Problème

Le document traite du défi critique consistant à garantir la cohérence des états de conformité réglementaire pour les actifs tokenisés opérant à travers des réseaux blockchain hétérogènes et des registres hors chaîne (off-chain). Sans garanties formelles, l'arbitrage réglementaire devient structurellement possible ; par exemple, un ordre de gel émis dans une juridiction doit être immédiatement et de manière déterministe reflété dans tous les domaines connectés.

Le problème est décomposé en deux dimensions :

Sûreté (Safety) : Garantir que si une synchronisation est effectuée, l'état résultant est cohérent à travers tous les domaines avec une préservation structurelle.
Vivacité (Liveness) : Garantir que dans un environnement décentralisé contenant des nœuds byzantins (acteurs malveillants), le processus de synchronisation progresse réellement, évitant ainsi les blocages (deadlocks) et l'inanition (starvation).

Les travaux antérieurs n'ont pas vérifié formellement ces deux propriétés simultanément dans un cadre unique, ni vérifié les propriétés de consensus spécifiques à la réglementation (telles que le déterminisme de priorité et l'absence de blocage d'actifs) en utilisant Isabelle/HOL.

2. Méthodologie

Les auteurs emploient une approche de preuve mécanisée utilisant Isabelle/HOL. Le développement se compose de 3 215 lignes de code réparties sur quatre fichiers de théorie, s'exécutant sans sorry ou oops (hypothèses non prouvées).

2.1 Modèles de Système et de Menace

Modèle de Système : Le système comprend un ensemble fini de domaines (chaînes/registres) partageant une structure de machine à états. La synchronisation est modélisée comme une opération atomique impliquant la vérification, la validation, l'acquisition de verrou, la mise à jour de l'état et la libération de verrou.
Modèle de Menace :
- Propriété 1 (Sûreté) : Suppose initialement des nœuds honnêtes et des canaux fiables.
- Propriété 2 (Vivacité) : Relâche l'hypothèse de nœuds honnêtes pour permettre jusqu'à $f < n/3$ nœuds byzantins. Les nœuds byzantins peuvent retenir les libérations de verrous ou agir de manière malveillante.
- Combiné : La Propriété 2 élimine l'hypothèse de "nœud honnête" de la Propriété 1, produisant une garantie inconditionnelle.

2.2 Modèle de Transition d'État Réglementaire

Le modèle formel est basé sur le cadre du Protocole de Conformité Réglementaire (RCP), qui systématise 31 exigences provenant de 15 autorités financières mondiales.

États : Cinq états réglementaires (ACTIF, GELÉ, SAISI, CONFISQUÉ, RESTREINT).
Actions : Sept actions réglementaires (GELER, SAISIR, CONFISQUER, RESTREINDRE, DÉGELER, ANNULER LA RESTRICTION, LIBÉRER).
Contraintes : Le modèle impose des contraintes juridiques spécifiques, telles que l'exclusion des transitions "SAISI $\rightarrow$ GELÉ" (car une saisie est une contrainte juridique plus forte qu'un gel) et la nature terminale de l'état CONFISQUÉ.

2.3 Infrastructure de Vérification : Locales Génériques

La méthodologie centrale repose sur la définition de sept locales génériques, indépendantes du domaine, dans Isabelle/HOL. Ces locales servent d'infrastructure de vérification réutilisable. Les théorèmes prouvés au sein de ces locales sont automatiquement hérités par tout domaine concret qui les instancie via le mécanisme d'interprétation d'Isabelle.

Locales de Sûreté (4) :
1. state_machine : Définit les états finis, les actions et les transitions déterministes.
2. state_preservation : Établit une condition de naturalité où la synchronisation commute avec les transitions d'état (homomorphisme).
3. symmetric_state_preservation : Ajoute des applications inverses pour garantir une préservation bidirectionnelle par aller-retour.
4. multi_domain_preservation : Généralise la cohérence à un ensemble arbitraire de domaines finis (cohérence $N$ -domaines) et assure l'isolation par actif.
Locales de Vivacité (3) :
1. priority_system : Garantit la sélection déterministe des actions via des priorités injectives.
2. deadlock_free_locking : Assure qu'aucune ressource n'est verrouillée indéfiniment via une libération forcée par expiration (timeout).
3. fair_leader_system : Garantit l'absence d'inanition sous réserve d'un ordonnancement de leader honnête périodique.

3. Contributions Clés

3.1 Preuve de Sûreté Mécanisée (Propriété 1)

Le papier étend le motif du foncteur de Merkle (précédemment limité à l'intégrité des données unidirectionnelle dans un domaine unique) à un cadre cross-domaine, bidirectionnel et multi-domaine.

Aller-retour Bidirectionnel : Prouve que les transitions d'état sont fidèlement reflétées dans les deux sens entre les domaines.
Cohérence N-Domaines : Prouve qu'après une synchronisation sur un domaine, tous les domaines connectés atteignent le même état résultant.
Isolation par Actif : Prouve que la synchronisation sur un actif n'affecte pas l'état des autres actifs.
Instanciation Concrète : Les auteurs fournissent des témoins concrets pour s'assurer que les locales ne sont pas satisfaites de manière vacante :
- Instance d'Escalade : Une instance d'actions hétérogènes où une chaîne ne supporte que les actions d'escalade (GELER, SAISIR, etc.) tandis que l'autre supporte l'ensemble complet, prouvant la préservation structurelle à travers des vocabulaires divergents.
- Instance de Traversée de Couche : Un pont bidirectionnel entre un énuméré reg_state on-chain et un enregistrement de permission DAML off-chain, prouvant l'injectivité et l'absence de perte d'information.

3.2 Preuve de Vivacité Mécanisée (Propriété 2)

Il s'agit de la première utilisation d'Isabelle/HOL seul pour vérifier la vivacité du consensus BFT dans un contexte de blockchain.

Déterminisme : Les actions réglementaires conflictuelles sont résolues via un ordre total sur les clés de priorité (niveau d'autorité, horodatage, sévérité, ID de nœud).
Absence de Blocage : Prouve que même si des nœuds byzantins retiennent les libérations de verrous, le mécanisme de timeout garantit que le verrou expire dans un temps borné.
Absence d'Inanition : Prouve que sous une limite de justice (garantissant un leader honnête dans $k$ époques), toutes les requêtes en attente sont finalement traitées.

3.3 Décharge d'Hypothèse (Garantie Combinée)

Le papier démontre un motif de raisonnement assume-guarantee. La Propriété 2 décharge l'hypothèse de "nœud honnête" requise par la Propriété 1. En prouvant que le système reste vivant et déterministe même avec des fautes byzantines ( $f < n/3$ ), la garantie de sûreté conditionnelle est promue à une garantie inconditionnelle : la préservation de l'état cross-domaine tient même en présence de nœuds byzantins.

4. Résultats et Artefacts

Artefacts de Preuve : Le développement inclut huit interprétations concrètes de locales (couvrant les sept locales génériques) aux côtés d'une instanciation multi-domaine paramétrique.
Modèle Réglementaire : Le modèle couvre 31 exigences réglementaires mappées sur 5 états et 7 actions.
Disponibilité : Tous les artefacts sont publiquement disponibles sur GitHub et ont été soumis à l'Archive of Formal Proofs (AFP) pour examen.
Guide de Conception : Les preuves produisent des contraintes de paramètres spécifiques pour l'implémentation (ex: $n \ge 3f + 1$ , timeouts positifs, limites de justice) qui se traduisent directement en un raisonnement mathématique de conception pour les séquenceurs décentralisés.

5. Signification et Revendications

Le papier revendique une importance dans trois domaines principaux :

Nouveauté dans la Vérification Formelle : C'est le premier travail à vérifier formellement simultanément la sûreté et la vivacité pour les transitions d'état réglementaire cross-domaine. C'est également le premier à vérifier des propriétés de consensus spécifiques à la réglementation (déterminisme de priorité, absence de blocage d'actifs réglementaires) dans un outil.
Avancement Méthodologique : En utilisant une hiérarchie de locales génériques, les auteurs fournissent une infrastructure de vérification réutilisable qui est indépendante du domaine. Cela permet d'appliquer les mêmes preuves de sûreté et de vivacité à des domaines arbitraires (ex: DeFi, bases de données distribuées) simplement en instanciant les locales.
Pont entre Théorie et Pratique : Ce travail va au-delà de la vérification abstraite du consensus (comme l'accord/validité) pour traiter des contraintes réglementaires spécifiques au domaine. Il fait explicitement le pont entre une machine à états théorique et un modèle de conformité réglementaire, fournissant un "guide de conception" pour les paramètres d'implémentation dérivés directement des preuves.

Les auteurs notent explicitement les limitations : le modèle ne vérifie pas les caractéristiques spécifiques aux chaînes (gas, temps de bloc), ne prouve pas de raffinement formel vers le code Rust/Solidity, et suppose un système fermé (l'arrivée dynamique de requêtes est un travail futur). Le cadre actuel établit les locales et instances fondamentales mais n'a pas encore formalisé les lois de foncteur de la théorie des catégories (identité et composition), qui sont réservées à des travaux futurs pour atteindre le statut complet de "foncteur".