Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Isabelle/Solidity: A Deep Embe...


view this post on Zulip Email Gateway (Aug 12 2022 at 18:29):

From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Isabelle/Solidity: A Deep Embedding of Solidity in Isabelle/HOL
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.

https://www.isa-afp.org/entries/Solidity.html

Enjoy!


Last updated: Mar 29 2024 at 04:18 UTC