  Bitcoin has attracted everyone's attention and interest recently. Ethereum
(ETH), a second generation cryptocurrency, extends Bitcoin's design by offering
a Turing-complete programming language called Solidity to develop smart
contracts. Smart contracts allow creditable execution of contracts on EVM
(Ethereum Virtual Machine) without third parties. Developing correct smart
contracts is challenging due to its decentralized computation nature. Buggy
smart contracts may lead to huge financial loss. Furthermore, smart contracts
are very hard, if not impossible, to patch once they are deployed. Thus, there
is a recent surge of interest on analyzing/verifying smart contracts. While
existing work focuses on EVM opcode, we argue that it is equally important to
understand and define the semantics of Solidity since programmers program and
reason about smart contracts at the level of source code. In this work, we
develop the structural operational semantics for Solidity, which allows us to
identify multiple design issues which underlines many problematic smart
contracts. Furthermore, our semantics is executable in the K framework, which
allows us to verify/falsify contracts automatically.
