Quantitative analysis of smart contracts Conference Paper


Author(s): Chatterjee, Krishnendu; Goharshady, Amir K; Velner, Yaron
Title: Quantitative analysis of smart contracts
Title Series: LNCS
Affiliation IST Austria
Abstract: Smart contracts are computer programs that are executed by a network of mutually distrusting agents, without the need of an external trusted authority. Smart contracts handle and transfer assets of considerable value (in the form of crypto-currency like Bitcoin). Hence, it is crucial that their implementation is bug-free. We identify the utility (or expected payoff) of interacting with such smart contracts as the basic and canonical quantitative property for such contracts. We present a framework for such quantitative analysis of smart contracts. Such a formal framework poses new and novel research challenges in programming languages, as it requires modeling of game-theoretic aspects to analyze incentives for deviation from honest behavior and modeling utilities which are not specified as standard temporal properties such as safety and termination. While game-theoretic incentives have been analyzed in the security community, their analysis has been restricted to the very special case of stateless games. However, to analyze smart contracts, stateful analysis is required as it must account for the different program states of the protocol. Our main contributions are as follows: we present (i)~a simplified programming language for smart contracts; (ii)~an automatic translation of the programs to state-based games; (iii)~an abstraction-refinement approach to solve such games; and (iv)~experimental results on real-world-inspired smart contracts.
Keywords: abstraction refinement; Game theory; Temporal property; Electronic money; Modeling languages; Automatic translation; Formal framework; Research challenges; Security community; Smart contracts; Trusted authorities; Program translators
Conference Title: 27th European Symposium on Programming, ESOP 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Volume: 10801
Conference Dates: April 14- 20, 2018
Conference Location: Thessaloniki, Greece
ISBN: 03029743
Publisher: Springer  
Date Published: 2018-04-01
Start Page: 739
End Page: 767
DOI: 10.1007/978-3-319-89884-1_26
Notes: The research was partially supported by Vienna Science and Technology Fund (WWTF) Project ICT15-003, Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Starting grant (279307: Graph Games).
Open access: no