SKANF

What it is

SKANF ships as a Docker image (dockerofsyang/skanf:latest) with a two-phase pipeline: a detection phase that reports attacker-reachable sensitive external calls, and an exploit phase that synthesizes and replays calldata. This document covers what the summary omits — how to actually run it, the two analysis modes, and its hard dependency on an Ethereum RPC endpoint.

How it works

The detection phase reads a deployed contract's bytecode fetched over JSON-RPC and emits a JSON file listing verified and unverified vulnerable calls. The exploit generator then reads output_eval_baseline.json, walks the verified array, symbolically generates calldata satisfying each call's preconditions, and replays it against a forked EVM to confirm balance changes. Successful exploits land in Exploits/<contract>.<block>.json.

Two modes exist: eval_baseline (pure symbolic) and eval_concolic (seeded symbolic, where the seed comes from a historical transaction via --hash).

Preconditions

• A reachable Ethereum JSON-RPC endpoint. WEB3_PROVIDER must be set; if unset or unreachable, SKANF raises a RuntimeError at startup naming the offending URL. An archive node is recommended for analyses at older blocks; Tenderly's free plan suffices for basic testing.
• Source build needs custom forks of greed and Gigahorse installed first (their setup.sh handles the toolchain), then pip install -r requirements.txt. The Dockerfile provisions Ubuntu 20.04, Miniconda + Python 3.10, Soufflé 2.4, and clones the greed-skanf fork at build time.

What to do

Pull and enter the container:

docker pull dockerofsyang/skanf:latest
export WEB3_PROVIDER="https://ethereum-mainnet.gateway.tenderly.co/<YOUR_TENDERLY_NODE_ACCESS_KEY>"
export NETWORK=ETH
export SKANF_IMAGE=dockerofsyang/skanf:latest
docker run --rm -it --network host \
  -e WEB3_PROVIDER="$WEB3_PROVIDER" \
  -e NETWORK="$NETWORK" \
  "$SKANF_IMAGE" \
  bash

Run the detection phase in either mode:

# Pure symbolic, baseline output filename
python3 main.py --address 0xABC... --block 20000000 --mode eval_baseline

# Seeded symbolic, seed from a historical transaction
python3 main.py --address 0xABC... --block 20000000 \
  --hash 0xdef... --mode eval_concolic

--network host is Linux-only and needed only when the container must reach an RPC node on localhost:8545. On macOS/Windows, omit it and pass a remote RPC URL. See quickstart.md for on-disk layout and the schema of every output file.

Caveats

Detection output separates verified from unverified calls; the exploit phase only acts on the verified array, so unverified findings are not auto-confirmed. Confirmation is empirical — it depends on observing balance changes against a forked EVM at the specified block.