Taming Callbacks for Smart Contract Modularity
summary
Paper claims the first sound semantic static algorithm to ensure callbacks don’t break modular reasoning, and ships ECFChecker that decompiles EVM bytecode, uses an SMT solver and commutativity/projection proofs to construct callback-free equivalent traces. Evaluation on top Ethereum contracts shows most call-containing functions are provably ECF, analysis usually runs <5s but some cases exceed an hour, and remaining outcomes include 18 real ECF violations, 11 false positives and 18 instances lacking source for manual checking.
AI-written summary · about
chapters (14)
- 0:00Taming Callbacks for Smart Contract Modularity
- 0:16Smart Contract Interaction is Complex
- 3:12Callbacks Make Modular Reasoning Difficult
- 4:52ECFChecker vs. Existing Tools (Syntax based) call
- 6:56The property checked by ECFChecker
- 7:36Projection and commutation
- 8:42Trivial ECF inference rules
- 9:28Generalized ECF using movements
- 10:18Reaching a violation of ECF
- 11:40Implementation
- 13:10Experimental results by function
- 13:42Breakdown of violations
- 14:20Running times
- 14:34Summary
related talks
17mModular Verification of Probabilistic Constant-Time
21mPractical Verification Of Smart Contracts Using Memory Splitting
33mSymbolic value-flow static analysis:deep,precise,complete modeling of Ethereum smartcontracts
15mSymbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
21mErays: Reverse Engineering Ethereum's Opaque Smart Contracts
01h 10mHow Context-Sensitive Static Analysis Led to the Best Smart Contract Decompiler
31mElipmoc: advanced decompilation of Ethereum smart contracts
29mCompositional Verification of Smart Contracts Through Communication Abstraction