Abstract

The Ethereum blockchain is often called a decentralized world computer. On this blockchain smart
contracts are deployed and executed. Smart contracts can control the platform's own currency
(ether) and data that is associated with a particular address. Changes can be made to the contract
internals by executing transactions on the set of functions that the smart contract oers. In this
thesis the background of the Ethereum network and how smart contracts execute on the blockchain
are explained. The dierence with standard programs is important because smart contracts are
committed to the blockchain. This means that the contract code is public and unchangeable.
Which means that everybody can read this code and interact with it. Ensuring the contract
executed like intended is important because vulnerabilities can not be easily solved. A number of
real world vulnerabilities have been detected and exploited on smart contracts. This resulted in
the loss of several millions of ether to malicious users.
Many tools and solutions have been proposed to make it easier to develop secure smart contracts.
Contracts can be made more secure by providing test suites and execute many tests for contracts.
However this only proves that the contract is correct for that specic set of inputs. Other solutions
to improve security are verication tools. Contracts are made more secure by analyzing them
with static analysis tools and detect patterns that are known to be vulnerable. Other tools let
users dene properties about the contract behaviour. These properties are then checked using a
model that tries to prove them correctly. These properties are then proven against all possible
inputs which means that smart contracts are more secure. However, giving a specication that is
correct and proving it against all possible inputs is dicult and suers from state explosion. Our
contribution is to design a method for the verication of smart contracts.
This thesis introduces the tool Solitor. Solitor is short for Solidity (runtime) monitor, and
uses runtime verication as a technique to make smart contracts more secure. It enables users to
specify the behaviour of a contract using annotations. It is a tool developed specically for smart
contracts on the Ethereum network. We dene an annotation language to specify the requirements
on a smart contract. Solitor can parse and translate these annotations in Solidity contracts to
Solidity code which checks the annotation at runtime. Annotations can be used to check if certain
properties hold during execution of the smart contract. These can either be contract invariants
or pre and postconditions for methods. In general, annotations are logical expressions that can
reference contract variables and blockchain specic identiers. To recognize the annotations the
original Solidity grammar is extended and is similar to that of the Java Modelling Language (JML).
To evaluate and validate the tool, we also describe two case studies, where the tool is used to specify
correct behaviour or detect a vulnerability.

Additional Resources

1. MSc thesis