While smart contracts have the potential to revolutionize many important applications like banking, trade, and supply-chain, their reliable deployment begs for rigorous formal verification. Since most smart contracts are not annotated with formal specifications, general verification of functional properties is impeded.
In this work, we propose an automated approach to verify unannotated smart contracts against specifications ascribed to a few manually-annotated contracts. In particular, we propose a notion of behavioral refinement, which implies inheritance of functional properties. Furthermore, we propose an automated approach to inductive proof, by synthesizing simulation relations on the states of related contracts. Empirically, we demonstrate that behavioral simulations can be synthesized automatically for several ubiquitous classes like tokens, auctions, and escrow, thus enabling the verification of unannotated contracts against functional specifications.
Sat 10 DecDisplayed time zone: Auckland, Wellington change
15:30 - 17:00 | PLDI PapersCOVID Time Papers In Person at Seminar Room LG004 Chair(s): Jonathan Aldrich Carnegie Mellon University | ||
15:30 30mTalk | Behavioral simulation for smart contracts COVID Time Papers In Person Sidi Mohamed Beillahi University of Toronto, Gabriela Ciocarlie University of Texas at San Antonio, Michael Emmi Amazon Web Services, Constantin Enea Ecole Polytechnique / LIX / CNRS Link to publication DOI | ||
16:00 30mTalk | Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities COVID Time Papers In Person Lexi Brent International Computer Science Institute, USA / University of Sydney, Australia, Neville Grech University of Malta, Sifis Lagouvardos University of Athens, Bernhard Scholz The University of Sydney, Yannis Smaragdakis University of Athens Link to publication DOI | ||
16:30 30mTalk | Practical Smart Contract Sharding with Ownership and Commutativity Analysis COVID Time Papers In Person George Pîrlea National University of Singapore, Singapore, Amrit Kumar Zilliqa Research, Ilya Sergey National University of Singapore Link to publication DOI |