SolType: Refinement Types for Arithmetic Overflow in Solidity
summary
SolType adds refinement types to Solidity and Solid implements it, inferring contract invariants to prove arithmetic overflow absence rather than paying per-operation runtime checks. Solid proves overflow safety for 120 contracts and in fully automated mode eliminates 86.3% of redundant checks, averages 41s per contract, and reports a ~20% false positive rate (Auto mode ~25%), beating VeriSmart on false positives and speed. It supports nested mappings with flatten/sum refinement terms and frames inference as a MaxSMT optimization solved by Solid.
AI-written summary · about
chapters (14)
- 0:00SolType introduction
- 1:02Smart contracts in Solidity
- 2:47Manual overflow checks
- 5:37SolType refinement types
- 6:19Proof process with SolType
- 9:48Invariant preservation
- 11:15Invariant inference problem
- 12:40Nested mappings in Solidity
- 14:30SolType implementation
- 15:12Benchmark results
- 17:16Inference impact on accuracy
- 18:18Nested mapping reasoning
- 18:41Conclusion
- 19:04Q&A
related talks
26mSolType: Refinement Types for Arithmetic Overflow in Solidity
29mSynthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
20mSolidity's most common security pitfalls and its best safeguards
25msolx: an LLVM-based Solidity toolchain
19mVarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
19mConsolidating Smart Contracts with Behavioral Contracts
15mCompositional Verification of Smart Contracts Through Communication Abstraction
22mPRBMath: A Modern Smart Contract Library for Fixed-Point Math