Formal Verification – The Ultimate Solution for Contract Security

Formal Verification - Ultimate Contract Security Solution

Author: @dvzhangtz; Source: Twitter @dvzhangtz

Recently, I’ve been looking at some formal verification projects and I feel that they will still be interesting narratives in the new cycle.

However, this technology, as the most important component of contract security, is almost invisible on Chinese forums. So I have summarized the knowledge I have gained from studying…

Now, you can take away this knowledge in five minutes.

• Long Push Receiving 1 million ARB airdrop, Summary and Reflections on 2 Years in the Circle
• Singapore VS Hong Kong, TOKEN2049 ignites the battle of the twin cities of Web3!
• Classification of Web3 Game Players Prototypes

Background: Smart contracts are one of the core elements of the blockchain world. If there are security issues with contracts, the money in Dapps is lost. According to the Rekt leaderboard, the direct losses caused by contract security can reach as high as $600 million, and the indirect losses are even more severe. Insecure contracts can cause the community to lose confidence in the project. https://rekt.news/leaderboard/

Traditionally, in order to make contracts more secure, the approach is to add layers of protection, for example:

1. Use standard function libraries such as @OpenZeppelin to write code and make the code more secure.

2. After writing, use some tools for preliminary screening to see if there are any issues.

3. Write some test programs to test the contract in modular form with sample data.

4. …

However, no matter how thick the armor is, there will always be vulnerabilities, and test programs can only be tested with some samples, it is impossible to exhaust all possibilities. So these methods can only reduce the possibility of security issues, but cannot guarantee that the contract is problem-free. Is there a way to ensure that the contract does not have certain security vulnerabilities, just like a prophet verifying werewolves? The answer is – formal verification.

To perform formal verification, a few steps are needed:

1. Write formal specifications, defining what we want to verify.

2. Use formal analysis frameworks to verify. These tools will automatically verify whether the contract meets the specifications we defined.

3. Identify problems that occur in certain situations.

4. Modify the code to solve the problems.

A real case: Wizard Duel @CHZWZRDS

https://github.com/dapperlabs/cheezyverse/blob/fef271db4c18c00949de291da0b46a1397216306/contracts/BasicTournament.sol#L2059…

The following code says: when the game times out, Wizard 1 will absorb Wizard 2’s power, and Wizard 2’s power will be cleared.

As a gamefi, this power is naturally important.

In theory, this power can only be transferred between two wizards, but if a hacker discovers a vulnerability in this code, they can make the power increase or disappear out of thin air, which will undoubtedly have a significant impact on this Gamefi.

Using normal security verification methods, we used several test data and found that everything was running nicely. We were even ready to deploy it directly on the chain. But wait, why not try formal verification?

Step 1: Define formal specifications

We hope that the power will only be transferred between wizards and will not increase or disappear out of thin air, which means: wiz1.power + wiz2.power = old_wiz1.power + old_wiz2.power.

Step 2: Formal Analysis Framework Automated Verification

These tools are essentially a technique for exploring all possible paths of contract execution to ensure that the specification is satisfied on all possible execution paths.

Step 3: Problem Discovery

Discovered a problem! A magical problem, if the two wizards in the duel are the same person, that is, the addresses of the two sides of the duel are the same, it will reset the user’s energy to zero! Step 4: Correcting the Problem Now that the problem has been discovered, it is actually very easy to fix. We just need to add one line of code, perform a pre-check to ensure that the two sides of the duel are not the same person~

A similar problem is the classic K-value verification problem. The core of Uniswap is the constant product model K=x*y, where the K-value is the product of the number of tokens held by the LianGuaiir contract, and each subsequent transaction must increase the K-value (transaction fee). If a hacker discovers a vulnerability in the contract, they can make their own transactions not comply with the constant product, turning the contract into an ATM. This problem can also be avoided using the approach mentioned above.

From the above text, we can perceive several characteristics of formal verification:

1. Finality: It can prove that certain problems do not exist in the contract;

2. Dependency on specifications (serious): The above text only verifies one specification, but actual contracts may face many problems. We may omit some specifications, and writing specifications itself is quite labor-intensive. Therefore, formal verification mainly focuses on verifying some key properties of the contract.

3. Performance issues (serious): Using a formal analysis framework for automated verification essentially explores all possible paths of contract execution that comply with the specification. This may encounter state explosion and path explosion problems. At the same time, it uses SMT solvers and other constraint solvers, which are also computationally intensive. So, in the future, outsourcing this matter in a cost-effective manner might promote its development.

If you want to perform formal verification, the relevant tools are as follows:

Languages for writing formal specifications

Act: https://github.com/ethereum/act

Scribble: https://docs.scribble.codes

Dafny: https://github.com/dafny-lang/dafny…

Validators for checking correctness

Certora Prover: https://docs.certora.com/en/latest/index.html…

Solidity SMTChecker: https://github.com/ethereum/solidity…

solc-verify: https://github.com/SRI-CSL/solidity…

KEVM: https://github.com/runtimeverification/evm-semantics…

We will continue to update Blocking; if you have any questions or suggestions, please contact us!