How Formal Verification Secures Smart Contracts: An Example Using Beosin-VaaS

Formal verification, as one of the core technologies of Beosin, has helped thousands of smart contracts to solve security issues. Why can formal verification detect vulnerabilities that cannot be discovered manually? Today we prepared an example on Ethereum for illustration.

1. Example: Wizard_game.sol

*Notes*

• This is an updating contract for the duel properties of wizards.
• Each wizard has its own dueling arena and dueling power.
• resolveTimedOutDuel interface updates the duel properties of both wizards according to their duel status.
• If wizard 1 does not fail in this duel, the duel power of wizard 2 is transferred to wizard 1, and the duel power of wizard 2 is cleared.
• We added a formal verification attribute assert (wiz1.power+wiz2.power == old_power1+old_power2);”, because the logic of the code is that the wizards’ duel power is transferred to each other, so the total duel power is constant, and the assert condition here should be satisfied at all times. Otherwise, there is some kind of logic vulnerability that causes the total duel power to change, resulting in the assert restriction not being satisfied.

The detailed code is as follows.

2. Upload the contract

Add a new project

Create the project to be detected in the VaaS tool. The project to be detected is an ETH type project, so click the “Add new project” button at the top left, enter the project name, select the project type, and click OK.

Add contract folder

Select the project you just created, click the “Add contract folder” button at the top left and enter the folder name.

Upload the contract file

Select the folder you just created and click the “Upload” button at the top left to upload the contract file for detection.

3. Contract detection

After uploading the contract, select the contract, enter the detection parameters according to the contract content, and click “Start detection”.

4. View the results

Check the detection results after the contract detection is completed. Specific information of the vulnerability are presented via code location, error description, and fix recommendations.

5. Result analysis

After analysis, the reason for this vulnerability is that when the resolveTimedOutDuel interface is executed to update the duel properties of Wizard 1 and Wizard 2, the case that Wizard 1 and Wizard 2 are equal is not considered. In this scenario, the duel power of Wizard 1 will first be doubled and then cleared, resulting in a change in the total duel power before and after the Wizard 1 status update, which causes the assert assertion to fail.

6. Formal verification logic

In this contract, since the duel power transfer is performed between wizard1 and wizard2, the logical relationship is that the sum of wizard1 and wizard2 duel power is a constant value and does not change, so the formal verification property can be written as: “assert(wiz1.power+wiz2.power == old_power1+old_ power2);”.

The detection flow is as follows.

• Since the input is not a real value, it abstracts wizardId1, wizardId2 as symbolic values; two cases exist at this point.

1) wizardId1 != wizardId2；

2) wizardId1 ==wizardId2;

• Before executing the _updatePower interface, record the values of wiz1.power and wiz2.power, represented by old_power1 and old_power2. There are also two cases.

1) When wizardId1 != wizardId2: old_power1+old_power2

2) When wizardId1 == wizardId2:

old_power1+old_power2 = 2*old_power1 = 2*old_power2

• After the execution of the _updatePower interface is completed, the values of wiz1.power and wiz2.power are changed, and there are still two cases.

1) When wizardId1 != wizardId2: As wiz1.power=old_power1+old_power2, wiz1.power=0, so：

wiz1.power+wiz2.power = old_power1+old_power2+0 = old_power1+old_power2；

At this point the sum of the dueling energies of Wizard 1 and Wizard 2 remains unchanged.

2) When wizardId1 == wizardId2: As wiz2.power=0, so wiz1.power+wiz2.power = 2*wiz2.power = 2*0 = 0

At this point, the sum of Wizard 1 and Wizard 2 dueling power is 0.

• Since formal verification solves for the values under each path, so wiz1.power + wiz2.power == 0 when wizardId1 == wizardId2 is satisfied, and if old_power1 + old_power2 ! = 0 is also satisfied, there will be a non-zero value equal to 0 error, i.e. “ old_power1+old_power2 ! = wiz1.power+wiz2.power”, resulting in the solution result violating the constraints of the formal property and thus a program vulnerability is discovered.

7. Solving the issue

This time we add a condition to the resolveTimedOutDuel interface “require(wizardId1 ! = wizardId2);” to ensure that wizard1 and wizard2 are not equal when performing duel property updates, and see if the vulnerability still exists.

8. Deficiencies in manual verification and fuzzing test

For the verification of smart contracts, it is usually accompanied by manual verification, relying on their own experience to continuously try to enumerate various input conditions that may not be satisfied, so as to compare the output to determine whether there is a vulnerability. The heavy workload, costly manual labor, repetitive work, and not all the paths are covered are the main problems for manual verification.

The other way of verification for smart contracts — fuzzing test, although can solve the problem of costly manual labor, there may also be some input missing problem as no actual implementation mechanism exist only by brute force to continuously enumerate each input. There are also problems of detecting some logical vulnerabilities based on the path.

9. Advantages of formal verification

For formal verification, there is no need to understand the details of the specific implementation of the contract, no need to construct specific scenarios, and no need for data enumeration. Reusable security properties are condensed through logical relationships, and rigorous mathematical formulae are reasoned for each path of the contract. Each possible system state and operation is automatically detected to calculated satisfiable solutions, and the possible security issues under each path are finally detected based on the comparison of the solution results to see if the security properties are violated.

Contact

If you have need any blockchain security services, please contact us:

Website Email Official Twitter Alert Telegram LinkedIn