Publication Type
Conference Proceeding Article
Version
acceptedVersion
Publication Date
5-2020
Abstract
Bitcoin has been a popular research topic recently. Ethereum (ETH), a second generation of 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 and secure smart contracts is challenging due to the decentralized computation nature of the blockchain. 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 in analyzing and verifying smart contracts. While most of the existing works either focus on EVM bytecode or translate Solidity smart contracts into programs in intermediate languages, we argue that it is important and necessary to understand and formally define the semantics of Solidity since programmers write and reason about smart contracts at the level of source code. In this work, we develop a formal semantics for Solidity which provides a formal specification of smart contracts to define semantic-level security properties for the high-level verification. Furthermore, the proposed semantics defines correct and secure high-level execution behaviours of smart contracts to reason about compiler bugs and assist developers in writing secure smart contracts.
Keywords
Bitcoin, Computer programming languages, Ethereum
Discipline
Finance and Financial Management | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
2020 IEEE 41st Symposium on Security and Privacy: San Francisco, May 18-21: Proceedings
First Page
1695
Last Page
1712
ISBN
9781728134970
Identifier
10.1109/SP40000.2020.00066
Publisher
IEEE
City or Country
Piscataway, NJ
Embargo Period
5-27-2021
Citation
JIAO, Jiao; KAN, Shuanglong; LIN, Shang Wei; SANAN, David; LIU, Yang; and SUN, Jun.
Semantic understanding of smart contracts: Executable operational semantics of solidity. (2020). 2020 IEEE 41st Symposium on Security and Privacy: San Francisco, May 18-21: Proceedings. 1695-1712.
Available at: https://ink.library.smu.edu.sg/sis_research/5968
Copyright Owner and License
Authors
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/SP40000.2020.00066