Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
by Diego Marmsoler and Achim D. Brucker
Smart contracts are automatically executed programs, usually representing 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 saw 280M worth of Ether destroyed. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts. We address this problem by formalizing 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 them 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 a simple verified token.
Keywords:
Categories: ,
Documents: (full text as PDF file)
Please cite this article as follows:
Diego Marmsoler and Achim D. Brucker.
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL.
In Archive of Formal Proofs, 2022. http://www.isa-afp.org/entries/Solidity.html, Formal proof development
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (
| abstract | = | {Smart contracts are automatically executed programs, usually representing 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 saw $280M worth of Ether destroyed. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts. We address this problem by formalizing 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 them 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 a simple verified token.}, | |
| author | = | {Diego Marmsoler and Achim D. Brucker}, | |
| date | = | {2022-07-19}, | |
| issn | = | {2150-914x}, | |
| journal | = | {Archive of Formal Proofs}, | |
| month | = | {jul}, | |
| note | = | {\url{http://www.isa-afp.org/entries/Solidity.html}, Formal proof development}, | |
| = | {https://www.brucker.ch/bibliography/download/2022/marmsoler.ea-isabelle-solidity-2022.pdf}, | ||
| title | = | {Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL}, | |
| url | = | {https://www.brucker.ch/bibliography/abstract/marmsoler.ea-isabelle-solidity-2022}, | |
| year | = | {2022}, |