Practical Verification Of Smart Contracts Using Memory Splitting
summary
The paper implements a conservative memory analysis and a memory-splitting transformation for EVM bytecode, integrated into CertoraProver, that recovers allocations by SSA incarnation numbers and a definite-write property to ensure reads of the free pointer map to disjoint abstract locations. Rewriting the monolithic byte-array into per-object regions reduces branches in SMT queries and yields up to a 120x speedup on some tasks and 16 timeouts mitigated across 229 real-world verification benchmarks.
AI-written summary · about
chapters (11)
- 0:00Smart contract verification intro
- 1:24Introducing Cur prover tool
- 2:30EVM memory layout
- 5:24SMT solver memory challenges
- 7:32Allocation analysis design
- 10:01Definite write property
- 12:49Related work and paper
- 13:10Memory splitting transformation
- 14:13Verification performance evaluation
- 15:37Compiler bug discoveries
- 16:25Q&A
related talks
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
29mCompositional Verification of Smart Contracts Through Communication Abstraction
15mCompositional Verification of Smart Contracts Through Communication Abstraction
28mMemory simulations, security and optimization in a verified compiler
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
14mRich Specifications for Ethereum Smart Contract Verification
28mProving Memory Access Violations in Isabelle/HOL