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: \textit{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.
(2311.13351.pdf) | 464KiB |
slides (POPL PriSC 2024_Gradual Verification for Smart Contracts.pdf) | 792KiB |
Sat 20 JanDisplayed time zone: London change
16:00 - 17:30 | |||
16:00 22mTalk | Computational-Bounded Robust Compilation and Universally Composable Security PriSC Robert Künnemann CISPA Helmholtz Center for Information Security, Ethan Cecchetti University of Wisconsin-Madison File Attached | ||
16:22 22mTalk | Gradual Verification for Smart Contracts PriSC Haojia Sun Shanghai Jiao Tong University, Kunal Singh Carnegie Mellon University, Jan-Paul Ramos-Davila Cornell University, Jonathan Aldrich Carnegie Mellon University, Jenna DiVincenzo (Wise) Purdue University File Attached | ||
16:45 22mTalk | Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation PriSC File Attached | ||
17:07 8mDay closing | Closing Remarks PriSC Shweta Shinde ETH Zurich |