Secure Smart Contracts with Isabelle/Solidity

By Diego Marmsoler, Asad Ahmed, and Achim D. Brucker.

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.

Keywords:
Program Verification, Smart Contracts, Isabelle, Solidity

Please cite this work as follows:
D. Marmsoler, A. Ahmed, and A. D. Brucker, “Secure smart contracts with Isabelle/Solidity,” in Software engineering and formal methods (SEFM), A. Madeira and A. Knapp, Eds. Heidelberg: Springer-Verlag, 2024. doi: 10.1007/978-3-031-77382-2_10. Author copy: https://logicalhacking.com/publications/marmsoler.ea-secure-smart-contracts-2024/

BibTeX
@InCollection{ marmsoler.ea:secure-smart-contracts:2024,
  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. },
  keywords  = {Program Verification, Smart Contracts, Isabelle, Solidity},
  author    = {Diego Marmsoler and Asad Ahmed and Achim D. Brucker},
  booktitle = {Software Engineering and Formal Methods (SEFM)},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {15280},
  isbn      = {3-540-25109-X},
  editor    = {Alexandre Madeira and Alexander Knapp},
  title     = {Secure Smart Contracts with {Isabelle/Solidity}},
  areas     = {formal methods, software, security},
  year      = {2024},
  doi       = {10.1007/978-3-031-77382-2_10},
  note      = {Author copy: \url{https://logicalhacking.com/publications/marmsoler.ea-secure-smart-contracts-2024/}},
  pdf       = {https://logicalhacking.com/publications/marmsoler.ea-secure-smart-contracts-2024/marmsoler.ea-secure-smart-contracts-2024.pdf},
}