Comme rapporté dans un article précédent, La société d’audit Tweag a effectuée l’audit des contrats intelligents déployés par Minswap. Bien que Tweag a réussi à mettre en evidence plusieurs failles critiques, ces contrats ce sont révélés avoir une vulnérabilité majeure que l’auditeur a raté. Celle a été mise en évidence par les concurrents de Minswap, la DEX Wingriders.
Dans le but d’informer les plus grand nombre sur l’origine et la nature de la vulnérabilité, nous proposons ici la traduction de la réponse très riche en détails techniques écrite par Mathieu Boespflug de chez Tweag.
La voici…
Ce qui c’est passé
Au matin du 22 Mars 2022, nous avons été informé de l’existence d’une vulnérabilité critique que nous ne connaissions pas sur l’un des contrats de Minswap. Tous les membres de l’équipe chargés des audits étaient affligés par la nouvelle. En effet, nous avions effectué un audit de Minswap quelque temps auparavant. Sur un total de 13 failles, nous en avions trouvé 3 de critiques qui auraient pu permettre à un attaquant de vider les reserves. Mais nous avons raté la dernière.
Comment cela est arrivé
Le coeur de la vulnérabilité tient dans une fonction à l’apparence anodine. Celle ci vérifie qu’une valeur donnée est unitaire pour un actif:
isUnity :: Value -> AssetClass -> Bool
isUnity v c = assetClassValueOf v c == 1Bien que sans danger pris isolément, la fonction isUnity se révèle être désastreuse dans le contexte dans lequel elle s’avérait être utilisée:
validateMintNFT :: BuiltinData -> BuiltinData -> ()
validateMintNFT rawRedeemer rawContext =
let ...
mintValue = SC.txInfoMint info
in if isUnity mintValue (assetClass ownSymbol poolTokenName)
&& SC.spendsOutput info refHash refIdx
then ()
else error ()Dans la fonction validateMintNFT il est vérifié que les jetons qui identifient une pool (NdT: se réfère à la structure qui permet d’accueillir/gérer des fonds mis à contribution par les détenteurs du coin ADA) sont émis. A premiere vue, cela semble raisonnable: Vous ne pouvez produire qu’une seule copie du jeton qui identifie une pool donnée; et cela uniquement au moment de la creation d’une pool. Le problème c’est que la fonction isUnity oublie d’effectuer une verification importante: qu’il n’y a pas d’autres actifs émis. Ainsi, à la creation d’une pool, il est possible d’émettre un jeton différent appartenant à ownSymbol. En particulier, il est possible d’émettre un jeton qui identifie une pool existante, dupliquant ce qui était censé être un jeton unique. Une manière simpliste de corriger isUnity aurait consisté à écrire:
isUnity :: Value -> AssetClass -> Bool
isUnity v c = assetClassValue c 1 == vCependant, ceci est trop restrictif car à la creation d’une pool, il est en fait nécessaire de produire 3 jetons différents. Cette correction simpliste aurait donc rendu le contrat inopérant. Ce que nous voulons vraiment c’est d’être sûr qu’il n’y a qu’un seul jeton associé au symbole de chaque devise et que ce jeton n’a pas de copie. Mais les symboles des autres devises doivent pouvoir exister dans la valeur:
isUnity :: Value -> AssetClass -> Bool
isUnity v c = Map.lookup curr (getValue v) == Just (Map.fromList [(tok, 1)])
where (curr, tok) = unAssetClass cCette fonction pourrait éviter une attaque tout en maintenant les capacités fonctionnelles du contrat.
Due au fait que les pools de jetons sont censées permettre au pools (et uniquement les pools !) démettre des jetons de liquidités (LP), être autorisé à dupliquer les jetons des pools revient à ce que tout le monde a la capacité d’émettre des jetons LP. En fait, ceci n’est pas le seule mécanisme qui permet de dupliquer des jetons: Durant notre audit, nous avons réussi à dupliquer les jetons LP par d’autres méthodes (problème 2.2.1.2 dans notre rapport). Une fois que nous avons réussi à répliquer ces jetons LP et à cause d’une combinaison malheureuse d’instinct et de biais de confirmation, nous n’avons pas réalisé que l’hypothèse d’unicité des jetons de pool était en fait fausse: Ce n’est pas par ce qu’un mécanisme donné peut être exploité d’une certaine manière qu’il ne peut pas l’être d’une autre manière aussi!
Une fois qu’il devient possible de dupliquer les jetons d’une pool, il est facile de dupliquer aussi les jetons LP puisque la procédure d’émission des jetons ne vérifie que le nom du jeton:
mkLiquidityValidator :: CurrencySymbol -> BuiltinData -> BuiltinData -> ()
mkLiquidityValidator nftSymbol _ rawContext =
let context = PlutusTx.unsafeFromBuiltinData rawContext
info = SC.scriptContextTxInfo context
ownSymbol = SC.ownCurrencySymbol context
...
nftTokenName :: TokenName
nftTokenName = case [o | o <- txOutputs, isJust (SC.txOutDatumHash o)] of
[o] -> case Map.lookup nftSymbol (getValue $ SC.txOutValue o) of
Just i -> case [m | m@(_, am) <- Map.toList i, am == 1] of
[(tn, _)] -> tn
lpTokenName :: TokenName
lpTokenName = case Map.lookup ownSymbol (getValue mintValue) of
Just i -> case Map.toList i of
[(tn, _)] -> tn
in if nftTokenName == lpTokenName -- !!! LP tokens can be minted when these match !!!
then ()
else error ()En permettant d’émettre de manière arbitraire des jetons LP pour n’importe laquelle des pools, un assaillant aurait pu facilement vider toutes les pools de leurs choix. Cela est un problème, très, très sérieux.
Epilogue: Qu’est ce qui aurait été utile?
Nos yeux nous ont trahis et nous n’avons vue que ce que nous voulions voir au lieu de voir la réalité des choses. C’est précisément pourquoi il est important d’avoir des méthodes de vérifications formelles ainsi que de preuves vérifiés par machine. Paraphrasant la citation célèbre de E. W. Dijkstra, “Le fait de tester des programmes peut être utilisé pour mettre en évidence des bugs, mais ne révélera jamais leurs absence!”. Des outils d’analyses assistés par machine aurait certainement aidé. J’irais même plus loin en disant qu’il ne faudrait même pas observer un code sans ces outils. Le problème ici est dual. Premièrement, de tels outils n’existent pas pour les contrats écrits en Plutus: nous sommes en train d’en produire, mais ceci demande du temps et beaucoup d’engagement.
Le cas présent fut une situation où nous avons échoué à identifier un bug dans un code. Avec le recul, cette erreur parait si simple qu’il est facile de se sentir honteux de l’avoir laissé passer. Ceci étant dit, aucun audit ne peut être 100% garantie car ils sont effectués par des êtres humains. Nos audits sont fait du mieux possible et nos rapports détaillent le plus de choses possibles. Même en ayant des preuves établissant l’exactitude d’un code, ou une vérification par machine, cela ne suffirait pas à garantir que ce code est exempt d’erreurs. La specification (NdT: fait référence au document écrit qui spécifie ce que doit faire un programme et comment le faire. Cela nécessite souvent l’utilisation de méthodes formelles) peut être elle meme fausse… ou alors les hypothèses sous-tendantes aux preuves formelles sont impossibles dans la pratique. Ces détails sur les hypothèses et sur les spécifications peuvent être incomprises durant les échanges entre l’équipe faisant l’audit et l’équipe qui effectue l’implementation. Toute forme d’audit, qu’il inclu ou non des méthodes formelles, est toujours un exercice visant à réduire autant que possible le risque compte tenu de la technologie existante.
Meme si nous ne pouvons être absolument certains de l’absence de bugs dans une implémentation, il est critique de developer des outils qui soient capables d’augmenter notre confiance. Chez Tweag, l’équipe des méthodes formelles a travaillée dure afin de peaufiner Pirouette, et cet outils aurait été capable de trouver le bug. Pirouette est en développement depuis longtemps à cause de changements réguliers au sein de l’écosystème de Plutus. Nous avons fait une démonstration du prototype de Pirouette au Sommet de Cardano 2021 et en avons discuté à la table-ronde sur le sujet de la certification, où nous étions déjà très clair sur l’importance de faire des audits assistés par des outils dédiés. Pirouette suppose que les contrats utilisent l’API StateMachine de Plutus. Nos observations dans le domaine est que les contrats utilisent rarement cette API. Nous adaptons donc Pirouette afin qu’il soit utilisable sur un plus grand nombre de contrats, Minswap inclut.
Les bonnes pratiques et les vulnérabilités courantes des contrats écrits en Plutus devraient être largement connues et comprises. Nous nous efforçons à améliorer autant que possible la documentation sur l’API de Plutus. Par exemple, dans la documentation à propos de assetClassValueOf, les développeurs pourront voir un avertissement précisant que si ils l’utilisent afin de chercher quelque chose dans un ensemble de valeurs, il est probable qu’il y a d’autres choses présentes qu’ils ne souhaitent pas dans cet ensemble. Qui plus est, la documentation sur l’API peut être l’endroit pour referencer des explications détaillées sur les vulnérabilités qui sont mises en évidence régulièrement, tel que celle discutée ici.
Les audits sont fait du mieux que l’on peut, mais inévitablement, c’est toujours le facteur humain qui a le dernier mot. Des incidents tels que celui que nous avons eu nous enseignent sur la manière dont nous, humains, pouvons optimiser les processus que nous établissons.
Bien que nous ne pouvons jamais être sûr de l’absence d’erreurs dans un programme, toute erreur mise en évidence est une opportunité pour en apprendre le plus possible sur la source de cette faute. Cette reflexion est ce qui permet de rendre de plus en plus rares les erreurs au sein de notre communauté.
.