Embedded Files
Dataset
Dataset
The smart contract dataset used for the evaluation is available in the /dataset folder in our GitHub repository.
We evaluated SolSEE and other source-level tools for Solidity on 10 smart contracts: the running example used to illustrate the paper (OwnedToken.sol) and 9 smart contracts that expose advanced features of Solidity:
MultipleModifiers.sol contains a function with two modifiers, one of which has two _; statements
FallbackFunction.sol implements a low-level Ether transfer function call .call.value()() and a fallback function that is invoked by this call
GetterFunction.sol calls an automatically-generated getter function a() of a public state variable uint a
SafeMathLibrary.sol uses SafeMath library functions for arithmetic operations on uint variables
MultipleInheritance.sol tests whether the tool implements the C3 linearization rule to decide the order of method invocations in presence of multiple inheritance
Structs.sol performs arithmetic operations on a variable of type struct
NewBytesArray.sol contains structs, multi-dimensional mappings, and the definition of a bytes32[] memory array using new keyword
UintOverflow.sol checks whether overflow semantics is properly implemented for variables of type uint8
Revert.sol contains a function call that gets reverted and checks whether the tool can handle revert() and still analyze the target assert() statement containing the property
As can seen in Table 1, VeriSmart and SMTChecker can correctly process smart contracts only in the absence of external function calls, i.e., if all the functionality is stored in a single smart contract. To test these tools, where possible, we have defined a single-contract version of an experimental smart contract file: MultipleModifiers-SingleContract.sol, GetterFunction-SingleContract.sol, SafeMathLibrary-SingleContract.sol, MultipleInheritance-SingleContract.sol, NewBytesArray-SingleContract.sol, Revert-SingleContract.sol.
To enable analysis by SMTChecker, a smart contract should contain pragma experimental SMTChecker;. Smart contracts with this pragma can we found in the /dataset/SMTChecker folder in our repository.
Evaluation
Evaluation
The executable of SolSEE can be obtained and run through the following Docker container:
docker pull liuyedocker/solsee:latest
To run the tool on a smart contract, e.g., Revert.sol, perform the following command:
docker run liuyedocker/solsee:latest solver -symexe-main ./Revert.sol
The tools we compare SolSEE with include solc-verify, VeriSol v0.1.5 and its modified version used in SmartPulse (denoted as VeriSol-SP in Table 1), VeriSmart, and SMTChecker that is included in solc v.0.5.11. All of these tools claim that they can identify assertion failures, which is the capability we perform the evaluation on. We could not compare with ExGen due to compilation issues. ESBMC-Solidity could not process smart contracts even from their own documentation; thus, we do not compare with it as well.
The raw evaluation logs can be found in the /logs folder of our repository.
The details of the evaluation and tool comparison can also be seen in Table 1.
Table 1. Evaluation results
In VeriSol/VeriSol-SP and solc-verify, the modular arithmetic mode that is required for precise handling of arithmetic overflow can be enabled using flags /useModularArithmetic and --arithmetic mod, respectively.
Page updated
Google Sites
Report abuse