Prouver la sécurité des protocoles de consensus basés sur des DAG

Les protocoles de consensus basés sur les DAG sont utilisés par les entreprises de blockchain pour réduire la consommation d'énergie et améliorer la Sécurité. Ces protocoles fonctionnent ensemble pour créer un ordre partiel des blocs de transactions, menant à une séquence claire de blocs. Vu l'importance des blockchains, il est nécessaire de prouver que les composants essentiels, en particulier les protocoles de consensus, fonctionnent comme prévu.

Cet article se concentre sur une méthode formelle pour prouver la validité de deux protocoles basés sur des DAG. Les spécifications révèlent plusieurs méthodes pour diffuser, construire le DAG et ordonner, qui peuvent être mélangées pour exprimer les deux protocoles. L'approche formelle doit être affinée pour modéliser le consensus de manière précise. Dans un premier temps, la sécurité du consensus basé sur un DAG est démontrée sur des blocs de leader, puis affinée pour inclure tous les blocs et processus.

Les spécifications pour chaque protocole se composent de plusieurs lignes, tandis que le système de preuve vérifie de nombreuses obligations en quelques minutes seulement.

#Importance de la Vérification Formelle

Les cryptomonnaies et la finance décentralisée (DeFi) offrent une nouvelle façon de gérer les services bancaires et financiers, transformant l'accès et la gestion de ces services. Les blockchains servent de fondation pour les cryptomonnaies, et les protocoles de consensus sont cruciaux pour garantir l'accord entre les processus concernant l'état de la blockchain.

Les anciens protocoles de consensus étaient basés sur des environnements synchrones pour garantir sécurité et activité. Récemment, un groupe de protocoles de consensus probabilistes asynchrones utilisant des Graphes Acycliques Dirigés (DAG) a émergé. Ces protocoles montrent une haute performance avec une tolérance aux fautes byzantines (BFT), sont équitables envers les processus et maintiennent une faible complexité de communication. Plusieurs blockchains de premier plan s'appuient maintenant sur des protocoles basés sur des DAG pour le consensus.

Comme de grandes quantités d'argent sont détenues dans différentes blockchains, manipuler le protocole de consensus peut devenir une cible d'attaques. Par exemple, les attaques de double dépense visent à exploiter des protocoles non sécurisés en trouvant des entrées qui mènent à des états inconsistants, permettant de dépenser la même monnaie deux fois.

Bien que les protocoles de consensus soient conçus pour être sûrs et réduire de telles attaques, la conception logicielle informelle rend difficile la preuve de la sécurité pour toutes les entrées. Les blockchains établies, malgré leur réputation, ne sont pas toujours sûres.

Une façon stricte d'assurer la sécurité est d'utiliser la vérification formelle. Cette méthode implique de créer des modèles mathématiques qui décrivent le comportement du système et de fournir une preuve mathématique que le protocole de consensus fonctionne correctement pour toutes les entrées et configurations. Bien que certains protocoles aient de telles preuves, beaucoup reposent sur des hypothèses de sécurité sans soutien formel. Cela est dû à la nature fastidieuse de la création de modèles formels, ainsi qu'à un manque de blocs de construction faciles à utiliser pour prouver la validité des nouveaux protocoles.

Bien que réutiliser des spécifications soit souvent faisable, le processus de preuve nécessite généralement de repartir de zéro. Cependant, sauter la modélisation et les preuves de sécurité n'est pas conseillé car le nombre d'interactions possibles dans des environnements asynchrones est écrasant. Se fier uniquement aux tests peut ne pas exposer les défauts dans la conception du protocole, car les comportements nuisibles des processus byzantins peuvent ne pas être entièrement capturés par les cas de test. En général, les tests et la vérification de modèle traditionnelle ne garantissent pas la validité des processus impliqués et de leurs configurations.

Cet article présente une étude de cas réelle où des modèles vérifiés de protocoles de consensus guident le développement. Dans notre étude de cas, nous vérifions formellement la sécurité de deux protocoles basés sur des DAG : DAG-Rider et Cordial Miners. Même si ces protocoles fonctionnent sur des principes similaires, les différences introduites pour améliorer la performance peuvent affecter la validité. Donc, le défi réside dans la création de spécifications et de preuves qui sont modulaires et adaptables pour les protocoles existants et nouveaux.

