Verified Development and Deployment of Multiple Interacting Smart Contracts with VeriSolid

May 2020·
Keerthi Nelaturu
,
Anastasia Mavridou
,
Andreas Veneris
Aron Laszka
Aron Laszka
Abstract
Smart contracts enable the creation of decentralized applications which often handle assets of large value. These decentralized applications are frequently built on multiple interacting contracts. While the underlying platform ensures the correctness of smart contract execution, today developers continue struggling to create functionally correct contracts, as evidenced by a number of security incidents in the recent past. Even though these incidents often exploit contract interaction, prior work on smart contract verification, vulnerability discovery, and secure development typically considers only individual contracts. This paper proposes an approach for the correct-by-design development and deployment of multiple interacting smart contracts by introducing a graphical notation (called deployment diagrams) for specifying possible interactions between contract types. Based on this notation, it later presents a framework for the automated verification, generation, and deployment of interacting contracts that conform to a deployment diagram. As an added benefit, the proposed framework provides a clear separation of concerns between the internal contract behavior and contract interaction, which allows one to compositionally model and analyze systems of interacting smart contracts efficiently.
Type
Venue
2nd IEEE International Conference on Blockchain and Cryptocurrency (ICBC 2020), 1–9
publications

Acceptance Rate: 22%

Authors

Aron Laszka
Associate Professor

Aron Laszka is an Associate Professor in the College of Information Sciences and Technology at the Pennsylvania State University. Previously, he was an Assistant Professor at the University of Houston, a Research Assistant Professor at Vanderbilt University, and a Postdoctoral Scholar at the University of California, Berkeley.

His research interests revolve around artificial intelligence and cyber-physical systems, focusing on machine learning for decision making and optimization, with applications in smart and connected communities, critical infrastructure, and cybersecurity.

His research is funded by the National Science Foundation, the Department of Energy, the Department of Transportation, and other agencies.