EVM bytecode disassembler with control flow graph construction using abstract interpretation and weakest precondition analysis, following the thesis . The generated CFG is used for static analysis of bytecode to detect vulnerabilites like Reentrancy.
- Bytecode Disassembly: Parse raw EVM bytecode into human-readable instructions.
- Abstract Interpretation: Track stack contents to determine dynamic JUMP targets.
- Weakest Precondition Analysis: Detects loops using semantically sound criteria, with invariant detection.
- CFG Construction: Build precise cfg.
- Minimize CFG: Minimize CFG using the equivalence of state automata.
- Reentrancy detection: CFG-based vulnerability analysis for reentrancy patterns.
- CALL followed by SSTORE on reachable path.
- State changes after delegatecall.
- Detects lock/unlock patterns with reentrancy guards.
- DOT Export: Graphviz visualizations.
- For cfg and disassembly:
python main.py 60015415601057600080fd5b600160015560006000600060006000335af16000600055600060015500- For reentrancy analysis along wih disassembly and cfg:
python main.py -r 60015415601057600080fd5b600160015560006000600060006000335af16000600055600060015500
