This article is a community contribution. The author is David Tarditi, VP of Engineering at Certik, a Web3 smart contract auditing company.
Summary
Formal verification of smart contracts ensures that they are free of bugs, vulnerabilities, and other unwanted behavior. It is performed by a human expert who presents the smart contract logic as mathematical statements, then runs them through an automated process that checks the actual logic against the smart contract's expected behavior models. The combination of formal verification and manual audit provides a comprehensive assessment of the security of a smart contract.
Introduction
Smart contracts are computer programs implemented on a blockchain that execute automatically when certain conditions are met. They can range from simple to extremely complex, and can contain assets worth millions or even billions of dollars.
Security vulnerabilities in smart contract code can lead to serious consequences, including the theft of all smart contract assets. In 2021, Automated Market Maker (AMM) Uranium Finance suffered a $50 million theft due to a typo in a smart contract.
Also in 2021, Compound Finance handed out $80 million in unearned rewards due to erroneous character alone. In 2022, $320 million was stolen from Wormhole Bridge due to a bug in one of its smart contracts.
It is important that the smart contract program is correct from the beginning. Smart contracts are open source, meaning that once the contract is deployed, the code is available to the public. If a hacker finds a bug, they can exploit it immediately. Additionally, patching security vulnerabilities is not a sustainable option, as the contract code typically cannot be modified after it is deployed.
How does smart contract verification work?
Formal verification of smart contracts is carried out by presenting the logic and desired behavior of the contracts as mathematical statements. Auditors then use automated tools to verify whether the statements are correct.
The process involves:
Define the specifications and desired properties of a contract in formal language.
Translate smart contract code into a formal representation, such as mathematical models and logic.
Use automated theorem provers or model checkers to validate contract specifications and properties.
Repeat the verification process to find and correct any errors or deviations from the desired properties.
Why smart contract verification is important
Using mathematical reasoning helps ensure that formally verified contracts are free of bugs, vulnerabilities, and other unwanted behavior. It also helps increase confidence in the contract since its properties have been rigorously tested to be correct.
Below we include some examples of how smart contract verification has helped prevent significant financial losses and other serious outcomes.
Uniswap
Uniswap is a well-known AMM. When the first version of the Uniswap smart contract was developed, it was formally verified. Prior to its launch, this formal verification found and corrected rounding errors that may have led to funds being drained from Uniswap V1.
Balancer
Balancer V2 is also known as an AMM that has been formally verified. Formal verification found and corrected an incorrect fee calculation related to the flash loan functionality in the smart contract, which could have left the exchange vulnerable to theft.
SafeMoon
SafeMoon V1 contained a subtle bug that was discovered in formal verification after contract implementation. If certain transactions were made before relinquishing ownership of the contract, it was possible for the owner of the contract to relinquish ownership and then reacquire it.
This bug went unnoticed in most manual audits of the SafeMoon V1 forks because finding it required analyzing specific combinations of the program's variable values. This is something that easily escapes human control, but is easily discovered by a machine.
How formal verification and manual audit work together
Formal verification provides a systematic and automated way to corroborate the logic and behavior of a contract in relation to its desired properties, making it easier to identify and correct potential errors and bugs. It is especially useful for finding complex and subtle problems that may go unnoticed by manual inspection.
Manual audit involves expert review of the code, design and implementation of the contract. The auditor uses his experience and skill to identify security risks and evaluate the overall security posture of the contract. You can also confirm that the formal verification process was completed correctly, as well as review any issues that are not detectable by automated tools.
The combination of formal verification and manual auditing provides a comprehensive and thorough assessment of the smart contract's security, increasing the likelihood of finding and fixing any vulnerabilities it may contain. The result is a defense-in-depth approach to security that leverages the unique capabilities of humans and machines.
Conclusions
To ensure the security of smart contracts, it is essential to follow a formal verification and also a manual audit, thus ensuring a comprehensive and thorough assessment of the security posture of the smart contract.
Although formal verification can be resource-intensive, it is worth the investment for contracts with high-value or high-risk factors. Finally, it is essential to prioritize security and ensure that smart contracts are free of bugs, vulnerabilities, and unwanted behavior.
Further reading
What are smart contracts?
What is a smart contract security audit?
Disclaimer and Risk Warning: This content is presented "as is" for general information and educational purposes only, without representation or warranty of any kind. It should not be construed as financial advice, nor is it intended to recommend the purchase of any specific product or service. Digital asset prices are volatile. The value of an investment can go down as well as up, and you may not get back the amount invested. Only you are responsible for your investment decisions. Binance Academy is not responsible for any losses you may incur. This material should not be construed as financial advice.
