With more than $500 million worth of tokens lost due to financial exploits in DeFi protocols during 2020, and $343m lost in the first 5 months of 2021 alone, security has been top of mind for all projects. A reputable audit report is the current standard, but that’s not always enough on its own. There are countless ways for hackers to exploit vulnerabilities, both technical and economic. This can be through manipulation of oracles (like in YFI), replay of transactions in mempools and front-running them, or implementation bugs in the pool contracts. But how can we reduce the damage? While there are insurance alternatives like Nexus Mutual and CertiKShield, those are for remediating the damage, not preventing it.
Certified contracts–which are safely composed from individual provably correct code constructs–present hard proof of the security of a DeFi protocol. These functions and statements are rigorously proved by math, and their correctness is independently verifiable (i.e.decentralized). While this level of rigor has been deemed as difficult and time-intensive, certain fundamental underpinnings of DeFi make sense to certify. Take Uniswap V2, for example, which had $57B volume last year and is copied by most altcoin DEXs (e.g. PancakeSwap on BSC, Pangolin on Avalanche). An unforeseen error in the code of such an important engine may have substantial cascading effects for the rest of blockchain.
For that reason, our research team at CertiK is excited to share our certified version of Uniswap V2, the provably correct, certified version that replaces trusted parties with cryptography, formal methods-driven program constructs, and game-theoretical incentive alignment.
For those inclined, we’ve put together a detailed explanation of our research below.
In Uniswap V2, let’s look at 2 things that you want to ensure. Firstly, you want to ensure that the cost of manipulating token prices in the AMM is high, which makes it hard for malicious actors to drain funds quickly. Secondly, because people use AMMs as on-chain price oracles, you want to ensure that malicious actors cannot move the price of an asset for less money than they would be able to make trading derivatives on that product.
Looking at the typical pen-and-paper statement of this property, you usually get:
There are multiple issues with such pen-and-paper statements and proof. Firstly, it is incomprehensible to many people. You can see that it uses Greeks, mathematical functions, and some analysis theorems. The complex paper proof may also contain holes and mistakes. Even if the statement is comprehensible and the paper proof can be trusted, people still don’t know if the code implementation of the protocol is faithful or not — one may start with the formula, but the actual contract methods won’t look exactly like it. What’s more, the math — with real numbers on paper and with bounded integers in contract execution — don’t always match and cannot be naively assumed to be the same.
Hard “proof evidence” from the above statement and paper proof — even with other necessary reasoning, traditional code-review or even the basic “formal verification” — simply won’t suffice.
Alternatively, in a certified Uniswap V2 protocol, you would say:
Seems more comprehensible, right? What’s even more exciting is the following:
You can actually prove it in precise terms which are understandable and verifiable by machines!
Now, what exactly makes the above proof a piece of hard “security evidence”?
Compared to the pen-and-paper proof, this one is more rigorous about integer approximation in the actual Uniswap implementation (e.g., rounding errors, etc,). Moreover, it embodies the very spirit of crypto by removing the cycle of human interference from the current DeFi security landscape and replaces trust in auditors with a mechanized, decentralized version of provable security. Plus, since this proof is actually checked against the bytecode generated by a certified smart contract compiler, we don’t even have to trust the often buggy Solidity compiler!
DeFi is still a new frontier, but by using certified contracts and proofs, we can navigate more cautiously and securely. Certification of large contracts takes time, but with leading techniques and technologies such as those used by the CertiK team, this process is not impossible. We aim to continue raising the standards of security in blockchain, and you can follow along at certik.comto view the security scores of your favorite projects. If your favorite DeFi project isn’t on the list, or if you want it to become one of the first provably correct certified contracts, have them contact us at bd@certik.io to get started!
Footnotes:
The contract and its proof, as discussed in this article, are deployed on CertiK Chain. You can check them yourself here: [links]
