# dataset-for-mcVer

**Repository Path**: zyzyzyzyzy12345/dataset-for-mcVer

## Basic Information

- **Project Name**: dataset-for-mcVer
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 1
- **Created**: 2022-04-26
- **Last Updated**: 2022-04-26

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# mcVer

**mcVer** is a verification tool for smart contracts written in Solidity. Based on model checking tool [VERDS](http://lcs.ios.ac.cn/~zwh/verds/), the mcVer framework is able to not only check some typical security vulnerabilities, but also verify a variety of properties of smart contracts.

## content

The project includes the dataset for  **mcVer: A Model Checking Based Framework for Smart Contract Verification**. The contents contained in each folder are explained as follows：

- vvmEx
  
  - In this folder, the vvm (vvmEx.vvm ) code of the example for illustrating the composition of VML are included.
- aucEx
  - 
  - the solidity source code( [aucEx.sol](https://solidity-cn.readthedocs.io/zh/develop/solidity-by-example.html) ),  property definition( p.txt ), scenario configuration( m.txt ) of the running example for the manuscript are included.
  - output of verification of the above configuration:  aucEx.vvm (VERDS model generated by **mcVer**), output_aucPr1.txt (output of verification of pr1), output_aucPr2.txt (output of verification of pr2), counterExample_aucPr2.html (counter example generated when verification of pr2)
- Security
  - 
  - todSC: dataset for TOD Vulnerability checking.
  - aucExdos: dataset for DoS Vulnerability checking.
  - ICON:  dataset for Modifier Vulnerability checking.
  - reSC:  dataset for Reentrancy Vulnerability checking.
  
- AccessControl
  -
  - Dataset for Access Control contract, including three scenarios (snr1.txt, snr2.txt, snr3.txt) and related properties (snr*_pr*.txt). Corresponding outputs are subfixed with snr*[_pr*].
    
- verds
  -  
  - In this folder, the model checking tool VERDS is included. The running environment should be Linux or CentOS.

  - It can be used to verify corresponding properties as follows( /verds/verds should be given the permission to execute ):

    ```bash
    ./verds/verds -ck 1 /aucEx/aucEx.vvm
    ```

  - When the contract does not meet the property, an execution trace will be generated by VERDS in current folder, such as  /runningExample/runningExample.cex

## Quick Start

1. **Original Solidity Code**

   Below is an example source code for the contract **aucEx.sol**

   ```solidity
    pragma solidity ^0.4.22;
    contract Auction{
        address public beneficiary;
        address public highestBidder;
        uint public highestBid;
        bool ended;
        constructor(address _beneficiary) public {
            beneficiary = _beneficiary;
        }
        function bid() public payable{
            require(!ended);
            require(msg.value > highestBid);
            if (highestBid!=0 ) {
                require(highestBidder.send(highestBid));
            }
            highestBidder = msg.sender;
            highestBid = msg.value;
        }
        function auctionEnd() public{
            require(!ended);
            ended = true;
            beneficiary.transfer(highestBid);
        }
    }
   ```

2. **Set the scenario**

   For aucEx, we set  a scenario describe that three bidders bid at the same time, it can be described in SDL (m.txt) as follows:

   ```solidity
   p0:constructor(1,0,1)
   p1:bid(2,2)|p2:bid(3,3)|p3:bid(4,4)
   p4:auctionEnd(1,0)
   ```
 

3. **Set the property to be verified**

   Under above defined  scenario, the property that the winner is always the bidder who gives the highest bid is described in CTL (p.txt) as follows:

   ```solidity
   AG (!End | highestBidder=4)
   ```
   Here End indicates the end of the scenario.
   
4. **Translate to VVM**

   **mcVer** translates the solidity contract (aucEx.sol), the scenario (m.txt) and the property (p.txt) into a VVM, aucEx.vvm.
 

5. **Verification**

   Finally, we need to verify the vvm file using VERDS. For the aucEx.vvm, we can verify the *i*<sup>th</sup>  property as follow:

   ```bash
   ./verds/verds -ck i /aucEx/aucEx.vvm
   ```

   The verification of the second property (AG(!(order=3)|(highestbidder=4))) is false. In this case, an  execution trace, named aucEx_aucPr2.cex is generated by VERDS. It shows the traces of a counterexample.

   The Solidity level counter example (counterExample_aucPr2.html) is then extracted from aucEx_aucPr2.cex.