Gradual Verification for Smart Contracts
Haojia Sun, Kunal Singh, Jan-Paul Ramos-Dávila, Jonathan Aldrich, Jenna DiVincenzo
TL;DR
Gradual verification addresses the difficulty of verifying smart contracts when interacting with external code and potential re-entrancy vulnerabilities. It blends static verification for known portions with dynamic, run-time checks for partially specified components, using a pyTEAL to Gradual C0 pipeline and the Weaver module to insert checks. The paper contributes a complete architecture, a front-end in PyTEAL, static/dynamic verification integration, and a concrete Algorand prototype, demonstrating soundness and reduced run-time overhead. This approach improves security guarantees in blockchain environments while keeping verification effort manageable for developers.
Abstract
Blockchains facilitate secure resource transactions through smart contracts, yet these digital agreements are prone to vulnerabilities, particularly when interacting with external contracts, leading to substantial monetary losses. Traditional verification techniques fall short in providing comprehensive security assurances, especially against re-entrancy attacks, due to the unavailable implementations of external contracts. This paper introduces an incremental approach: gradual verification. We combine static and dynamic verification techniques to enhance security, guarantee soundness and flexibility, and optimize resource usage in smart contract interactions. By implementing a prototype for gradually verifying Algorand smart contracts via the pyTEAL language, we demonstrate the effectiveness of our approach, contributing to the safe and efficient execution of smart contracts.