A Denotational Semantics of Solidity in Isabelle/HOL

By Diego Marmsoler and Achim D. Brucker.

Smart contracts are programs, usually automating legal agreements such as financial transactions. Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly initialized contract was the root cause of the Parity Wallet bug that made USD 280mil worth of Ether inaccessible. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts.

In this paper, we address this problem by presenting an executable denotational semantics for Solidity in the interactive theorem prover Isabelle/HOL. This formal semantics builds the foundation of an interactive program verification environment for Solidity programs and allows for inspecting Solidity programs by (symbolic) execution. We combine the latter with grammar-based fuzzing to ensure that our formal semantics complies to the Solidity implementation on the Ethereum Blockchain. Finally, we demonstrate the formal verification of Solidity programs by two examples: constant folding and memory optimization.

Keywords:
Solidity, Denotational Semantics, Isabelle/HOL, Gas Optimization

Supplementary material:
[  label  ]

Please cite this work as follows:
D. Marmsoler and A. D. Brucker, “A denotational semantics of Solidity in Isabelle/HOL,” in Software engineering and formal methods (SEFM), R. Calinescu and C. Pasareanu, Eds. Heidelberg: Springer-Verlag, 2021. Author copy: https://logicalhacking.com/publications/marmsoler.ea-solidity-semantics-2021/

BibTeX
@InCollection{ marmsoler.ea:solidity-semantics:2021,
  abstract        = {Smart contracts are programs, usually automating legal
                     agreements such as financial transactions. Thus, bugs in smart
                     contracts can lead to large financial losses. For example, an
                     incorrectly initialized contract was the root cause of the
                     Parity Wallet bug that made USD 280mil worth of Ether
                     inaccessible. Ether is the cryptocurrency of the Ethereum
                     blockchain that uses Solidity for expressing smart contracts.
                     
                     In this paper, we address this problem by presenting an
                     executable denotational semantics for Solidity in the
                     interactive theorem prover Isabelle/HOL. This formal semantics
                     builds the foundation of an interactive program verification
                     environment for Solidity programs and allows for inspecting
                     Solidity programs by (symbolic) execution. We combine the
                     latter with grammar-based fuzzing to ensure that our formal
                     semantics complies to the Solidity implementation on the
                     Ethereum Blockchain. Finally, we demonstrate the formal
                     verification of Solidity programs by two examples: constant
                     folding and memory optimization.},
  keywords        = {Solidity, Denotational Semantics, Isabelle/HOL, Gas
                     Optimization},
  author          = {Diego Marmsoler and Achim D. Brucker},
  booktitle       = {Software Engineering and Formal Methods (SEFM)},
  language        = {USenglish},
  publisher       = {Springer-Verlag },
  address         = {Heidelberg },
  series          = {Lecture Notes in Computer Science },
  isbn            = {3-540-25109-X},
  editor          = {Radu Calinescu and Corina Pasareanu},
  title           = {A Denotational Semantics of {Solidity} in {Isabelle/HOL}},
  areas           = {formal methods, software},
  year            = {2021},
  supplementary01 = {https://www.isa-afp.org/entries/Solidity.html},
  supplabel01     = {label},
  note            = {Author copy: \url{https://logicalhacking.com/publications/marmsoler.ea-solidity-semantics-2021/}},
  pdf             = {https://logicalhacking.com/publications/marmsoler.ea-solidity-semantics-2021/marmsoler.ea-solidity-semantics-2021.pdf},
}