Smart Contracts - A Killer Application for Deductive Source Code Verification

Wolfgang Ahrendt, Gordon J. Pace, Gerardo Schneider

Smart contracts are agreements between parties which, not only describe the ideal behaviour
expected from those parties, but also automates such ideal performance. Blockchain, and
similar distributed ledger technologies have enabled the realisation of smart contracts
without the need of trusted parties - typically using computer programs which have access
to digital assets to describe smart contracts, storing and executing them in a transparent
and immutable manner on a blockchain. Many approaches have adopted fully fledged programming
languages to describe smart contract, thus inheriting from software the challenge of
correctness and verification - just as in software systems, in smart contracts mistakes
happen easily, leading to unintended and undesirable behaviour. Such wrong behaviour may
show accidentally, but as the contract code is public, malicious users can seek for
vulnerabilities to exploit, causing severe damage. This is witnessed by the increasing number
of real world incidents, many leading to huge financial losses. As in critical software, the
formal verification of smart contracts is thus paramount. In this paper we argue for the use
of deductive software verification as a way to increase confidence in the correctness of
smart contracts. We describe challenges and opportunities, and a concrete research program,
for deductive source code level verification, focussing on the most widely used smart
contract platform and language, Ethereum and Solidity.