Introduction

La sécurité de Bitcoin, et d'autres blockchains, telles que Liquid, repose sur l'utilisation d'algorithmes de signatures numériques tels que ECDSA et les signatures Schnorr. Une bibliothèque C appelée libsecp256k1, nommée d'après la courbe elliptique sur laquelle la bibliothèque opère, est utilisée à la fois par Bitcoin Core et Liquid, pour fournir ces algorithmes de signatures numériques. Ces algorithmes utilisent un calcul mathématique appelé inverse modulaire, qui est un composant relativement coûteux du calcul.

Dans « Calcul rapide du pgcd à temps constant et inversion modulaire », Daniel J. Bernstein et Bo-Yin Yang développent un nouvel algorithme d'inversion modulaire. En 2021, cet algorithme, appelé « safegcd », a été implémenté pour libsecp256k1 par Peter Dettman. Dans le cadre du processus de vérification de cet algorithme novateur, Blockstream Research a été le premier à compléter une vérification formelle de la conception de l'algorithme en utilisant l'assistant de preuve Coq pour vérifier formellement que l'algorithme termine effectivement avec le bon résultat d'inverse modulaire sur des entrées de 256 bits.

L'écart entre l'algorithme et l'implémentation

L'effort de formalisation en 2021 n'a montré que l'algorithme conçu par Bernstein et Yang fonctionne correctement. Cependant, l'utilisation de cet algorithme dans libsecp256k1 nécessite de mettre en œuvre la description mathématique de l'algorithme safegcd dans le langage de programmation C. Par exemple, la description mathématique de l'algorithme effectue une multiplication matricielle de vecteurs qui peuvent être aussi larges que des entiers signés de 256 bits, cependant le langage de programmation C ne fournira nativement que des entiers allant jusqu'à 64 bits (ou 128 bits avec certaines extensions de langage).

L'implémentation de l'algorithme safegcd nécessite de programmer la multiplication matricielle et d'autres calculs en utilisant les entiers de 64 bits de C. De plus, de nombreuses autres optimisations ont été ajoutées pour rendre l'implémentation rapide. En fin de compte, il existe quatre implémentations distinctes de l'algorithme safegcd dans libsecp256k1 : deux algorithmes à temps constant pour la génération de signatures, un optimisé pour les systèmes 32 bits et un optimisé pour les systèmes 64 bits, et deux algorithmes à temps variable pour la vérification des signatures, à nouveau un pour les systèmes 32 bits et un pour les systèmes 64 bits.

Verifiable C

Pour vérifier que le code C implémente correctement l'algorithme safegcd, tous les détails d'implémentation doivent être vérifiés. Nous utilisons Verifiable C, qui fait partie de l'outil de logiciel vérifié pour raisonner sur le code C en utilisant le prouveur de théorèmes Coq.

La vérification se fait en spécifiant des préconditions et des postconditions à l'aide de la logique de séparation pour chaque fonction subissant une vérification. La logique de séparation est une logique spécialisée pour raisonner sur les sous-programmes, les allocations de mémoire, la concurrence et plus encore.

Une fois que chaque fonction a une spécification, la vérification se poursuit en commençant par la précondition d'une fonction, et en établissant un nouvel invariant après chaque instruction dans le corps de la fonction, jusqu'à établir finalement la post-condition à la fin du corps de la fonction ou à la fin de chaque instruction de retour. La plupart des efforts de formalisation sont dépensés « entre » les lignes de code, en utilisant les invariants pour traduire les opérations brutes de chaque expression C en déclarations de niveau supérieur sur ce que les structures de données manipulées représentent mathématiquement. Par exemple, ce que le langage C considère comme un tableau d'entiers de 64 bits peut en réalité être une représentation d'un entier de 256 bits.

Le résultat final est une preuve formelle, vérifiée par l'assistant de preuve Coq, que l'implémentation de l'algorithme d'inverse modulaire safegcd de libsecp256k1 à temps variable de 64 bits est fonctionnellement correcte.

Limitations de la Vérification

Il existe certaines limitations à la preuve de correction fonctionnelle. La logique de séparation utilisée dans Verifiable C met en œuvre ce que l'on appelle la correction partielle. Cela signifie qu'elle prouve uniquement que le code C retourne avec le bon résultat s'il retourne, mais elle ne prouve pas la terminaison elle-même. Nous atténuons cette limitation en utilisant notre précédente preuve Coq des limites de l'algorithme safegcd pour prouver que la valeur du compteur de boucle de la boucle principale ne dépasse en fait jamais 11 itérations.

Un autre problème est que le langage C lui-même n'a pas de spécification formelle. Au lieu de cela, le projet Verifiable C utilise le projet de compilateur CompCert pour fournir une spécification formelle d'un langage C. Cela garantit que lorsqu'un programme C vérifié est compilé avec le compilateur CompCert, le code assembleur résultant répondra à sa spécification (sous réserve de la limitation ci-dessus). Cependant, cela ne garantit pas que le code généré par GCC, clang ou tout autre compilateur fonctionnera nécessairement. Par exemple, les compilateurs C sont autorisés à avoir des ordres d'évaluation différents pour les arguments dans un appel de fonction. Et même si le langage C avait une spécification formelle, tout compilateur qui n'est pas lui-même formellement vérifié pourrait encore mal compiler des programmes. Cela se produit en pratique.

Enfin, Verifiable C ne prend pas en charge le passage de structures, le retour de structures ou l'attribution de structures. Alors que dans libsecp256k1, les structures sont toujours passées par pointeur (ce qui est autorisé dans Verifiable C), il y a quelques occasions où l'attribution de structures est utilisée. Pour la preuve de correction de l'inverse modulaire, il y avait 3 attributions qui devaient être remplacées par un appel de fonction spécialisé qui effectue l'attribution de structure champ par champ.

Résumé

Blockstream Research a formellement vérifié la correction de la fonction d'inverse modulaire de libsecp256k1. Ce travail fournit des preuves supplémentaires que la vérification du code C est possible en pratique. L'utilisation d'un assistant de preuve généraliste nous permet de vérifier des logiciels construits sur des arguments mathématiques complexes.

Rien n'empêche le reste des fonctions implémentées dans libsecp256k1 d'être également vérifiées. Ainsi, il est possible pour libsecp256k1 d'obtenir les garanties de correction logicielle les plus élevées possibles.

Ceci est un article invité de Russell O’Connor et Andrew Poelstra. Les opinions exprimées sont entièrement les leurs et ne reflètent pas nécessairement celles de BTC Inc ou de Bitcoin Magazine.

Source : Bitcoin Magazine

Le post L'implémentation de Safegcd formellement vérifiée est apparu en premier sur Crypto Breaking News.