abstract

Formal validation of smart contracts can avoid errors, vulnerabilities, and other adverse situations. In this process, human experts will convert the logic of smart contracts into mathematical statements, and then use automated processes to check the actual logic against the model of expected contract behavior. By combining formal verification with manual auditing, we can comprehensively evaluate the security of smart contracts.

synopsis

A smart contract is a computer program deployed on a blockchain that automatically runs when certain conditions are met. Smart contracts can be very simple or extremely complex, capable of holding assets worth millions or even billions of dollars. If there are security vulnerabilities in the smart contract code, it may cause devastating consequences, such as being stolen by criminals of all the assets they hold. In 2021, due to a spelling error in the smart contract, Automatic Market Maker (AMM) Uranium Finance was stolen $50 million. In 2021, due to a single code error, Compound Finance mistakenly issued a reward of $80 million. In 2022, Wormhole Bridge was stolen $320 million due to an error in the smart contract. Therefore, it is important to get the smart contract program right from the beginning. The smart contract adopts an open-source model, which means that once the contract is deployed, the code will be made public. If hackers discover any errors, they can immediately take advantage of them. In addition, the routine operation of patching security vulnerabilities over time is not useful, as the code of smart contracts typically cannot be modified after deployment.

How does smart contract verification work?

The formal verification of smart contracts is achieved by presenting the logic and expected behavior of smart contracts as mathematical statements. Subsequently, the auditor will use automated tools to check if these statements are correct. This process involves: Define the specifications and expected characteristics of contracts in formal language. Convert the code of the contract into formal statements, such as mathematical models or logic. Use automated theorem proving or model checking to verify the specifications and characteristics of contracts. Repeat the verification process to identify and fix any errors or deviations from expected characteristics.

Why is smart contract verification important

By applying mathematical reasoning, it helps to ensure that formally validated smart contracts avoid errors, vulnerabilities, and other unfavorable situations. Verification also helps to increase trust and confidence in contracts, as their characteristics have been rigorously tested and are correct and reliable. The following examples roughly illustrate how smart contract validation can help prevent significant financial losses and other catastrophic consequences.

Unified Exchange

Uniswap is a well-known AMM. The Uniswap V1 smart contract underwent formal validation during the development process. Prior to release, this formal validation discovered and fixed some rounding errors, avoiding Uniswap V1’s funding being drained.

oscillate

Balancer V2 is also a validated AMM. Formal verification has discovered and fixed cost calculation errors in the lightning loan function of smart contracts, which can make trading platforms vulnerable to theft.

Safe Moon

After deployment, SafeMoon V1 discovered an extremely minor error through formal verification. If the error is not detected, the contract owner may regain the contract if they perform certain actions before relinquishing ownership. Most manual audits of SafeMoon V1 forks miss this error because it requires analyzing specific combinations of program variable values to detect it. It is easy for humans to miss this problem, but machines can catch it in a timely manner.

How formal verification and manual auditing work together to play a role

Formal validation provides a systematic and automated way to examine the logic and behavior of contracts based on their expected characteristics. This can make it easier to identify and fix any potential errors or vulnerabilities. This is particularly useful for complex and subtle issues that are difficult to detect through manual inspection. Manual auditing involves experts reviewing the code, design, and deployment of contracts. Auditors will utilize their experience and professional knowledge to identify security risks and evaluate the overall security status of contracts. They can also confirm whether the formal validation process is being executed correctly and check for any issues that automated tools may not be able to detect. By combining formal verification with manual auditing, we can comprehensively evaluate the security of smart contracts. This can increase the chances of discovering and fixing any vulnerabilities. In this way, we are essentially adopting a deep defense security measure that combines the expertise of both humans and machines.

consequent

To ensure the security of smart contracts, it is necessary to combine formal verification and manual auditing to ensure a comprehensive and thorough evaluation of the security situation of smart contracts. Although formal validation requires high resource consumption, it is a worthwhile investment for contracts with high value or high-risk factors. After all, in the final analysis, security is more important than Taishan. We must give priority to security and ensure that smart contracts are free from errors, loopholes and adverse unexpected behaviors.