Consolidating Smart Contracts with Behavioral Contracts
summary
ConSol extends Solidity with a transpiler that attaches behavioral contracts to first-class addresses by expanding 160-bit addresses into a guarded address representation that encodes pre/postconditions; calls decode and dispatch checks at invocation. The prototype minimizes storage changes, reifies address specs, and extracts repeated low-level checks into separate specs, cutting about half the local assertion lines in evaluated functions. Tested on ~20 real-world cases and benchmarks, it blocks known attacks and adds only about 0.2% gas overhead.
AI-written summary · about
chapters (16)
- 0:00Talk introduction
- 0:42Smart contracts
- 2:05Bugs and losses in contracts
- 3:08Behavioral contracts
- 3:48Consol: Extending Solidity
- 4:51Behavioral contract annotations example
- 6:16Address arguments challenges
- 7:19Higher-order functions checks
- 8:01Decoupling security from logic
- 9:26Tracking addresses costs
- 11:13Gas overhead in EVM
- 13:03Expressiveness vs real attacks
- 14:27Simplifying security checks
- 15:08Gas overhead benchmarks
- 16:54Consol summary and benefits
- 17:37Q&A: Dynamic vs static checks
related talks
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
25mBehavioral simulation for smart contracts
01h 25mSpeculation in Smart Contracts
26mSolType: Refinement Types for Arithmetic Overflow in Solidity
21mPractical Verification Of Smart Contracts Using Memory Splitting
21mSolType: Refinement Types for Arithmetic Overflow in Solidity
05mBonsol, ZK Plumbing on Solana
17mSmartCon Developer Keynote