Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce theVeriSolidframework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction.VeriSolidallows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (calleddeployment diagrams) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability ofVeriSolid, we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by usingVeriSolid. We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.

With the emergence of decentralized finance, smart contracts and their users become more and more susceptible to expensive exploitations. This paper investigates the price gouging transaction order dependency vulnerabilities in smart contracts. A static analysis based approach is proposed to automatically locate and rectify such vulnerabilities, and a prototype tool using Slither, a static analyzer for Solidity, is also developed. All in all, empirical results on a benchmark suite containing 51 Solidity smart contracts show that the proposed methodology can be used successfully to both detect such vulnerabilities and rectify them, or to certify that a Solidity smart contract under question does not contain such vulnerabilities.