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