What Happened

On the morning of the 22nd of March, 2022, we were notified about the existence of an unknown critical vulnerability on one of Minswap’s contracts. Everyone here on the audit team was dismayed, since we had conducted an audit for Minswap not long before. We found 3 critical issues that would have likewise enabled an attacker to empty the reserves, and 13 issues in total, but failed to find this one.

How It Happened

The heart of the vulnerability lies in this seemingly harmless function which checks that a given value possesses a single unit of an asset class:

isUnity :: Value -> AssetClass -> Bool
isUnity v c = assetClassValueOf v c == 1

While harmless in isolation, in the context it was used isUnity revealed itself to be disastrous:

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 ()

The validateMintNFT function is where tokens that identify a pool are minted. At first glance, it looks reasonable: you can only mint one copy of the token identifying a given pool, and you can do it only when creating a pool. The problem is that isUnity forgets an important check: that there is no other asset being minted. Therefore, you could also mint different tokens belonging to ownSymbol when creating a pool. In particular, you could mint a token identifying an existing pool, essentially duplicating what was supposed to be a unique token. A naive attempt at correcting isUnity would have read:

isUnity :: Value -> AssetClass -> Bool
isUnity v c = assetClassValue c 1 == v

Yet, that is too restrictive because pool creation mints three different tokens, so that would have broken the contract functionality. What we really want is to ensure that there is only one token belonging to the given currency symbol and its amount is one, but other currency symbols must be allowed to exist within the value:

isUnity :: Value -> AssetClass -> Bool
isUnity v c = Map.lookup curr (getValue v) == Just (Map.fromList [(tok, 1)])
  where (curr, tok) = unAssetClass c

This function would have prevented the attack while maintaining the correct contract functionality.

Because pool tokens were meant as a means of enabling pools (and only pools!) to mint liquidity position (LP) tokens, being able to duplicate pool tokens meant that anyone could mint LP tokens. In fact, this was not the only mechanism to duplicate LP tokens, during our audit, we managed to duplicate LP tokens through other means (issue 2.2.1.2 in our report). Once we managed to duplicate these LP tokens through some other means, through a terrible combination of survivorship and confirmation bias, we failed to identify that the assumption about the uniqueness of pool tokens was actually wrong: it is not because a given mechanism can be exploited in one way that it cannot be exploited in other ways too!

Once pool tokens could be duplicated, it was easy to duplicate LP tokens again since the minting policy only checks for the token name:

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 ()

With the ability to mint arbitrary LP tokens for arbitrary pools, an attacker could easily empty any pools of their choosing. This is very, very serious.

Epilogue: What Could Have Helped?

Our eyes failed us and read what our minds wanted to read, instead of what was really there. This is precisely why machine-checked proofs and formal verification are so important. Paraphrasing the famous quote by E. W. Dijkstra — “Program testing can be used to show the presence of bugs, but never to show their absence!”. Machine-assisted analysis tools would certainly have helped. I’d even go a step further and argue that perhaps we should never look at code without these tools. The problem here is twofold. On the one hand, there are no such tools for Plutus contracts: we are working on building them, but these are long and involved projects.

This was a situation where we failed to spot a bug in the code. In hindsight, it looks so simple that it’s easy to feel ashamed of letting that slip through. That being said, no audit would be one hundred percent guaranteed because they are conducted by humans. Our audits are done on a best effort basis and we state as much in our reports. Even a machine-checked proof-of-correctness would not suffice to guarantee the code is bug-free. The specification itself could be wrong… Or maybe the assumptions under which the proof was carried cannot be met. These details about assumptions and specifications might get lost in translation in between the auditing and the implementation team. Any form of auditing, whether it includes formal methods or not, is always an exercise in reducing risk as much as possible given current technology.

Even if we cannot be absolutely certain of the absence of bugs in an implementation, it is paramount we develop tools that are capable of increasing our confidence. At Tweag, the formal methods team has been working hard to polish Pirouette, and it would have been able to spot this bug. Pirouette has been in development for a long time due to changes around the Plutus ecosystem. We gave a demo of Pirouette’s prototype at the Cardano Summit 2021 and discussed it at the certification round table, where we were already adamant about the importance of tool-assisted auditing. Pirouette assumes that contracts use the StateMachine Plutus API. Our observation in the field is that contracts seldom do, so we are adapting Pirouette to be applicable to more contracts, including Minswap’s.

Best practices and common vulnerabilities for Plutus contracts should be widely known and well understood. We endeavour to improve Plutus API documentation wherever possible. For instance, in the docs of assetClassValueOf, developers should see a paragraph warning that if they are using it to look for something in the value map, there might be additional things they didn’t want in that map. Moreover, this API documentation could be the place to link to more in-depth explanations of vulnerabilities that were actually spotted in the wild, such as this one.

Audits are best-effort and inevitably, it is always the human factor that fails us. Incidents like these inform where to fine-tune the process us humans carry out.

While we can never guarantee the absence of faults in software, whenever a fault comes to light we take the opportunity to learn as much as we can from it. This reflection is what allows us to help make errors increasingly rare in our community.