Secure Smart Contracts with Isabelle/Solidity
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.
For example, in 2016, a vulnerability in an Ethereum smart contract was exploited, resulting in a loss of approximately $60M. More recently, hackers exploited a vulnerability in the DeFi-platform Poly Network to steal $600M. Overall, it is estimated that since 2019, more than $5B have been stolen due to vulnerabilities in smart contracts. The high impact of vulnerabilities in smart contracts, together with the fact that once deployed to the blockchain, they cannot be updated or removed easily, makes it important to “get them right” before they are deployed. To address this problem, we developed Isabelle/Solidity, a shallow embedding of Solidity in Isabelle/HOL.
Isabelle/Solidity 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.
In our paper at the Software Engineering and Formal Methods (SEFM 2024) conference [1], we describe Isabelle/Solidity in more detail and also show how we ensure its compliance to the official Solidity tooling.