Quantitative analysis of smart contracts
Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Department
Grant
Series Title
LNCS
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.
Publishing Year
Date Published
2018-04-01
Acknowledgement
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).
Volume
10801
Page
739 - 767
Conference
ESOP: European Symposium on Programming
Conference Location
Thessaloniki, Greece
Conference Date
2018-04-16 – 2018-04-19
IST-REx-ID
Cite this
Chatterjee K, Goharshady AK, Velner Y. Quantitative analysis of smart contracts. In: Vol 10801. Springer; 2018:739-767. doi:10.1007/978-3-319-89884-1_26
Chatterjee, K., Goharshady, A. K., & Velner, Y. (2018). Quantitative analysis of smart contracts (Vol. 10801, pp. 739–767). Presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece: Springer. https://doi.org/10.1007/978-3-319-89884-1_26
Chatterjee, Krishnendu, Amir Kafshdar Goharshady, and Yaron Velner. “Quantitative Analysis of Smart Contracts,” 10801:739–67. Springer, 2018. https://doi.org/10.1007/978-3-319-89884-1_26.
K. Chatterjee, A. K. Goharshady, and Y. Velner, “Quantitative analysis of smart contracts,” presented at the ESOP: European Symposium on Programming, Thessaloniki, Greece, 2018, vol. 10801, pp. 739–767.
Chatterjee K, Goharshady AK, Velner Y. 2018. Quantitative analysis of smart contracts. ESOP: European Symposium on Programming, LNCS, vol. 10801, 739–767.
Chatterjee, Krishnendu, et al. Quantitative Analysis of Smart Contracts. Vol. 10801, Springer, 2018, pp. 739–67, doi:10.1007/978-3-319-89884-1_26.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2018_ESOP_Chatterjee.pdf
1.39 MB
Access Level
Open Access
Date Uploaded
2018-12-17
MD5 Checksum
9c8a8338c571903b599b6ca93abd2cce
Material in ISTA:
Dissertation containing ISTA record