Separation Logic pentru Smart Contracts Conducător S ,tiint ,ific: Autor: Prof. Dr. Ing. Iulia Manda Bucures ,ti, 2017 University POLITEHNICA of… [621034]

Universitatea POLITEHNICA din Bucures ,ti
Facultatea de Automatică s ,i Calculatoare,
Departamentul de Calculatoare
LUCRARE DE DISERTAT ,IE
Separation Logic pentru Smart Contracts
Conducător S ,tiint ,ific: Autor:
Prof. Dr. Ing. Iulia Manda
Bucures ,ti, 2017

University POLITEHNICA of Bucharest
Faculty of Automatic Control and Computers,
Computer Science and Engineering Department
MASTER THESIS
Separation Logic for Smart Contracts
Scientific Adviser: Author:
Prof. Dr. Ing. Iulia Manda
Bucharest, 2017

I would like to thank…
I would as well…

Abstract
Cryptocurrency frameworks have recently gained significant attention in the field of research.
Since there is no central authority that guards a decentralized network and updates and reversal
are hardly manageable, security guarantees of the code being deployed on such a network should
be mandatory. Smart contracts are programs running in such a network, written in Solidity.
They can be written and deployed by anyone holding an account, anonymously. This causes
numerous vulnerable spots.
Although Ethereum does not implement explicit concurrency, transactions invoked from differ-
ent accounts can concurr, which may result in unwanted behaviour.
In this paper we present a mean of statically detecting data races in a multi-party communica-
tion private network by using concurrent separation logic. This method could as well be used
if parallelization of operations will be implemented in Ethereum.
Keywords: cryptocurrency, Ethereum, separation logic, formal verification
ii

Contents
Acknowledgements i
Abstract ii
1 Introduction 1
1.1 Project Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2
1.3 Thesis Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
2 State of the Art 4
2.1 Decentralized Platforms and Smart Contracts . . . . . . . . . . . . . . . . . . . . 4
2.1.1 Decentralized Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
2.1.2 Smart Contracts in Ethereum . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Vulnerabilities and Attacks in Smart Contracts . . . . . . . . . . . . . . . . . . . 6
2.2.1 The DAO . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2.2 Transaction Ordering Dependence . . . . . . . . . . . . . . . . . . . . . . 7
2.3 Formal Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.4 Concurrent Separation Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
2.5 Verification of Smart Contracts . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
2.6 Verification Tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
3 Related Work 9
3.1 EVM Verification Using Proof Assistants . . . . . . . . . . . . . . . . . . . . . . . 9
3.1.1 eth-isabelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.1.2 KEVM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.2 Contract Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
3.3 A Concurrent Perspective on Smart Contracts . . . . . . . . . . . . . . . . . . . . 10
3.4 Others . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
4 Implementation 12
4.1 Implementation Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
4.2 Other ideas we have tried . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
4.3 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
5 Evaluation 15
6 Conclusions and Future Work 16
iii

List of Figures
2.1 Ethereum Network Components . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
2.2 Deploy a Custom Smart Contract . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
4.1 Voting Contract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
4.2 Transaction Ordering Concurrency . . . . . . . . . . . . . . . . . . . . . . . . . . 13
iv

