Smart contracts are digital contracts stored on a blockchain that are automatically executed when predetermined terms and conditions are met. They are often used to automate financial transactions and thus they hold great potential to transform and disrupt the financial industry. In particular it is estimated that blockchain and smart contracts can add up to $72.2B to the UK’s GDP by 2030 and create up to 700,000 new jobs by 2030.

Technically, smart contracts are programs and as such, they may contain bugs. However, since smart contracts are often used to automate financial transactions, exploiting these bugs may result in huge financial damages. In 2016, for example, a vulnerability in a smart contract was exploited, resulting in a loss of approximately $60M. More recently, hackers had exploited a vulnerability in a smart contract to steal $600M. In general, it is estimated that since 2019, more than $5B were lost due to vulnerabilities in smart contracts. This threatens society’s trust in smart contracts and thus limits their potential for the development of FinTech, one of the most promising sectors for the UK economy.

Unfortunately, however, even rigorous testing and auditing cannot guarantee that a smart contract does what it is supposed to do. In the best case scenario, vulnerabilities can be found with these techniques but they can never guarantee their absence.

Thus, with this project, we will develop tools and techniques to support the verification of smart contracts to achieve the highest degree of reliability. Finally, we will engage in training next generation experts in the verification of smart contracts by hosting a summer school on formal methods for blockchains in Exeter

Semantics

The core of Isabelle/Solidity is a deep embedding of Solidity in Isabelle/HOL. A first version of the semantics is described in our paper A Denotational Semantics of Solidity in Isabelle/HOL presented at the 19th International Conference on Software Engineering and Formal Methods.

Since then the language was constantly extended and as of now it supports the following features of Solidity:

• Fixed-size integer types of various lengths and corresponding arithmetic.
• Domain-specific primitives, such as money transfer or balance queries.
• Different types of stores, such as storage, memory, and stack.
• Complex data types, such as hash-maps and arrays.
• Assignments with different semantics, depending on data types.
• An extendable gas model.
• External and internal method declarations and the ability to transfer funds with external method calls.
• Declaration of fallback methods which are executed with monetary transfers.
• Dynamic creation of new contract instances.

Validation

To ensure our semantics complies with the reference implementation the semantics comes with a grammar based fuzzying framework to allow for automatic testing of compliance. The testing framework is described in more detail in our paper Conformance Testing of Formal Semantics using Grammar-based Fuzzing presented at the 16th International Conference on Tests and Proofs.

Applications

The semantics was so far used to verify the correctness of a gas optimization tool and a basic implementation of a token.

Funding

This project is funded by EPSRC under grant no EP/X027619/1