Exhaustive Symbolic Execution for EVM Bytecode
A dual-backend formal analysis platform proving contract invariants, synthesizing concrete exploits from SMT models, and eliminating path explosion via abstract interpretation.
quickstart.sh
$ git clone https://github.com/KELLERBABG/SymEx-EVM.git
$ cd SymEx-EVM && cargo test --workspace
$ cargo run --bin symex -- scan --target contracts/Vault.bin --solver native-z3
Control Flow Graph & Symbolic Path Exploration
STATUS: SAT (Counter-Example Found)
The execution tree forking at conditional jump `JUMPI [0x04a2]`. The engine models storage slots as uninterpreted arrays and Keccak-256 preimages as collision-resistant algebraic mappings.
BLOCK_00 [0x00..0x45]
CALLDATALOAD(0x04)
CALLVALUE == 0
Path: True
==>
BRANCH [0x04a2]
SLOAD(balances[msg.sender])
amount > balance
ITE Merge Pruning
==>
REENTRANCY SINK
CALL(gas, to, val, ...)
SSTORE(slot, new_bal)
Violation: CE Generated
Solving Path Explosion
Unconstrained symbolic execution suffers from combinatorial explosion on complex loops and cryptographic hashes. SymEx-EVM solves this with three core innovations:
- ITE-Based State Merging: Converging control paths are unified into conditional expressions `(ite cond pathA pathB)`, eliminating duplicate sub-trees.
- Keccak Uninterpreted Functions: `SymbolicHashTable` maps hash outputs back to preimages, bypassing non-linear bitvector expansions in Z3.
- Concolic Fuzzing Seeds: Hybrid concrete execution guides deep exploration, solving path predicates dynamically when branches turn intractable.
Dual Z3 Engine Backend
High-throughput automated reasoning engine supporting both zero-dependency SMT-LIB2 string emission and direct native C-bindings:
| Feature | Native Z3 (C-API) | SMT-LIB2 Fallback |
|---|---|---|
| Solving Latency | 0.4ms / push-pop | 18ms / process pipe |
| Incremental Solving | Yes (context stack) | No (re-instantiated) |
| Memory Footprint | Direct FFI Heap | Buffered Strings |
| Deployment Mode | Linux/macOS x86/ARM | WASM & Embedded |
Built-in Vulnerability Detectors & Taint Sinks
Reentrancy (State Taint)
Detects state updates (`SSTORE`) occurring after external untrusted invocations (`CALL`, `DELEGATECALL`) along feasible paths.
tx.origin Phishing
Flags critical authentication assertions depending on the transaction initiator rather than direct caller (`msg.sender`).
Unchecked Return Values
Symbolic stack audit identifying external calls whose boolean return status is dropped without branch verification.
Post-London Gas Griefing
Models EIP-2929 cold/warm access state and transient storage (EIP-1153) to detect unbounded gas starvation vectors.