Chapter 1
Introduction
Decentralized networks and their implementation as cryptocurrency systems have recently
gained significant popularity due to the numerous use cases they enable. Smart contracts have
added significant value to cryptocurrencies due to their capability of defining contract rules and
automatically enforcing them to the existing parties2. Ethereum implements Ethereum Virtual
Machine (EVM3), a platform which allows various applications to run on. In Ethereum, it is
simple not only for developers to write and deploy smart contracts. Therefore, it is crucial to
prove automatically that their implementation is secure against attacks.
Formal verification is the mean of evaluating the correctness of a program with respect to a
certain formal specification, using formal methods of mathematics [ ?]. Formalization is useful
for analyzing and deploying reliable smart contracts. In this paper we present an idea on how
to formally specify and verify certain properties of Ethereum smart contracts statically.
1.1 Project Description
Ethererum does not implement real concurrency, in terms of how the operations/ transactions
in the network are executed by the miners. Even so, there are multiple studied examples in
which data races or communication issues can occur. Given this, we propose a method to
statically detect this kind of issues using concurrent separation logic. We will work on a proof
of concept example and show how we can overcome this kind of issues (TODO: reformuleaza).
The following assumptions were considered for the proposed solution:
we can use local reasoning projected globally in order to check if there is any concurrent
behaviour on a certain shared resource
the language in which we write our example could be easily translated into EVM bytecode
in order to be cross-checked with its correspondent written in Solidity
Research on this topic is recent and the main focus so far was on formalizing the infrastructure
on which the contracts run (Ethereum VM) or on other properties of smart contracts. Since it
is very hard to name a contract reliable without verifying the bytecode, our idea as well is not
complete until we provide a compiler from our language to EVM bytecode that can run on the
EVM so that we can cross-check.
In [], I. Sergey et. al. present a concurrent view on smart contracts. They discuss by means of
an analogy with threads how implicit concurrency could be added for smart contracts. They
2https://blockgeeks.com/guides/smart-contracts/
3http://ethdocs.org/en/latest/introduction/what-is-ethereum.html
1

CHAPTER 1. INTRODUCTION 2
examine as well means for approaching concurrency issues in smart contracts, but do not
offer any specific example/implementation using concurrent separation logic, even though they
present its benefits.
1.2 Motivation
Besides detecting current vulnerabilities determined by implicit concurrency (due to transac-
tion ordering, for example []), Solidy [] (smart contracts’ implementation language), is still
under considerable improvement. In this context, it is probable that explicit synchronization
mechanisms will be added, in which case automatic tools could as well provide the solution for
concurrency issues (and not only detect them).
On the running example:
o entitate – Seller – pune la dispozitie o resursa shared (price), care poate fi accesata de alte
entitati – Buyer-i – iar in functie de actiunile acestora valoarea resursei se poate modifica (daca
Buyer-ii au cumparat produse a.i stock-ul sa ajunga sub o anumita valoare, pretul produsului
creste).
Explanation: price can be changed if Seller has less than y products in stock after Buyer1’s
request. Thus, price in Buyer2 can be outdated.
Translate this Solidity program into a minimalistic language that can be verified
Formalize this language
Create the specification language
Model the problem using these + CSP
Prove that there are no data races.
As a result, we will be able to detect existing data races. There are possible solutions after the
detection, but they have to be manually implemented by the developer of the contract before
being deployed.
We base our idea from a comparison between parties in Ethereum and threads using concurrent
objects in shared memory []. We state the problem as follows: at any moment at most one
thread can query/modify memory’s state. Separation of state access has long been studied in
concurrent separation logic, this is why it seems to be fit for our problem.
In order to prohibit the unwelcome interference on a contract’s state, we need to control the
set of operations allowed for different parties. This would need to enforce exclusive ownership
for a party over an object. In Ethereum, this is solved just by allowing only the owner of
the contract to make certain changes []. This discharges completely the idea of concurrency,
even though it is clearly existent implicitly []. In this context, we provide a way to detect
possible concurrency issues by using concurrent separation logic, which has been used in the
past to define an ownership discipline and to verify that a particular implementation follows
this definition [].
The solution is useful to avoid existing data races due to transaction ordering dependencies in
Ethereum smart contracts. Moreover, since there are currently ongoing discussions of imple-
menting explicit concurrency in Ethereum in order to improve the speed of running transac-
tions, our approach could enhance the security mechanisms used for guaranteeing the correct
functioning of the newtork.

CHAPTER 1. INTRODUCTION 3
1.3 Thesis Structure
The chapters of the thesis are structured as follows: Chapter2 presents the concepts required
for the user to familiarize with in order to understand the proposed solution. Chapter3 details
related work in the area of formal verification of smart contracts. Chapter4 Chapter5 Chapter6

