Verified Development and Deployment of Multiple Interacting Smart Contracts with VeriSolid

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.