You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
feat(evm): symbolic-assist worker (concolic-lite v1) for coverage-guided fuzzing
Adds a directed-mutation worker that periodically replays a corpus seed under a
branch-trace inspector, finds the deepest unseen opposite-side branch ("frontier"),
and proposes ABI-aware calldata rewrites that flip the branch — without invoking
an SMT solver. Inspired by Echidna's Echidna.SymExec.Exploration and the
SaferMaker writeup (https://hackmd.io/@SaferMaker/EVM-Sym-Exec).
Architecture:
- BranchTraceInspector (crates/evm/evm/src/inspectors/branch_trace.rs):
observation-only REVM Inspector that records every JUMPI together with the
immediately-preceding compare opcode (EQ/LT/GT/SLT/SGT/ISZERO) and its
concrete operands. Uses the same edge-id hashing as EdgeCovInspector so
frontier ids can be looked up directly in the corpus history map.
- crates/evm/evm/src/executors/symexec/:
- types.rs: FrontierKey, FrontierStats, SymExecState, Candidate, hard caps.
- select.rs: seed scoring (favored > productive > shorter), deepest
unseen-frontier picker, attempt bookkeeping.
- mutate.rs: ABI-aware Redqueen-style calldata rewrites for scalar args
(uintN/intN/bool/address/bytesN). Skips dynamic types in v1.
- mod.rs: SymBackend trait + HeuristicAbiRewrite v1 backend +
run_symexec_assist top-level loop. Trait stays in place so v2 can swap in
z3/hevm/halmos without changing the loop.
- WorkerCorpus helpers: is_master, symexec_seed_pool, history_map_snapshot,
master_sync_dir, symexec_validate. The validator clones the executor and
history map and only reports new edges; it never mutates the live history
map, so the next calibrate() picks up the persisted file in the normal way
without poisoning the corpus.
- Config: FuzzCorpusConfig.symexec_assist (bool, default false) +
symexec_assist_interval (u32, default 200) + symexec_assist_active() guard
(requires coverage-guided + EVM edge coverage; sancov-edges disables it).
- Wiring:
- executors/fuzz/mod.rs: master worker only, periodic call after each sync,
stateful = false.
- executors/invariant/mod.rs: single worker, periodic call at the top of the
run loop, stateful = true (commits prefix txs during replay/validation,
resolves the final tx's ABI dynamically via FuzzRunIdentifiedContracts.
- Inspector plumbing: branch_trace propagates through InspectorStack ->
InspectorData -> RawCallResult.branch_trace (mirrors the existing
edge_coverage path).
Validation gate ensures only candidates that produce a real new EVM edge are
persisted to <corpus_dir>/worker0/sync/, where the existing corpus protocol
distributes them to other workers.
Hard CPU budget per cycle: 1 seed, 1 frontier, <=8 candidates, max 3 attempts
per frontier per campaign.
Tests:
- forge cli: symexec_assist_solves_equality_guard (stateless fuzz) — handler
with require(x == MAGIC) where MAGIC is a 32-byte distinctive value;
asserts the corpus directory contains the magic bytes after the run.
- forge cli: symexec_assist_solves_equality_guard_invariant (stateful
invariant) — same handler exposed via targetContract; trivial invariant;
same structural corpus check.
All existing tests still pass:
forge cli fuzz tests: 16 passed (incl. new regression)
forge cli invariant tests: 68 passed (incl. new regression)
foundry-evm lib tests: 21 passed
foundry-config lib tests: 154 passed
Future extensions kept open by the SymBackend trait:
- Z3PathFlip backend (real SMT)
- ExternalHevm / ExternalHalmos backends
- Mutating the final-tx sender for access-control branches
EOF
)
Amp-Thread-ID: https://ampcode.com/threads/T-019e2bc9-ece8-718f-9279-971e3e982bec
Co-authored-by: Amp <amp@ampcode.com>
0 commit comments