Constructing Trustworthy Smart Contracts
summary
ASP is a new contract language plus a proof checker and a defensive compiler that guarantees absence of common bugs like overflow and reentrancy, compiles to Solidity with runtime checks that revert on violations, and preserves verified safety and reachability claims by language inclusion. Key features are an abstract coin type (value, move, move_all), nondeterministic timers used in well‑founded rank proofs (auction and vending examples), verification via Viper, and an open‑source toolchain; the talk cites ~$2B lost to exploits in 2023.
AI-written summary · about
chapters (13)
- 0:00Trustworthy smart contracts
- 1:03Blockchain and smart contracts
- 3:54Smart contract verification challenges
- 4:57ASP language for contracts
- 6:02ASP abstract types
- 8:51ASP timer and state machine
- 10:57ASP message and coin types
- 12:45Proof checker for safety
- 15:33Reachability with timers
- 18:19Adversarial lockouts
- 19:21ASP to Solidity
- 21:07ASP future
- 22:31Q&A
related talks
46mFormal verification of C# smart contracts
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
38mThe Duality of Smart Contracts and Electronic Rights
15mCompositional Verification of Smart Contracts Through Communication Abstraction
04mInterview
40mWeb Apps vs Blockchain DApps (Smart Contracts): Tools, Vulns And Standards
41mBattle of the Languages
01h 13mHardware-Software Contracts for High Assurance with Applications to Side-Channel Security