SolType: Refinement Types for Arithmetic Overflow in Solidity
summary
SolType is a refinement-type system for Solidity with an implementation called Solid that translates contracts to a miniSol SSA IR, encodes overflow checks as soft max-CHC-style constraints, and runs a greedy inference to synthesize contract invariants. It reasons about sums of complex mappings by flatten/compose terms, proves overflow safety across 120 real contracts, eliminates 86.3% of redundant runtime checks in automated mode, reports a 20.4% false positive rate (vs higher baseline) and averages ~41s per contract.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:28Outline
- 0:40Smart Contracts
- 1:25Solidity
- 1:58SafeMath
- 2:46Overflow Safety
- 4:39SolType
- 11:13Type Inference
- 13:01Complex Mappings
- 13:57Summary
- 15:26Solid
- 16:04Evaluation
- 17:27Conclusion
- 18:07Disabling sums
- 18:32Conclusions
- 19:01Audience Questions
- 21:03Online Audience Question
related talks
21mSolType: Refinement Types for Arithmetic Overflow in Solidity
29mSynthesis-Powered Optimization of Smart Contracts via Data Type Refactoring
25msolx: an LLVM-based Solidity toolchain
19mConsolidating Smart Contracts with Behavioral Contracts
20mSolidity's most common security pitfalls and its best safeguards
38mIntroducing Core Solidity
19mVarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
01h 00mint != safe && int != ℤ