Using formal methods to prevent creating money out of thin air
(Blog with Danil Annenkov and Eske Hoy Nielsen)
The Polygon network recently had a vulnerability which would allow hackers to create an arbitrary number of their MATIC tokens. The analysis above explains that this is due to a missing check that the sending address has enough balance. Such vulnerabilities are not uncommon in decentralized finance. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications.
Fortunately, here formal methods can help to prevent such vulnerabilities. In the case of polygon, this could have been prevented by clearly specifying properties of the MATIC token. Although, their token is based on ethereum’s ERC20 standard, it is different is in a small, but very important, way. The ERC20 standard comes with an informal specification which would have prevented this. In that, one can derive from the informal specification that this check should have been carried out. In fact, we have checked a mathematical proof of this fact using a computer proof assistant. The proof is based on precise modelling of a blockchain, as we will now explain.
The ConCert framework, developed at CoBRA, contains an abstraction of account based blockchains, such as the Ethereum blockchain. In fact, the model is so close to more modern blockchains, like Tezos and concordium, that one can automatically convert the smart contracts written in a proof assistant to smart contracts in the CamLIGO and rust smart contract languages and deploy them on the blockchain.
This model also allows us to find other high profile vulnerabilities using automated property based testing (here and here).
Concretely, our model of ERC-20 tokens shows that the vulnerability is not present.
Of course, one wonders whether such vulnerabilities exist in other token standards. We have a model of the analogous Tezos standard FA1.2 in ConCert, which also prevents this vulnerability. This is part of more a bigger project to formalize a decentralized exchange. Concurrent work on the formalization of Tezos token standards is described in this paper.
Finally, ConCert includes a formalization (by Danil Annenkov) of the Concordium CIS token standard. This formalization shows that (our model of) the CIS-tokens does not have the Polygon vulnerability. The CIS standard, like the ERC20 and FA1.2 standards, are specifications in natural language. Hence, they are currently not enforced by an automatic tool, like a type checker. There are various ways to include such static checks. One way is already present in the ConCert framework, as it includes the basic functionality to statically check that smart contracts, like tokens, actually adhere to the described standards.
