-
This artifact has been archived at the following permanent location:
-
This repository serves as a submission for the Available and Reusable badges.
This reporitory demonstrates how DeFinery can be used to automatically repair smart contracts that do not satisfy their functional specification. DeFinery takes a user-defined correctness property and a trace leading to its violation as input, based on which it automatically generates a diverse set of patches for a smart contract, while providing formal correctness guarantees w.r.t. the intended behavior. It combines search-based patch generation with semantic analysis of an original program to efficiently navigate the search space and generate higher-quality patches that cannot be obtained by other smart contract repair tools.
This README describes the prerequisites for running DeFinery. In the Quick Start section of the README, we show how to run the pre-built Docker image of DeFinery. It can be used to reproduce the results shown in the paper (Reproducing Experimental Results).
The information on the smart contract dataset used for the evaluation is provided in Experimental Data. More details on the prototype implementation are shown in Prototype Implementation.
The instructions on how to build the tool from scratch are provided separately in the INSTALL.md file.
The repository is structured as follows:
DeFinery
│ DeFinery.pdf
│ README.md
│ INSTALL.md
│ LICENSE.md
│ Dockerfile
| definery-see.zip
│ build.sh
│ start.sh
└───contracts
│ └─── eval/
│ └─── patched/
│ └─── raw/
└───raw_results
│ └─── Confused_Sign/
│ └─── EtherBank/
│ └─── Refund_NoSub/
│ └─── Unprotected/
│ └─── Uranium/
│ └─── Value/
│ └─── cToken/
│ └─── iToken/
│ └─── xForce/
└───SCRepair
│ README.md
│ CLI.py
│ CR.py
│ ETC.py
│ GR.py
│ IN.py
│ Slither.py
│ SolVer.py
│ SolidityM.py
│ StoreKeyValuePairAction.py
│ Utils.py
│ __init__.py
│ __main__.py
│ build.rb
│ requirements.txt
│ setup.py
│ └─── sm/
│ └─── test/
| Files/Dirs | Descriptions |
|---|---|
| DeFinery.pdf | PDF of the accepted paper. |
| README.md | This README file. |
| INSTALL.md | File containing instructions for building and running the tool. |
| build.sh | Script for local installation of the tool. See INSTALL. |
| Dockerfile | File used to make a Docker image. See INSTALL. |
| contracts | Smart contracts used for evaluation. See Experimental Data. |
| raw_results | Raw results of the evaluation discussed in the paper. See Experimental Data. |
| definery-see.zip | An archived binary of a symbolic execution engine used in DeFinery. |
| start.sh | Script running DeFinery on a given smart contract. |
| SCRepair | Implementation of the repair component based on SCRepair. |
A companion website for the paper submission can also be found at: https://sites.google.com/view/ase2022-definery/.
We use Docker 20.10.14 that can be obtained from the Docker website.
DeFinery also uses Python 3.7 and Node v14.20.0.
The scripts included in this repository have been tested on Ubuntu 18:04. The binary of a symbolic execution component (definery-see.zip) is also built for Linux-AMD64 (Ubuntu 18.04).
The easiest way to run DeFinery is by a public Docker image using the following command:
docker run -it --rm -v YOUR_PATH/experiments:/experiments/ definerysc/definery CONTRACT_NAME
The command will pull the Docker container and execute both symbolic analysis and patch generation for a given smart contract, which can be one of the following: [xForce, iToken, cToken, Value, Uranium, Unprotected, Refund_NoSub, Confused_Sign, EtherBank]. Please make sure that YOUR_PATH is an absolute path—YOUR_PATH/experiments:/experiments/ mounts a local folder (YOUR_PATH/experiments) to the Docker container to facilitate the exploration of patched smart contracts—you can, then, view the results produced by the tool in this folder.
Running this command will add files produced by symbolic engine and patch generator into the YOUR_PATH/experiments/CONTRACT_NAME folder. The patched folder contains plausible patches that pass the test cases generated by our tool. Once at least one of the patches passes conditional equivalence checking, you will see the following text pointing to the location of a correct patch in a /patched folder:
The valid implementation is EQUIVALENT: /experiments/CONTRACT_NAME/patched/patched_0.sol
For example, you can run the following command to repair the xForce smart contract:
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery xForce
The tool will, first, start the symbolic analysis of the given smart contract:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
dumping contract information:
Contract: _MAIN_
Constructor: _MAIN_()
State Variables:
force
$var_0
$var_1
user
xforce
Modifiers:
Functions:
_MAIN_:::function ()
_MAIN_::declare_property:function (bool)
...
The result of the analysis will be saved in the ~/Desktop/experiments/xForce folder to be reused during repair, after which the repair process will start:
result context [1]:
Is possibly reentrant: 0
RESULT: 0
The trace is INVALID
$var_0 = 0
$var_1 = 97
result context [2]:
Is possibly reentrant: 0
RESULT: 1
The trace is VALID
$var_0 = 2
$var_1 = 2
Recording summary, validCount: 1
Summary file is /experiments/xForce/summary.txt
[2022-08-04 10:22:25.762851] INFO: CLI: Start repairing problems
The repair component will output the information on the patch searching process, such as identified plausible patches, fitness values for the evaluated generation, etc. Once the valid (equivalent) patch is identified, it will show the name of the repaired smart contract located in the ~/Desktop/experiments/xForce/patched/ folder.
fitness values
----------------------------------------------------------------------------
gen evals min max op #targetedVuls #targetedVuls(detailed)vuls-best-patch(max: 3)
0 11 {'hard': '(-1.0,)', 'soft': '(1.0,)'} {'hard': '(0.0,)', 'soft': '(1.0,)'} init (0, 0, 0, 1, 1, 0, 1, 0, 1, 0, 1)
plausible-last-gen 6 {'hard': '(0.0,)', 'soft': '(2.0,)'} {'hard': '(0.0,)', 'soft': '(1.0,)'} init (0, 0, 0, 0, 0, 0)
[2022-08-04 10:22:41.192624] INFO: CR.py: Plausible patches details:
...
[2022-08-04 10:22:41.192737] INFO: CR.py: Evaluated 10 patches
Testing equivalence... 0
Testing equivalence... 1
The valid implementation is EQUIVALENT: /experiments/xForce/patched/patched_1.sol
Testing equivalence... 2
Testing equivalence... 3
Testing equivalence... 4
Testing equivalence... 5
If you inspect the generated file, you will notice that the fix require(res); is now included in the deposit() function of the xForce smart contract:
-> % cat ~/Desktop/experiments/xForce/patched/patched_1.sol
...
function deposit(uint256 amount) external {
// Gets the amount of Force locked in the contract
uint256 totalForce;
totalForce = force.balanceOf(address(this));
// Gets the amount of xForce in existence
uint256 totalShares = totalSupply;
// If no xForce exists, mint it 1:1 to the amount put in
if (totalShares == 0 || totalForce == 0) {
_mint(msg.sender, amount);
} else {
uint256 what = (amount * totalShares) / totalForce;
_mint(msg.sender, what);
}
// Lock the Force in the contract; Missing check on return value of transferFrom();
bool res;
res = force.transferFrom(msg.sender, address(this), amount);
require(res);
}
The instructions for building the tool from the source code contained in this repo are described in the INSTALL.md file.
To reproduce the results of the evaluation shown in the paper using Docker, you may simply repeat the process described above for the 9 smart contracts used in the experiments: xForce, iToken, cToken, Value, Uranium, Unprotected, Refund_NoSub, Confused_Sign, EtherBank.
Please note that while most of the smart contracts are usually repaired in under 1 minute, Uranium may take several minutes to be processed (due to the non-linear arithemtic expressions used in a smart contract, which SMT solvers struggle with). For the cToken, two correct and conditionally equivalent patches are identified—in this case, the first, simpler, patch is preferable.
The commands to be run would look as follows:
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery Confused_Sign
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery xForce
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery Unprotected
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery cToken
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery iToken
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery Value
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery Refund_NoSub
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery EtherBank
docker run -it --rm -v ~/Desktop/experiments:/experiments/ definerysc/definery Uranium
The output of the tool will suggest the name of the valid (equivalent) patch for the contract, which will be located in, e.g. ~/Deskop/experiments/CONTRACT_NAME/patched/ folder.
We evaluated our tool on a dataset of 9 smart contracts that include 5 real-world DeFi smart contracts and 4 benchmark smart contracts selected from the SmartBugs dataset. The analyzed smart contracts are available in the /contracts folder. The /raw folder contains adapted source code of the analyzed smart contracts, while /eval contains files that were symbolically analyzed, i.e., they include analyzed smart contract code, the Main contract encoding the harness function for symbolic analysis, and supplementary code (e.g., User smart contracts).
/raw_results reports raw experimental data for running our tool on our dataset. On average, it tool DeFinery 53 seconds to analyze and fix a smart contract. We provide more detailed statistics on our website.
The code for the patch generation module based on SCRepair is available in the /code/SCRepair folder with the installation instructions. The implementation of the patch generation module is a work in progress.
Our modified version of SCRepair relies on our symbolic engine, DeFinery-see, the binary for which is available for download, and assumes that semantic analysis results are available in the /experiments/CONTRACT_NAME folder. The binary is built for Linux-AMD64 (Ubuntu 18.04). It takes 3 arguments:
- Execution mode:
-symexe-main(symbolically executes the harness function and records the results in the/experiments/CONTRACT_NAME/folder;-symexe-check(symbolically executes the harness function but does not save resulting files);-symexe-eqcheckperforms conditional equivalence checking between the file provided as a second argument (e.g.,./contracts/CONTRACT_NAME_patched.sol) and a previously recorded summary of theCONTRACT_NAME. The summary of the original smart contract is to be available at./experiments/CONTRACT_NAME/, therefore the invokation in this mode should be preceded by a-symexe-mainexecution. - The path to a smart contract or a file with several smart contracts to be analyzed, e.g.,
/contracts/CONTRACT_NAME.sol. This file has to be located in the /contracts folder. There should also be an/experimentsfolder to store the results. - The name of a vulnerable smart contract to be repaired:
CONTRACT_NAME
./definery-see -symexe-main ./contracts/CONTRACT_NAME.sol CONTRACT_NAME