Pour y parvenir, nous créons des spécifications modulaires qui capturent les aspects communs des protocoles tout en permettant la réutilisation des preuves. Ce processus implique de choisir des abstractions appropriées pour les protocoles, ce qui nous permet de décomposer les propriétés et les preuves en composants plus petits. Notre travail est une étape cruciale vers la production d'un ensemble de spécifications et de preuves qui peuvent être facilement réutilisées, ne nécessitant que des ajustements mineurs pour différents protocoles basés sur des DAG.

Nous avons rendu public une spécification formelle et une preuve open-source pour DAG-Rider et Cordial Miners. La spécification est écrite en Temporal Logic of Actions (TLA+), et les preuves sont effectuées à l'aide du système de preuve TLA+ (TLAPS), qui vérifie l'exactitude des preuves efficacement.

#Aperçu des Protocoles de Consensus Basés sur des DAG

Les protocoles de consensus basés sur des DAG s'attaquent au problème de la diffusion atomique byzantine (BAB), qui consiste à ordonner des blocs de messages (transactions) dans un contexte où certains processus peuvent agir de manière malveillante. Ces protocoles supposent un réseau de processus où un certain nombre peut se comporter de manière incorrecte.

Les processus peuvent créer, signer et envoyer des messages les uns aux autres. On suppose que chaque message envoyé d'un processus correct à un autre sera finalement reçu, et chaque processus peut produire séquentiellement des messages.

L'objectif principal d'un protocole de consensus basé sur un DAG est de garantir que les résultats respectent deux propriétés clés : la sécurité et l'activité. La sécurité signifie que les séquences de résultats de deux processus corrects doivent être cohérentes, impliquant que l'une est un préfixe de l'autre. L'activité exige que chaque message envoyé par un processus correct finisse par être produit par tous les processus corrects avec un haut degré de certitude.

En termes généraux, il est crucial de formuler le problème du consensus, surtout pour les lecteurs familiers avec le consensus traditionnel mais pas avec les concepts de blockchain. Le problème du consensus vise à établir un accord commun entre les processus concernant les transactions actuelles et leur ordre.

Les protocoles de consensus basés sur des DAG sont conçus pour gérer les processus byzantins jusqu'à une certaine limite. Ils fonctionnent sous l'hypothèse que certains processus exécutent le protocole de consensus tandis qu'un nombre défini peut être byzantin.

Les propriétés nécessaires pour les protocoles de consensus basés sur des DAG incluent :

1. Sécurité: Les séquences de résultats des transactions de tous les processus corrects doivent être cohérentes.
2. Activité: Chaque transaction envoyée par un processus correct sera finalement produite par tous les processus corrects.

Pour clarifier, la cohérence en matière de sécurité repose sur l'idée de préfixe pour les séquences de transactions. Étant donné un ensemble de séquences, l'une est un préfixe de l'autre si elle représente le début de cette séquence. Les résultats sont considérés cohérents lorsque l'un est un préfixe de l'autre.

La construction des protocoles basés sur des DAG se fait en deux étapes : une phase de communication et une phase d'ordonnancement.

#Phase de Communication

Au cours de cette phase, les processus créent et partagent des sommets au sein de rounds spécifiques. Un sommet comprend l'ID du créateur, un numéro de round, des références à des sommets des rounds précédents et le bloc proposé. Chaque processus construit son DAG local, qui détient ses sommets créés et ceux reçus des autres.

Les arêtes sortantes dans le DAG local connectent les sommets à ceux auxquels ils font référence. Un sommet est ajouté à un DAG local une fois ses références présentes ; sinon, il reste dans un buffer.

Un processus est dit avoir terminé un round lorsque son DAG local détient un nombre spécifique de sommets de ce round. Un processus ne peut créer et partager un sommet dans le round suivant qu'après avoir terminé le round actuel.

Chaque DAG local organise naturellement les sommets en couches ; les sommets du round zéro forment la couche inférieure, et ceux des rounds supérieurs pointent vers des inférieurs. Donc, chaque DAG local décrit un ordre partiel sur ses sommets. Il est important de noter que les DAG locaux entre différents processus n'ont pas à être égaux ou à suivre la même structure. Cependant, le protocole garantit que si un sommet apparaît dans plus d'un DAG local, son histoire causale est la même dans les deux.

#Phase d'Ordonnancement

Dans la phase d'ordonnancement, chaque processus doit ordonner totalement les sommets de son DAG local de manière indépendante et sans communication supplémentaire. Le défi réside dans l'obtention d'un ordonnancement identique parmi tous les processus corrects.

Si les processus peuvent s'accorder sur certains sommets "d'ancrage", ils peuvent organiser les sommets non triés restants en fonction d'une procédure de tri topologique prédéfinie. Le premier ancrage est noté, suivi d'autres ancrages. La différence dans l'histoire causale entre ces ancrages peut alors être ordonnée en utilisant le tri convenu.