Chapter 2
State of the Art
In this chapter we create an overview of the domains which we which we base our work on:
decentralized networks and formal verification. Our work is targetting smart contracts as they
are implemented in Ethereum. For the verification part we will discuss more about concurrent
separation logic, since it is the mean used to approach our problem. We will shortly discuss
general attack vectors existing in Ethereum.
2.1 Decentralized Platforms and Smart Contracts
In this section we make a brief introduction to decentralized systems and to smart contracts.
We will focus on smart contracts in Ethereum, which is currently the mostly used platform for
running them.
2.1.1 Decentralized Systems
Acryptocurrency is a digital currency in which encryption mechanisms are used to control
the generation of units of currency, in order to provide the unicity of the generated units.
In adecentralized network , there is no central entity that coordinates the actions of the
involved peers. The resources of the network are represented by the global collection of the
resources added by each individual workstation. All the entities in the network are of equal
importance and capabilities, and at the same time are capable or running independently of each
other.
In such a network, anonimity is guaranteed by default – all the transactions are made under
the identity of an account, and not an individual. Moreover, in a fully decentralized network,
all the actions are public to everyone, causing the transparrency of the network. Decentralized
networks implicitly implement a solution for DDoS attacks (e.g the Dyn attack2), since they do
not contain any single point of failure that can be exploited by attackers. In order to succeed
with such an attack in a decentralized network, each station should be attacked individually3
Ablockchain is similar to distributed database of records. It is a public ledger recording all
the transactions that have been executed on the network. These transactions are immutable, so
thereisnomeantomodifyorremovethem, guaranteeingfull transparency . Alltheblockchain
2https://en.wikipedia.org/wiki/2016_Dyn_cyberattack
3https://streembit.github.io/2017-01-04-DDoS/
4

CHAPTER 2. STATE OF THE ART 5
is shared among participating parties. Each transaction is verified by a distributed consensus.
Briefly, this works… TODO>
Applications of blockchain technologies include implementations of custom currencies, control-
ling these currencies directly by programs that run on the network – smart contracts – that can
be implemented by anyone. Even more, they allow the existence of complex applications, that
take the form of decentralized autonomous organizations (DAOs)[7].
2.1.2 Smart Contracts in Ethereum
Bitconis the first important decentralized cryptocurrency framework. The main disadvatages
of Bitcoin are the very specific use-case (cryptocurrency) it allows, lack of Turing-completeness,
long time to create and distribute blocks between miners and long transaction confirmation
times (ten minutes, on average).
Ethereum appeared in order to overcome some of the disadvantage of previous cryptocurrency
frameworks, mainly by allowing more generic operations. It is a decentralized platform, sup-
porting cyrptocurrencies and applications (smart contracts) at the same time, or interefered.
The role of the digital currency in Ethereum is mainly to transfer, store and execute code, but
Ether can be as well transferred between different accounts. This covers the behaviour of other
cryptocurrency systems, such as Bitcoin.
Image 2.1 describes briefly the main Ethereum components and possible actions.
Figure 2.1: Ethereum Network Components
Ethereum smart contracts run on its custom virtual machine, EVM (which is Turing-complete
[]). Anyone with an account can write smart contracts. At the moment it uses "ASIC-resistant"
Proof of Work algorithm1. It implements a consensus protocol, which practically decides the
miner (resource in the network) which is going to run a certain transaction. Mining is the
process of aggregating multiple transactions, building them into a block and trying different
1https://github.com/ethereum/wiki/wiki/Ethash-Design-Rationale

