English · 简体中文
Reverse Engineer · EVM Security · Program Analysis
Rust EVM Symbolic Execution Reproducible Analysis
I'm ethever, a reverse engineer focused on Ethereum Virtual Machine (EVM) security and program analysis. I build Rust tooling to understand what smart contracts actually do — from bytecode and execution traces to state-dependent behavior, especially when source code or reliable contract metadata is unavailable.
My work brings together bytecode analysis, symbolic execution, and on-chain state. I care about both the reasoning behind a finding and the execution context needed to reproduce it.
Understand the behavior. Make the assumptions explicit. Reproduce the result.
| Area | Questions I work on |
|---|---|
| Bytecode → semantics | Recovering control flow, intermediate representations (IR), and contract behavior without source code. |
| Paths → constraints | Combining symbolic and concrete execution, satisfiability modulo theories (SMT) solving, and concrete replay. |
| Tokens → state changes | Understanding ERC-20 transfer fees, mint/burn behavior, permissions, and state-dependent rules. |
| State → security | Analyzing DeFi interactions, cross-contract execution, and behavior against a specified chain state. |
I am working toward practical bytecode-level security analysis: preserving execution context, checking findings with concrete replay, and balancing exploration coverage with computational cost.
bytecode + chain state
↓
execution & analysis
↓
inspectable behavior + reproducible traces
| Layer | Tools |
|---|---|
| Implementation | Rust · Solidity · Linux |
| Execution & analysis | Z3 · Foundry · Reth |
| Rules & data | Datalog / Soufflé · DuckDB · Parquet |
| Reproducibility | Nix · Git |
- Explicit assumptions. State what the analysis models and what it leaves out.
- Evidence before claims. Separate observed behavior, modeled behavior, and hypotheses.
- Reproducible results. Keep execution context and evaluate both coverage and computational cost.
Bytecode first. Behavior matters. Evidence over assumptions.