Les systèmes distribués basés sur le consensus permettent à un ensemble d’acteurs non localisés de parvenir à différents types d’accords sans dépendre d’une autorité centrale. Les algorithmes de consensus les plus sophistiqués sont dits «tolérants aux fautes byzantines» (BFT), c’est-à-dire qu’ils garantissent l’atteinte d’un consensus en dépit de la présence d’un certain nombre d’acteurs défaillants ou malveillants, qualifiés de «byzantins ». Cependant, les algorithmes BFT ne garantissent l’obtention d’un consensus que si le nombre d’acteurs byzantins reste inférieur à un certain seuil, généralement égal à 1/3 du nombre total d’acteurs. Pour savoir si cette hypothèse de fonctionnement est vérifiée pour un système distribué, et donc si le consensus atteint est fiable, il est nécessaire de pouvoir identifier et compter les acteurs byzantins au cours de l’exécution du système.
Notre méthode de vérification à l’exécution permet d’identifier les comportements byzantins et de fournir des preuves publiques de ces comportements. Cette méthode inclut les trois étapes suivantes basées sur l’outil d’analyse formelle MAAT IAT du CEA-List :
l’évaluation de la conformité du comportement de chaque acteur par une technique formelle de conformité de la multi-trace au regard de sa spécification (MAAT IAT). Lorsqu’un acteur byzantin est identifié, le modèle est mis à jour pour intégrer cette information et permettre la poursuite de l’analyse à la recherche d’autres acteurs byzantins éventuels.
Cette méthode se différencie de l’état de l’art par les innovations suivantes : elle permet d’identifier plusieurs acteurs byzantins opérant simultanément, elle fournit des preuves publiques et elle ne nécessite aucun matériel spécifique. En outre, elle peut être étendue à tout algorithme distribué pouvant être modélisé dans le langage MAAT IAT
