En juin 2016, l’enthousiasme était grand à l’idée que « The DAO », construit sur la blockchain Ethereum, était sur le point de devenir le premier fonds d’investissement décentralisé et entièrement numérique au monde.
Mais en quelques semaines, il est devenu l’illustration des piratages DeFi après que des attaquants lui ont volé 50 millions de dollars d’éther.
Pour pirater le DAO, l'attaquant a exploité une vulnérabilité dite de réentrance, une vulnérabilité de concurrence dans laquelle une méthode d'un contrat intelligent spécifique est appelée alors qu'une autre méthode est encore en cours d'exécution, et le DAO n'est qu'une partie du développement à long terme du contrat intelligent.Le premier souffre de telles erreurs.
Les successeurs importants incluent Uniswap/Lendf.Me, qui s'est fait voler 25 millions de dollars en 2020, CREAM, qui s'est fait voler 18 millions de dollars en 2021, et Fei, qui s'est fait voler 80 millions de dollars en 2022.
La raison pour laquelle ces bogues persistent est qu'ils peuvent impliquer des interactions de code inattendues dispersées dans tout le contrat intelligent, parfois même dans différents contrats intelligents. Le nombre de ces interactions de code peut être très important, ce qui rend difficile pour les humains de détecter et d'éliminer les contrats intelligents involontaires. .code requis.
De plus, ces interactions sont souvent difficiles à tester automatiquement et systématiquement.
TLA+ : L'Exterminateur
Entrez Temporal Logic of Actions (TLA+), un langage pour spécifier et valider des systèmes complexes non seulement trouve les erreurs, mais vérifie également leur existence.
Comment est-ce possible, demandez-vous ? TLA+ est livré avec un ensemble d'outils pour une vérification formelle légère sous la forme de ce que l'on appelle la vérification de modèle. Grâce à la vérification de modèle, il explore de manière exhaustive toutes les interactions simultanées possibles du modèle de code – les domaines mêmes difficiles à tester – et trouve les bogues.
Imaginez un exterminateur qui éclaire chaque coin et recoin pour exposer et éliminer les parasites indésirables qui se cachent dans ces coins sombres qui sont souvent manqués ou ignorés. Il est important de noter qu’une fois le modèle de code créé, la vérification du modèle ne nécessite pratiquement aucune intervention humaine, ce qui la rend très rentable.
Pour illustrer avec quelques chiffres inventés : si les pratiques standard de l'industrie telles que les tests et les examens de sécurité éliminent 80 % des bogues et que la vérification formelle « lourde » en élimine 99 %, l'utilisation de TLA+ élimine 90 % avec un seul petit nombre d'efforts de vérification lourds.
Ordinateurs TLA+ et Internet
Notre équipe d'ingénieurs utilise TLA+ pour analyser tous les aspects de l'informatique sur Internet, y compris les contrats intelligents critiques en matière de sécurité qui s'exécutent sur la plateforme. Bien que les ordinateurs Ethereum et Internet aient des modèles d’exécution différents, des erreurs de réentrance peuvent apparaître dans les contrats intelligents sur les deux blockchains.
En fait, en raison de leur débit élevé, les ordinateurs Internet permettent plusieurs appels simultanés vers un seul contrat intelligent, ce qui oblige les auteurs de contrats intelligents à être plus prudents pour éliminer les interactions simultanées indésirables. La sécurité étant essentielle au succès des ordinateurs sur Internet, TLA+ est utilisé dans de nombreux contrats intelligents pour détecter les erreurs pendant la phase de développement.
Un conteneur d'analyse TLA+ (contrats intelligents pour ordinateurs sur Internet) a récemment été réalisé sur le nouveau Chain-Key Bitcoin (ckBTC), dont je partagerai les résultats ci-dessous.
Contrat intelligent ckBTC
Pour parler de l’analyse TLA+ de ckBTC, commençons par un aperçu de haut niveau de ckBTC. ckBTC est un jeton natif d'ordinateur Internet soutenu en toute sécurité par Bitcoin (BTC) dans un rapport de 1:1.
Le registre ckBTC est un contrat intelligent de conteneur sur la blockchain informatique d’Internet qui suit la quantité de ckBTC que possède chaque utilisateur final. Ce même registre permet aux utilisateurs finaux de transférer leurs ckBTC à d'autres utilisateurs finaux plus rapidement et à moindre coût que le transfert de BTC sur le réseau Bitcoin.
Afin de convertir ckBTC en BTC et inversement, les utilisateurs finaux interagissent avec un autre contrat intelligent, le monnayeur ckBTC.
À un niveau élevé, l’opération de conversion de BTC en ckBTC ressemble à ceci :
Étapes pour obtenir ckBTC :
1. L'utilisateur final transfère d'abord du BTC vers une adresse de dépôt Bitcoin spécifique à l'utilisateur, toutes les adresses de dépôt sont entièrement contrôlées par le code du conteneur intelligent ckBTC minter en raison de la signature ECDSA de la clé de chaîne, qui crée un nouvel UTXO appartenant au dépôt adresse;
2. L'utilisateur final informe le contrat intelligent ckBTC mint de l'UTXO nouvellement déposé en demandant à la monnaie de mettre à jour le solde de l'utilisateur ;
3. Le contrat intelligent du monnayeur utilise ensuite l'intégration Bitcoin des ordinateurs Internet pour récupérer tous les UTXO appartenant à l'adresse de dépôt contrôlée par le monnayeur mais spécifique à l'utilisateur. Le monnayeur sélectionne ensuite les nouveaux UTXO du réseau Bitcoin en leur envoyant des vérifications croisées. sa liste comptable interne des UTXO qu’il a traités ;
4. Enfin, le monnayeur demande au grand livre de créer un nouveau ckBTC pour tous les nouveaux UTXO dans un rapport de 1:1, et une fois terminé, il ajoute les UTXO nouvellement découverts à la liste des UTXO traités.
Avertissement : le processus ci-dessus omet le processus KYT (Know Your Transaction) par souci de simplicité.
Le contrat intelligent ckBTC rencontre TLA+
L’image de haut niveau présentée ci-dessus cache en fait un subtil problème de concurrence, et la bonne nouvelle est que nous pouvons détecter le problème à l’aide de la boîte à outils TLA+.
Mais avant que TLA+ puisse détecter quoi que ce soit, nous devons d’abord lui fournir deux choses :
Créer un modèle de notre système en utilisant le langage TLA+
Spécifiez les propriétés TLA+ que nous attendons du système à mettre en œuvre
Ce modèle est une version simplifiée mais néanmoins entièrement définie du système, qui comprend dans notre cas le contrat intelligent Minter, mais également toutes les autres parties pertinentes du système, à savoir le contrat du grand livre et le réseau Bitcoin.
Pour chaque composant, nous modélisons son état et la manière dont les actions pertinentes qu'un utilisateur final pourrait entreprendre (c'est-à-dire transférer du BTC ou du ckBTC, déposer du BTC ou appeler différentes actions exposées par le monnayeur) modifient l'état.
Tous ces éléments sont quelque peu simplifiés dans le modèle, avec les parties sur lesquelles l'analyse se concentre (par exemple le code du minter) modélisées plus en détail, tandis que d'autres parties (par exemple le réseau Bitcoin) sont modélisées de manière moins détaillée. En fait, un modèle TLA+ est similaire à une spécification de conception détaillée d’un système.
Intuitivement, la principale fonctionnalité que nous souhaitons implémenter est de garantir que notre ckBTC est entièrement pris en charge. En d’autres termes, aucun utilisateur final ne devrait pouvoir « dépenser deux fois » son BTC déposé pour obtenir plus de ckBTC que ce qu’il a déposé.
Mais pour analyser une telle propriété, il faut rendre cette intuition très précise en l'exprimant formellement dans le langage TLA+. Notre définition formelle est que l'offre totale de ckBTC (c'est-à-dire la somme de tous les soldes ckBTC de l'utilisateur final, tels que stockés dans le grand livre ckBTC) ne dépasse pas le montant total de BTC contrôlé par le conteneur de frappe (c'est-à-dire la valeur de tous UTXO détenus par une adresse de dépôt).
Détecter et résoudre les problèmes
Une fois que nous avons créé le modèle et les propriétés, la boîte à outils TLA+ peut analyser le modèle. Pour exécuter l'analyse, nous définissons d'abord les paramètres d'exécution de l'analyse. Par exemple, notre configuration pour ckBTC n'inclut que deux utilisateurs finaux différents et une petite quantité de l'offre totale de Bitcoin (par exemple, 5 satoshis).
Bien que ce cadre soit très limité, des études empiriques montrent que la grande majorité des problèmes des systèmes informatiques peuvent se trouver dans un petit nombre d’entités. La petite configuration permet à l'analyse d'explorer systématiquement toutes les séquences d'actions possibles définies par le modèle et de vérifier si les propriétés prescrites sont valables dans une telle séquence.
De plus, l’analyse s’exécute de manière entièrement automatique, c’est-à-dire qu’elle ne nécessite aucune intervention humaine, et si ces propriétés ne sont pas vérifiées, elle nous fournit la séquence exacte des opérations qui viole cette propriété.
Par exemple, l'analyse peut révéler que nous pouvons violer notre propriété « pas de ckBTC non sécurisé » dans un scénario comme celui illustré ci-dessous :
ici:
Les utilisateurs finaux déposent du BTC, comme auparavant ;
Cependant, l'utilisateur final demande désormais au monnayeur ckBTC de mettre à jour le solde deux fois de suite, et sur un ordinateur Internet, ces mises à jour peuvent interagir simultanément avec d'autres contrats intelligents ;
Deux mises à jour exécutées simultanément demandent au réseau Bitcoin tous les UTXO déposés par l'utilisateur final, et toutes deux reçoivent en réponse le même UTXO déposé à l'étape 1. Puisque l'UTXO n'est pas encore dans la liste « traitée », les deux mises à jour pensent qu'UTXO est nouveau ;
Les deux mises à jour demandent au grand livre de frapper le montant correspondant de ckBTC à l'étape 4.
Par conséquent, à la fin de l’étape 4, nous sommes dans un état où l’offre de ckBTC est deux fois supérieure à la somme des UTXO dans les adresses de dépôt, ce qui viole notre propriété « aucun ckBTC non pris en charge ».
Notez que cette erreur se produit uniquement parce que les mises à jour du solde de l'utilisateur final sont exécutées simultanément - il s'agit en fait d'une erreur réentrante du même style que celle qui a fait tomber The DAO.
Une façon de résoudre ce problème est d'empêcher les mises à jour du solde de s'exécuter en parallèle pour le même utilisateur final. Nous pouvons le faire en demandant au monnayeur de stocker l'utilisateur final dans une liste d'utilisateurs « verrouillé » lorsque la mise à jour du solde démarre, et de les y conserver. pendant toute la durée de la liste de mise à jour pour y parvenir.
Si l'utilisateur final tente de lancer une autre mise à jour simultanée du solde, la mise à jour vérifiera et trouvera d'abord cet utilisateur final spécifique dans la liste des utilisateurs verrouillés, puis sera abandonnée.
Notez que nous simplifions légèrement l'attaque ici : le verrouillage est en fait un modèle assez courant pour les contrats intelligents IC, et les monteurs de ckBTC l'ont déployé depuis le début. Cependant, un verrouillage mal exécuté ouvre la porte aux attaques ci-dessus, que TLA+ est capable de détecter.
De plus, nous avons trouvé des cas extrêmes qui violaient « aucun ckBTC non pris en charge » et d'autres propriétés importantes, et une fois que nous avons appliqué tous les correctifs, TLA+ a pu vérifier et confirmer qu'il n'y avait plus de violations de propriété dans notre configuration définie.
Devriez-vous utiliser TLA+ pour vos contrats intelligents ?
Absolument! D'accord, d'accord, je devrais peut-être fournir une réponse plus nuancée, que notre équipe R&D utilise pour les contrats intelligents critiques sur les ordinateurs Internet chaque fois qu'une concurrence non triviale est impliquée.
Par exemple, l'analyse TLA+ a révélé de subtils bogues de concurrence dans la gouvernance informatique de l'Internet et les conteneurs Ledger qui avaient été manqués lors des examens manuels de sécurité précédents et qui auraient pu conduire à des problèmes, des cas et des points majeurs - TLA+ a découvert des problèmes aussi épineux. Une explosion absolue.
Bien sûr, il y a un prix à payer en termes d’acquisition du savoir-faire puis de construction du modèle, mais empiriquement, le prix est raisonnable, surtout compte tenu des enjeux élevés de la sécurité de la blockchain.
Il ne faut pas se laisser intimider par le langage TLA+ lui-même, malgré son nom intimidant, accéder à ses puissantes fonctionnalités est assez simple. En fait, une aide-mémoire TLA+ décrivant presque toutes les fonctionnalités de TLA+ pourrait tenir à peu près sur une seule page :
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
De plus, l'effort requis pour créer le modèle est comparable aux examens de sécurité manuels standard. Par exemple, pour un monteur ckBTC, il faudrait au total environ 3 semaines à 1 personne pour comprendre la conception, créer le modèle initial et les propriétés.
Le modèle TLA+ résultant est beaucoup plus simple que l’implémentation, à la fois parce qu’il est plus simple que le code et en raison de la nature de haut niveau de TLA+. Le modèle du minter ckBTC nécessite environ 250 lignes de code par rapport aux milliers de lignes d’implémentation de Rust. Il est peut-être surprenant de constater que l’une des tâches les plus difficiles en termes d’efforts consiste à spécifier les propriétés requises, car on trouve souvent des lacunes dans les spécifications intuitives.
Une fois le modèle terminé, l’analyse (vérification du modèle) s’effectue automatiquement. L’analyse peut prendre beaucoup de temps – par exemple, pour ckBTC, cela a pris plus de 20 heures. Enfin, un autre avantage de TLA est que la modélisation et l'analyse peuvent être effectuées dès la phase de conception avant l'implémentation du code, ce qui permet d'éliminer ultérieurement les refactorisations importantes dues à des erreurs de conception.
Où TLA+ ne sert à rien
Du côté négatif, TLA+ est moins utile pour les programmes séquentiels complexes que pour les programmes simultanés, et il n'est pas non plus efficace pour gérer des protocoles cryptographiques complexes, pour lesquels il existe d'autres outils (par exemple Tamarin) qui sont plus utiles.
Enfin, il y a le problème de maintenir la synchronisation du modèle TLA+ et de l'implémentation réelle, car à mesure que le code d'implémentation évolue au fil du temps, il peut ne plus être conforme au modèle, ce qui peut être difficile à comprendre sans la prise en charge des outils.
En fait, notre équipe R&D essaie de résoudre ce problème – j’espère que nous pourrons bientôt partager quelques outils avec vous !
J'espère que cet aperçu a éveillé votre intérêt pour l'utilisation de TLA+ pour vos propres contrats intelligents critiques, et si c'est le cas, restez à l'écoute : un article de suivi avec un didacticiel plus approfondi sur la façon d'utiliser TLA+ pour les contrats intelligents sera bientôt disponible, et ci-joint est un véritable modèle TLA+ développé par notre équipe R&D.
Contenu IC qui vous intéresse
Progrès technologique | Informations sur le projet |
Collectez et suivez IC Binance Channel
Restez à jour avec les dernières informations