whbjzzwjxq/Foray

Foray

Attack Synthesis for DeFi Apps

Initial Benchmark Collection

We use DeFiHackLabs as the benchmark records.

Setup by command line (If you are using a Macbook)

Install python 3.11.

brew install python@3.11

Install dependencies.

pip3 install -q --upgrade pip && pip3 install -q -r ./requirements.txt && \
solc-select install 0.8.21 && solc-select use 0.8.21 && npm install --quiet --save-dev

Install Foundry 0.2.0.

curl -L https://foundry.paradigm.xyz | bash

Evaluation

Foray eval

This command will evaluate all sketches of a benchmark.

python3 ./main.py -e -i ./benchmarks/Discover

Ablation study

python3 ./main.py -e --fixed -i ./benchmarks/Discover

Forge eval

This test is for testing whether the ground truth works or not.

forge test -vvv --match-path ./benchmarks/Discover/Discover.t.sol

Halmos eval

This command will evaluate all sketches of a benchmark.

python3 ./main.py -ha -i ./benchmarks/Discover

(It works with cached results and if you don't want to cache, run rm ./benchmarks/Discover/result/*.json)

Use anvil

anvil --no-mining --timestamp 0 --base-fee 0 --gas-price 0

Citations

This work is accepted by ACM CCS '24. Link

Tips

Halmos cache

Halmos will use the same cache directory as foundry.toml.

Supported cheating codes: Check this file

Prepare code (We have already prepared it for you, no need to re-run it)

python3 ./main.py -p -i ./benchmarks/Discover
python3 ./main.py -p -i all

Clean result

rm ./benchmarks/**/result/eurus_*.json
rm ./benchmarks/**/result/record.json