DeFinery - Data, Code, and Results

Data, Code, and Results

Experimental Dataset

Our experimental dataset consists of the 9 smart contracts that include 5 real-world DeFi smart contracts and 4 benchmark smart contracts selected from the SmartBugs dataset.

Analyzed smart contracts are available in our GitHub repository.

The contracts/raw folder contains adapted source code of the analyzed smart contracts:
- Confused_Sign adapted from the SmartBugs dataset smart contract using a wrong comparison operator: require(amount >= balances[from]);
- EtherBank adapted from the SmartBugs dataset smart contract prone to reentrancy;
- Refund_NoSub adapted from the SmartBugs dataset smart contract missing a balance update after withdrawal: balances[msg.sender] = 0;
- Unprotected adapted from the SmartBugs dataset smart contract missing an access-control check: require(msg.sender == owner);
- Value adapted from the ValueDeFi: ProfitSharingRewardPool smart contract missing a state variable update initialized = true; which allows smart contract re-initialization;
- cToken adapted from the CreamFi: cToken smart contract prone to reentrancy;
- iToken adapted from the bZx/iToken: LoanTokenLogicStandard smart contract either missing a check on input paramers require(from != to); or using an incorrect order of statements, which allows token duplication;
- xForce adapted from the ForceProfitSharing smart contract missing a check on a return value of a function call require(force.transferFrom(...)); or bool res = force.transferFrom(...); require(res); which allows minting tokens for free;
- Uranium adapted from a modified version of Uniswap2Pair using an incorrect numeral constant in a check: require(balance0Adjusted * balance1Adjusted >= _reserve0 * _reserve1 * 1000**2, 'UniswapV2: K'); which allows buing tokens at an abnormal exchange rate;

We also used a unified implementation for tokens used by the listed DeFi smart contracts (DAI, USDC, Value stakedToken) based on ERC20 and DSToken implementations;

contracts/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).
contracts/patched shows correct patches identified by DeFinery.

Evaluation Results

We ran the experiments on MacOS Monterey v.12.3.1, 32GB RAM and 2 GHz quad-core Intel Core i5 processor. On average, it took DeFinery 53 seconds to analyze and fix the experimental smart contracts. We repeated every experiment 5 times.

Table 1 summarizes the result of running our tool on 9 experimental smart contracts, showing the correct patch found by DeFinery and the property that was used to find and assess the fix. Raw result logs are also available in the repository.

The detailed statistics on processing time (in seconds) for both semantic analysis and patched generation module is shown in the tables below. Sheet 1 shows averaged statistics, while Sheet 2 demonstrates results of each experiment in detail.

NIER DeFinery Evaluation

Prototype Implementation

Docker

We recommend running our tool in a Docker container using the following command:

docker run -it --rm -v YOUR_PATH/experiments:/experiments/ definerysc/definery CONTRACT_NAME

This 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].

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 some smart contracts, more than one correct and conditionally equivalent patch is identified (e.g., for cToken). In this case, the first, simpler, patch is preferable.

DeFinery-SEE Executable

An executable file for our symbolic execution engine, DeFinery-see, can also be downloaded via the following link. 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-eqcheck performs conditional equivalence checking between the file provided as a second argument (e.g., ./contracts/CONTRACT_NAME_patched.sol) and a previously recorded summary of the CONTRACT_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-main execution.
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 /experiments folder 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

Patch Generation Module

The code for our patch generation module based on SCRepair is available in the /SCRepair folder of our repository. The implementation of the patch generation module is a work in progress.

To install the our modified version of SCRepair, use the following command, and the dependencies will be automatically installed and configured:

python3.7 setup.py install

To setup the patch generation component implemented in TypeScript, run the following command:

cd sm && npm install && npm run-script build

To start the patch generation process, use the following command:

python3 CLI.py --targetContractName CONTRACT_NAME repair PATH_TO_CONTRACT

The modified version of SCRepair used in DeFinery relies on DeFinery-see and assumes that semantic analysis results are available in the /experiments/CONTRACT_NAME folder.

Page updated

Google Sites

Report abuse