CHAPTER 2. STATE OF THE ART 6
values for nonces[] until one that respects the proof of work condition is found. The miner that
produces a valid block receives a variable number of Ether as a reward and all of the transaction
fees in the block [1].
Smart contracts Smart contracts are programs that are stored and replicated on a distributed
storage platform. They are executed by a network of computers. Each action (transaction)
triggered by running a function from a smart contract can result in ledger updates: account
balances, variable states etc.
The steps for creating and deploying a smart contract are straightforward, and are discribed in
2.2.
Figure 2.2: Deploy a Custom Smart Contract
Within a smart contract, one can create any custom rules for ownership, transactions or for the
correctness of the modified states following diverse actions. This can result in a lot of vulnerable
spots, such as:
1if(gameHasEnded && !( prizePaidOut ) ) {
2 winner.send(1000);
3 prizePaidOut = True;
4}
In this situation, we know that the call to send from the winner address can fail, throwing an
exception. But in this case the error code of the call to send function is not checked. Thus, in
case there is an error, the winner does not receive the prize (1000 Ether), prizePaidOut variable
is set [4].
2.2 Vulnerabilities and Attacks in Smart Contracts
2.2.1 The DAO
A DAO (decentralized autonomous application) is a virtual organization, invloving multiple
user accounts, that is run through rules encoded as smart contracts.
The code (smart contracts) that will run a DAO can be written by anyone. The writers will
be the users of the organization. Ininitially, there is a founding period. Whoever is investing
fundsintheorganizations, receivesacorrespondingnumberoftokens, whichwilldefineinfluence
their decision making in the organization. After the funding period, the DAO starts to function.

CHAPTER 2. STATE OF THE ART 7
Owners of tokens in the DAO can propose targets for how to invest the money. Afterwards,
they have a common voting period in which they decide in what to invest.
Also known as Race to Empty or Recursive Call Attack Re-entrancy manifests as a race between
a recursive call to continue the contract’s behavior and updates to the contract state that should
be sequentially handled before the recursive call Vulnerable function: splitDAO()
All calls to send should have a gas limit Balances should be reduced before a send, not after
one The splitDAO() should be mutexed and keep permanent track of the status of each possible
splitter, not just through token tracking Long term: a purely functional language with a rich
type system
TODO: Zi de cum ajuta formal verifiation aici. E good proof.
2.2.2 Transaction Ordering Dependence
2.3 Formal Verification
By formally proving a property of a smart contract, malicious attackers cannot find any input
that breaks the proven attribute of the contract. Since EVM is constantly being updated, the
verification must be constantly re-checked against the new variants.
Formal verification is a method to prove a program correct with respect to a given formal
specification. There are many formal means of reasoning about the correctness of programs [],
but in this section we will discuss about Hoare logic, which represents the technical basis for
our work. Separation logic, which we will use to analyze contract properties, is an extension of
Hoare logic.
Hoare logic introduces two properties, preconditions and post conditions. The precondition has
to be correct in order for the function to be executed, while the postcondition has to be met
after the function has run. Both have to be true in order for the program to be proven correct.
A Hoare triple is formally defined as follows:
{P} S {Q}
where P is the precondition, Q is the postcondition and S is the program to be verified.
A proof in Hoare logic is a sequence of rules, each of which is either an axiom of the logic is
deduced from earlier rules by inferint the logic[8]. They must be sound1in order to deduce true
conclusions.
Hoare logic serves as the basis for many software verification tools, but has a lot of limitations:
difficult to check recursive predicate, hard to prove properties about shared objects, difficult to
make local reasoning, as well as yielding proofs that are hard to debugi[10]. In the following
section we discuss how separation logic can be used to overcome these limitations.
2.4 Concurrent Separation Logic
Separation logic extends Hoare logic, by allowing reasoning about applications that orchestrate
pointer data structures, logical separation between concurrent processes and changes of owner-
ship on resources. It defines the separating conjunction P Q, which states the fact that the
pre and postconditions will hold for separate portions of memory, enabling writing proof rules
that make use of the separation concept to provide modular reasoning about programs. Thus,
1https://en.wikipedia.org/wiki/Soundness