Puisque le protocole est asynchrone et déterministe, les ancrages doivent être choisis au hasard. Chaque processus divise son DAG local en plusieurs vagues, permettant la sélection d'un sommet leader aléatoire pour chaque vague à l'aide d'une pièce parfaite globale, souvent mise en œuvre avec des signatures de seuil.

Le consensus sur la séquence des leaders de vague engagés (ancrages) est essentiel pour obtenir un ordre cohérent des sommets dans les DAG. Les blocs représentés par les sommets ordonnés peuvent être sortis séquentiellement pour assurer la sécurité.

#Spécifications et Preuves Réutilisables

L'architecture des spécifications et des preuves intègre la création d'abstractions pour les rendre modulaires et réutilisables. Le principal défi est de savoir comment représenter l'état du réseau, car les processus peuvent avoir reçu différents ensembles de messages menant à des DAG locaux uniques.

L'abstraction de l'état du réseau stocke un DAG local pour chaque processus. Chaque DAG local est stocké sous forme de tableau à deux dimensions, représentant des sommets créés par différents processus lors de différents rounds. Certaines positions peuvent être vides, indiquant qu'un processus n'a pas reçu de communication d'autres lors de ce round.

L'objectif est de convenir d'un sommet représentant chaque position dans le DAG local. Cette tâche implique de gérer à la fois des stratégies de communication fiables et non fiables.

Dans le cas de diffusions fiables, il ne peut y avoir qu'un sommet à une position donnée dans le DAG local. Pour les diffusions non fiables, il peut y avoir plusieurs sommets à une seule position. Cela nécessite des techniques pour sélectionner un sommet représentant unique pour chaque position.

En abstrahant la sélection de sommets comme un processus en deux étapes, la spécification des protocoles de consensus peut être divisée en sections accompagnantes. La spécification de communication inclut des éléments de la phase de communication, tandis que la spécification d'ordonnancement se concentre sur l'accord sur les positions des leaders de vague engagés.

Pour maintenir une représentation uniforme de la spécification d'ordonnancement, nous simplifions les représentations de DAG locaux pour nous concentrer uniquement sur les positions des leaders de vague. Chaque vague a une position de leader unique, ce qui entraîne la création d'un vague-DAG, où les sommets ne reflètent que les sommets leaders.

Les arêtes dans ce vague-DAG montrent des relations basées sur le protocole de communication actuel, soit la fermeture transitive des arêtes fortes pour DAG-Rider, soit la relation de ratification pour Cordial Miners.

#Preuves de Sécurité

La sécurité des spécifications est soutenue par plusieurs théorèmes et invariants. Chaque spécification a son propre ensemble d'invariants qui doivent être établis puis prouvés dans le cadre du système.

Pour maintenir la sécurité des phases d'ordonnancement et de communication, des invariants spécifiques comme LeaderConsistency et LeaderMonotonicity doivent être validés. LeaderConsistency garantit que les séquences de leaders engagés de deux processus corrects s'alignent de manière cohérente, tandis que LeaderMonotonicity exige que les engagements de vagues suivent un ordre spécifique et constant.

Chaque invariant est prouvé indépendamment, et les dépendances entre eux sont structurées de manière systématique. Le processus de preuve utilise diverses stratégies, y compris l'induction, ce qui permet de garantir que les invariants tiennent dans tous les états accessibles pendant la phase d'ordonnancement.

#Conclusion

L'effort global pour spécifier et prouver plusieurs protocoles de consensus basés sur des DAG a pris beaucoup de temps, mais une fois modularisé, le temps nécessaire pour spécifier et prouver le protocole de Cordial Miners a considérablement diminué. Cela signifie que de nombreux autres protocoles pourraient probablement être modélisés et prouvés avec un effort similaire réduit.

La précision introduite par des spécifications et des preuves vérifiables par machine exige une approche plus rigoureuse, garantissant que l'implémentation correspond étroitement au modèle utilisé pour la vérification formelle. Nous sommes en train d'étendre ces spécifications et preuves pour soutenir des protocoles basés sur des DAG améliorés, en nous appuyant sur les enseignements tirés des phases de spécification et de preuve.

Les avantages de ce processus de vérification formelle sont clairs : non seulement ils aident à garantir la sécurité, mais ils contribuent également à des implémentations plus robustes et fiables des protocoles de consensus à travers diverses applications de blockchain.