SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 15:30 - 16:00 at Seminar Room LG004 - PLDI Papers Chair(s): Jonathan Aldrich

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 Dec

Displayed 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
30m
Talk
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
30m
Talk
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
30m
Talk
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