CHAPTER 2. STATE OF THE ART 8
the conjunction is true is and only if the memory can be split in two parts, one which satisfies
P and another which satisfies Q.
Needed to mention is a specific inference rule of separation logic, which enables local reasoning:
fPgSfQg
fPgfRgSfQgfRgmodif (C)\fr(R) =;
This rule means that if a programs executes correctly in a local state, satisfyin P, it can execute
correctly in any global state R – the reason why R is true in the postcondition and non of the
variables that S is modifying are free1in2R. Brifly, this rule helps infering global specifications
from local ones.
Additionally, concurrent separation logic is an adaptation of separation logic for reasoning
about resource management in concurrent programs, introduced by Peter O’Hearn[12]. Fol-
lowing the frame rule of separation logic ??, if we specify in the precondition separately the
resources accessed by each process, then we, then we can reason about the concurrent processes
independently.
2.5 Verification of Smart Contracts
Verification of smart contracts appeared as a need to deploy reliable smart contracts. The main
components that would benefit from finding a good method for large scale contract verification
are: smart contracts properties, language to EVM compiler, the EVM specification, developing
a safer smart contract language.
The two main aspects to check for are: correctness – after defining a specification for how a user
wants the program to behave, the runtime conforms to that specification – and performance –
accurate pre-estimation of gas consumption of a transaction.
The most popular programming language for smart contracts is Solidity3. It has a rich syntax
but no formal specification. The only definition of Solidity is the Solidity compiler implemen-
tation, which compiles Solidity programs into EVM bytecode. Solidity must be compiled to
bytecode and run on the EVM in order to check the exact behaviour of the implementation.
Thus, the code that is statically verified should be automatically translated into bytecode and
reverse in order to cross-check the validity of the verification.
[?]
2.6 Verification Tools
smallfoot TODO: Second, Smallfoot uses a strict separation model, which does not allow
sharing of read access. As a consequence it cannot handle, e.g., a readers and writers program,
whichisprovenin[8]usingalessstrict“countingpermissions” modelofseparationlogic. Adding
permission accounting is on our to-do list.
holfoot
1https://en.wikipedia.org/wiki/Free_variables_and_bound_variables
2https://en.wikipedia.org/wiki/Separation_logic
3https://solidity.readthedocs.io/en/develop/

Chapter 3
Related Work
Since the DAO attack2, research in the area of formal verification of Ethereum infrastructe
has incresead signifficantly. Due to numerous factors, such as investments and the fact that
decentralized cryptocurrencies cannot be largely used but safety and reliability are guaranteed
(since changes of the network state are costly), current research is extremely novel and new
proposals/ideas are developing day by day.
In this chapter we present the current efforts in proving the correctness, performance and
security of the Ethereum network and implicitly of the running contracts. In TODO section
we detail an idea which represents the basis of our work.
3.1 EVM Verification Using Proof Assistants
3.1.1 eth-isabelle
In his work [9], Yoichi et. al. defined EVM in Lem3, a lightweight tool for writing semantic def-
initions. The language can be compiled to generate definitions for interactive theorem provers,
in their case Isabelle/HOL.
The definition covers all EVM instructions. The EVM definition was tested against an official
test suite for Ethereum implementations, while its full verification is still in progress. They
proved some safety properties of Ethereum smart contracts in Isabelle/HOL, such as reentrancy,
a topic undergoing intense study since the DAO attack. An important contribution is that they
discovered differences between the specification (Yellow Paper [14]) and the implementation,
which resulted in updates of the YP.
3.1.2 KEVM
In [9], Yoichi et. al. present the K-Framework [22] as a good alternative for Lem. The K-
Frameworkisatoolspecificallyengineeredfordefiningprogramminglanguages. ThegoalofKis
toseparatespecificationofanalysistoolsfromspecificationofparticularprogramminglanguages
or other models, making it easier to specify both the analysis tools and the programming
languages.
2https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability/
3http://www.cl.cam.ac.uk/ pes20/lem/
9

