Abstract
The adoption of blockchain-based distributed computation platforms is growing fast. Some of these platforms, such as Ethereum, provide support for implementing smart contracts, which are envisioned to have novel applications in a broad range of areas, including finance and the Internet-of-Things. However, a significant number of smart contracts deployed in practice suffer from security vulnerabilities, which enable malicious users to steal assets from a contract or to cause damage. Vulnerabilities present a serious issue since contracts may handle financial assets of considerable value, and contract bugs are non-fixable by design. To help developers create more secure smart contracts, we introduce FSolidM, a framework rooted in rigorous semantics for designing contracts as Finite State Machines (FSM). We present a tool for creating FSM on an easy-to-use graphical interface and for automatically generating Ethereum contracts. Further, we introduce a set of design patterns, which we implement as plugins that developers can easily add to their contracts to enhance security and functionality.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
- 4.
Solidity is the most widely used high-level language for developing Ethereum contracts. Solidity code can be translated into Ethereum Virtual Machine bytecode, which can be deployed and executed on the platform.
- 5.
The Ethereum Name Service is a decentralized service, built on smart contracts, for addressing resources using human-readable names.
- 6.
Please note that we introduce an additional plugin in Appendix A.
- 7.
- 8.
- 9.
- 10.
- 11.
- 12.
Gas measures the cost of executing computation on the Ethereum platform.
- 13.
At the time of writing, this cost of deployment was well below $1 (if the deployment does not need to be prioritized).
References
Underwood, S.: Blockchain beyond Bitcoin. Commun. ACM 59(11), 15–17 (2016)
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Technical Report EIP-150, Ethereum Project - Yellow Paper, April 2014
Clack, C.D., Bakshi, V.A., Braine, L.: Smart contract templates: foundations, design landscape and research directions. arXiv preprint arXiv:1608.00771 (2016)
Christidis, K., Devetsikiotis, M.: Blockchains and smart contracts for the Internet of Things. IEEE Access 4, 2292–2303 (2016)
Vukolić, M.: Rethinking permissioned blockchains. In: Proceedings of the ACM Workshop on Blockchain, Cryptocurrencies and Contracts, pp. 3–7. ACM (2017)
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 23rd ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 254–269. ACM, October 2016
Finley, K.: A \$50 million hack just showed that the DAO was all too human. Wired, June 2016. https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/
Qureshi, H.: A hacker stole \$31m of ether - how it happened, and what it means for Ethereum. freeCodeCamp, July 2017. https://medium.freecodecamp.org/a-hacker-stole-31m-of-ether-how-it-happened-and-what-it-means-for-ethereum-9e5dc29e33ce
Bhargavan, K., et al.: Short paper: formal verification of smart contracts. In: Proceedings of the 11th ACM Workshop on Programming Languages and Analysis for Security (PLAS), in Conjunction with ACM CCS 2016, pp. 91–96, October 2016
Leising, M.: The Ether thief. Bloomberg Markets, June 2017. https://www.bloomberg.com/features/2017-the-ether-thief/
Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 614–619. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_45
Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22
Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_8
Bartoletti, M., Pompianu, L.: An empirical analysis of smart contracts: platforms, applications, and design patterns. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 494–509. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_31
Hirai, Y.: Formal verification of deed contract in Ethereum name service, November 2016. https://yoichihirai.com/deed.pdf
Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_33
Fröwis, M., Böhme, R.: In code we trust? In: Garcia-Alfaro, J., Navarro-Arribas, G., Hartenstein, H., Herrera-Joancomartí, J. (eds.) ESORICS/DPM/CBT-2017. LNCS, vol. 10436, pp. 357–372. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67816-0_20
Solidity by Example: Blind auction. http://solidity.readthedocs.io/en/develop/solidity-by-example.html. Accessed 9 May 2017
Solidity Documentation: Common patterns. http://solidity.readthedocs.io/en/develop/common-patterns.html#state-machine. Accessed 9 May 2017
Mavridou, A., Laszka, A.: Designing secure Ethereum smart contracts: a finite state machine based approach. arXiv preprint arXiv:1711.09327 (2017)
Maróti, M., et al.: Next generation (meta) modeling: web-and cloud-based collaborative tool infrastructure. In: Proceedings of the MPM@ MoDELS, pp. 41–60 (2014)
Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: a satellite on-board software case study. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 260–279. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57666-4_16
Acknowledgements
We thank the anonymous reviewers for their invaluable suggestions and feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Event Plugin
A Event Plugin
In this section, we introduce an additional plugin, which developers can use to notify users of transition executions. The event plugin uses the event feature of Solidity, which provides a convenient interface to the Ethereum logging facilities. If this plugin is enabled, transitions tagged with \(\textit{event}\) emit a Solidity event after they are executed. Ethereum clients can listen to these events, allowing them to be notified when a tagged transition is executed on the platform.
Implementation. If the event plugin is enabled, then
where \(\{t_1, t_2, \ldots \}\) is the set of transitions with the tag \(\textit{event}\).
For every transition t such that \(\textit{event} \in t^{tags}\) (i.e., transitions that are tagged to emit an event),
Rights and permissions
Copyright information
© 2018 International Financial Cryptography Association
About this paper
Cite this paper
Mavridou, A., Laszka, A. (2018). Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In: Meiklejohn, S., Sako, K. (eds) Financial Cryptography and Data Security. FC 2018. Lecture Notes in Computer Science(), vol 10957. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-58387-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-662-58387-6_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-58386-9
Online ISBN: 978-3-662-58387-6
eBook Packages: Computer ScienceComputer Science (R0)