How to use Security Prover

A step-by-step guide for using the scanning engine Security Prover on MetaScan

Here is a step-by-step guide for using the scanning engine Security Prover on MetaScan based on the demo contract code. You can also watch the video instructions. (Video Link: https://youtu.be/CatvrkcJTNk)

1. Upload the smart contract to MetaScan. Click "Add Projects" and select "Upload Files" to add the project that needs scanning.

   

   
2. Select the appropriate project type based on the situation. Here we select "Framework-less Solidity Files" and click "Continue".

   
3. Upload a zip file of the project and click "Continue".

   
4. Input a project name and click "Upload" to upload the project.

   
5. Configure contract analysis settings and scan. Click "Start Scan" to prepare for scanning.

   
6. Select "Security Prover" and fill in the name of the contract to verify in "Entry Contract", here we fill in "Token". Then click "Start Scan" to start security scanning.

   

   
7. Review key metrics and information from the report.

   
8. Click on "EquailzationOfTransferBalances" under "Rules" and check the "Call Trace" information based on violation. From the information, we know the violated condition is assert(balanceBefore == balanceAfter); From the "Rule Call Resolutions" on the right, we know that when msg.sender is the same as $to, it will violate the check condition

   
9. Click on the "transfer" in the "Call Trace" to check deeper call stack information. In uint256 senderAmount = _balances[sender]; senderAmount is 20000 In uint256 recipientAmount = _balances[recipient]; recipientAmount is 20000

   
10. After calling _balances[sender] = senderAmount.sub(amount);, _balances[sender] becomes 19900

    
11. After calling _balances[recipient] = recipientAmount.add(amount);, _balances[recipient] becomes 20100

    

Thus the assertion assert(balanceBefore == balanceAfter); is finally violated.