CHAPTER 3. RELATED WORK 10
3.2 Contract Verification
Luu et al. [11] proposes one of the fisrt tools for automatically verifying smart contracts, called
Oyente. This symbolic execution tool statically reasons about a program path-by-path. It
analyzes directly EVM bytecode, using Z3-solver (e.g to decide satisfiability). Oyente simulates
EVM code which, according to the Yellow Paper, has 64 instructions.
It requires as input:
The contract bytecode, which maps instructions to constraints;
Ethereum global state – current values of contract variables
The tool detects problematic symbolic paths, arose from bugs such as transaction-ordering
dependence, timestamp-dependence or mishandled exceptions[11]. As a result, a contract can
be modified to throw each time such a bug is detected.
An interesting bug Oyente can detect is briefly explained further. In Ethereum, the limit of
the depth of the call stack to 1024. After exceeding this limit, the send instruction fails. The
call stack is increased either by a call or a send. A malicious use can deliberately reach the
settled limit by calling itself 1023 time, though determining the call to fail [2]. As long as if
the callee raises an exception, it pushes 0 to the the caller’s operand stack. Thus, it is the
responsability of the caller to check the top of the stack. In case it doesn’t, it is considered that
it has undefined behaviour.
In Solidity, it is easy to fail knowing that that sendand its variants are not guaranteed to
succeed (send returns a bool). An unsuccessful send does not trigger an exception. The pro-
grammer has to undo any side effects manually.
Another issue is detailed by Bhargavan et. al. [6]. Since transactions are also method calls,
transferring funds to another contract is a transfer of program control => reentrancy issues X
et. al created an effect system that detects the type of F* computations that return values of
type a. In this way it is possible to enforce that a contract always throws when a send fails.
In order for the verification to be accurate, it is required as well that the formal modelling
of the Ethereum source code (in Solidity) matches the generated bytecode. In practice, given
a Solidity program and its equivalent EVM bytecode, they propose translating both into F*
language1and verify their equivalence using relational reasoning.
3.3 A Concurrent Perspective on Smart Contracts
Sergey et al.[13] propose an approach for managing concurrency between smart contracts in
blockchains, introducing as well a way of implementing multi-threading in such an ecosystem.
They suggest that accounts calling methods of smart contracts in a blockchain are similar to
threads using concurrent objects in shared memory. Since there is no explicit concurrency in
Ethereum, bad synchronization, as we shall see further, determines data races wich result in
losing the integrity of the memory.
A smart contract’s methods can be accessed by multiple peers both within a block and in
multiple blocks, depending on how the transactions were grouped in blocks by the miners.
Transactions from the same account are guaranteed to be executed sequencially due to the
nonce. This represents a simple value associated with the account which counts the number of
transactions that respective account has made in the whole network. Thereby, there is no need
to discuss about concurrency in case of transactions arising from the same account. Otherwise,
between different accounts, there is no ordering gurantee.
1https://www.fstar-lang.org/

CHAPTER 3. RELATED WORK 11
Being able to call Calling other contracts == cooperative multitasking (e.g the DAO) =>
reentrancy Contract as a service for users and contracts: managing access to a shared resource
They as well summaries which could be the benefits of formal verificaton in various concurrent
aspects of communication between accounts and smart contracts: detecting the violations of
atomicity assumptions, lack of synchronization, permission accounting and separation of state
access, through the means of concurrent separation logic, fractional/counting permissions.
3.4 Others
Securify[3] is a tool, currently in Beta, that formally verifies Ethereum contracts for common
security issues, such as transaction reordering and missing input validation. Securify is the
first smart contract verifier that provides: automation, to enable everyone to verify contracts,
guarantees, to ensure the contract is free of certain vulnerabilities, and extensibility, to capture
any newly discovered security vulnerabilities.
Existing solutions based on executing the contract check only a subset of the possible paths and
can therefore miss critical security problems. Further, approaches based on interactive-theorem
provers can provide strong guarantees, for all paths, but they cannot be easily automated or
easily extended. In contrast, Securify combines the best of both worlds: it analyzes all paths
while being fully automated. Further, Securify features a designated domain-specific language
for specifying vulnerabilities, which makes it easy to keep Securify up-to-date with current
security and other reliability issues.

