Secure Smart Contracts with Isabelle/Solidity

Abstract

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. The framework consists of a novel formalization of the Solidity storage model, a shallow embedding of Solidity expressions and statements, an implementation of Isabelle commands to support a user in specifying Solidity smart contracts, and a verification condition generator to support a user in the verification. Compliance of the semantics is tested by a set of unit tests and the approach is evaluated by means of three case studies. Our results show that the framework can be used to verify even complex contracts with reasonable effort. Moreover, they show that the shallow embedding significantly reduces the verification effort compared to an alternative approach based on a deep embedding.