Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
summary
SmartACE is an automated pipeline that translates Solidity + Scribble specs to an LLVM harness and applies parametrized verification via local bundle abstractions to reduce 2^160 addresses to a few representative users. It plugs into existing analyzers (Seahorn for model checking, libfizzy for fuzzing, CLEA for symbolic execution), verifies OpenZeppelin Ownable and Escrow, uses fault injection to find bugs, and shows that without parametrization analysis times explode (works at 5 users, times out by 500).
AI-written summary · about
chapters (19)
- 0:00Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
- 0:31Motivation and Background: The Problem of Smart Contract Verification
- 0:43Motivation: What is a smart contract
- 2:37Motivation Examples of Smart Contracts
- 3:42Motivation Trust via Source Code Verification
- 5:03Notation: States and Traces
- 7:27Challenges: Current Solutions
- 11:10Program Analysis in SmartACE: Architecture and Techniques
- 13:24Conversion: Source-to-Source Translation Pipeline
- 13:53Conversion: Participation Analysis
- 15:11Conversion: Mapping Representation
- 17:33Conversion: Execution Model Homess Design
- 18:42Limitations Unsupported Features and Future Work
- 20:46Case Studies
- 21:24Properties: Specifications in Scribble
- 22:03Properties: Universal Map Quantifiers
- 22:52Properties: Aggregate Properties
- 23:48Properties: Max Aggregation
- 24:24Results: Performance
related talks
46mFormal verification of C# smart contracts
21mPractical Verification Of Smart Contracts Using Memory Splitting
25mBehavioral simulation for smart contracts
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
37mAuthoring and Formal Verification of Smart Contracts in Pact
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
31mAccount Abstraction Panel
19mConsolidating Smart Contracts with Behavioral Contracts