Chapter 4
Implementation
4.1 Implementation Overview
4.2 Other ideas we have tried
Voting Contract
Figure 4.1: Voting Contract
Starting from the Voting contract example on the Solidity official page[5]
We consider the following two functions: giveRightToVote(), vote().
The chairperson can make one of the following actions:
Adds the proposal names
12

CHAPTER 4. IMPLEMENTATION 13
Gives right to vote to certain voters (based on their address)
1 voters[voter].weight = 1;
Decides the winner
The voter, on the other hand, can take the following actions:
Votes a certain proposal:
proposals[proposal].voteCount += sender.weight;
As long as there is no guarantee of ordering of transactions issued by different accounts (TODO:
speak about nonce), we can end up in the following situation: a voter can try to vote before it is
given the right to do that. If so, and he should actually have the right to vote if the operations
happened in the wished order, then his vote will wrongly not count.
TODO: A bit abt HIP/SLEEK, protocol, peer local reasoning with separation logic, why it
does not wrok. Why we cannot use it in the other example.
Gas Estimation Short description of the gas consumption thingy (each instruction costs X,
decompile bytecode and estimate the costs)
4.3 Implementation
1. Create the running example (voting contract/ seller buyer)
Figure 4.2: Transaction Ordering Concurrency
1recv(x)
2if(stock > x)
3 send(x)
4If ((stock – x) < y)
5 price++
2. Establish a minimal language for the example

CHAPTER 4. IMPLEMENTATION 14
3. Formalize the language decided at 2.
4. Create and formalize a specification language
5. Model the problem having 2/3/4
6. Show on the model that you can detect the data race.
Resouces:
Data race detection with CSL (Concurrent Separation Logic)
Examples related to session logic and abstract states of the programs
Communicating State Transition Systems for Fine-Grained Concurrent Resources
http://ilyasergey.net/projects/fcsl/

Chapter 5
Evaluation
15

Chapter 6
Conclusions and Future Work
16

Bibliography
[1] Ethereum glossary. https://github.com/ethereum/wiki/wiki/Glossary , Accessed: August
2017.
[2] Ethereum safety. https://github.com/ethereum/wiki/wiki/Safety , Accessed: August 2017.
[3] Securify. http://http://securify.ch/ , Accessed: August 2017.
[4] Send failure bug. http://hackingdistributed.com/2016/06/16/
scanning-live-ethereum-contracts-for-bugs/ , Accessed: August 2017.
[5] Solidity voting contract. http://solidity.readthedocs.io/en/develop/solidity-by-example.html ,
Accessed: August 2017.
[6] Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi,
Georges Gonthier, Nadim Kobeissi, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy,
and Santiago Zanella-Béguelin. Short paper: Formal verification of smart contracts.
[7] Vitalik Buterin et al. Ethereum white paper, 2013.
[8] Mike Gordon. Background reading on hoare logic, 2012.
[9] Yoichi Hirai. Defining the ethereum virtual machine for interactive theorem provers.
[10] Michael Johnson and Varmo Vene. Algebraic Methodology and Software Technology .
Springer, 2006.
[11] LoiLuu, Duc-HiepChu, HrishiOlickel, PrateekSaxena, andAquinasHobor. Makingsmart
contracts smarter. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and
Communications Security , pages 254–269. ACM, 2016.
[12] Peter W O’hearn. Resources, concurrency, and local reasoning. Theoretical computer
science, 375(1-3):271–307, 2007.
[13] Ilya Sergey and Aquinas Hobor. A concurrent perspective on smart contracts. arXiv
preprint arXiv:1702.05511 , 2017.
[14] Gavin Wood. Ethereum yellow paper, 2014.
17