# How to use Security Prover

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](https://youtu.be/CatvrkcJTNk).  (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.

   <div><figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FWPtKdnAjTNd1cJ0OTYM0%2Fstep1-01.png?alt=media&#x26;token=c270bb6a-327f-4cc5-8397-1bb33da80dfd" alt=""><figcaption></figcaption></figure> <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2F8ct4OTkX7Jg8JSbX1t8s%2Fstep1-02.png?alt=media&#x26;token=92d4c545-9d1d-4ff1-9ed2-07f8b8bdbd2b" alt=""><figcaption></figcaption></figure></div>
2. Select the appropriate project type based on the situation. Here we select "Framework-less Solidity Files" and click "Continue".

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FrGQ9SRHHSPGxJadjCDd2%2Fstep2.png?alt=media&#x26;token=f39f6a35-4014-420f-a701-e14e80e170c5" alt=""><figcaption></figcaption></figure>
3. Upload a zip file of the project and click "Continue".

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FQmu30Mt9q6WKA1MhSB0I%2Fstep3.png?alt=media&#x26;token=ce0cf5f8-3c9c-4ffc-ab53-6782c6bf92cb" alt=""><figcaption></figcaption></figure>
4. Input a project name and click "Upload" to upload the project.

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FvO7XONy0QE7sXJZLLKab%2Fstep4.png?alt=media&#x26;token=3724511c-7991-4658-85a1-62982828d309" alt=""><figcaption></figcaption></figure>
5. Configure contract analysis settings and scan. Click "Start Scan" to prepare for scanning.

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FcgsLroh2IXAedjvDqpu9%2Fstep5.png?alt=media&#x26;token=cb1f0d25-5e95-4940-b594-3d3097cda359" alt=""><figcaption></figcaption></figure>
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.

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FjbYs4v8IL8xybn1mrh67%2Fstep6-01.png?alt=media&#x26;token=b9b0480b-536c-4216-8bd0-30e1203279b0" alt=""><figcaption></figcaption></figure>

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2F6Ahwst0fcwRw33cGpPUD%2Fstep6-02.png?alt=media&#x26;token=81c57805-2d31-4b39-b30f-ebf967d5d288" alt=""><figcaption></figcaption></figure>
7. Review key metrics and information from the report.

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FJd6UTh7RBWDvDfuSnY0A%2Fstep7.png?alt=media&#x26;token=b50f96ab-ebec-4421-ae29-3c12526faa98" alt=""><figcaption></figcaption></figure>
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

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FvlgXElIYlr03WjrgTcif%2Fstep8.png?alt=media&#x26;token=37c6b895-f428-4a99-9a50-8f0639aaec33" alt=""><figcaption></figcaption></figure>
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

   <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FuPjzwutWGECN9Yf0QHtl%2Fstep9.png?alt=media&#x26;token=8c8f866f-e6ef-4222-84d1-84e07fa69514" alt=""><figcaption></figcaption></figure>
10. After calling `_balances[sender] = senderAmount.sub(amount);`, `_balances[sender]` becomes 19900

    <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2FzPMDRw0ol2ED0HPSQCb6%2Fstep10.png?alt=media&#x26;token=2c6df682-b56e-4a3b-8a25-1150ea245bea" alt=""><figcaption></figcaption></figure>
11. After calling `_balances[recipient] = recipientAmount.add(amount);`, `_balances[recipient]` becomes 20100

    <figure><img src="https://2103595560-files.gitbook.io/~/files/v0/b/gitbook-x-prod.appspot.com/o/spaces%2FXwKHdN6p38PW7Li7k59G%2Fuploads%2F1zfJJj9cnv5lqC5l6bYb%2Fstep11.png?alt=media&#x26;token=89b5a76d-328e-4e0e-b398-17fa12081c3a" alt=""><figcaption></figcaption></figure>

**Thus the assertion `assert(balanceBefore == balanceAfter);` is finally violated.**<br>