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.

本文介绍了一种新的针对智能合约的，关于可量化属性的形式化分析框架，并提出了设计一种简化的智能合约编程语言，自动翻译程序为状态感知博弈，以及实验结果的方法。