Abstract
Smart contracts are appealing because they are self-executing business agreements between parties with the predefined and immutable obligations and rights. However, as with all software, smart contracts may contain vulnerabilities because of design flaws, which may be exploited by one of the parties to defraud the others. In this paper, we demonstrate a systematic approach to building secure design models for smart contracts using formal methods. To build the secure models, we first model the behaviors of participating parties as state machines, and then, we model the predefined obligations and rights of contracts, which specify the interactions among state machines for achieving the business goal. After that, we illustrate executable secure model design patterns in TLA+ (Temporal Logic of Actions) to against well-known smart contract vulnerabilities in terms of state machines and obligations and rights at the design level. These vulnerabilities are found in Ethereum contracts, including Call to the unknown, Gasless send, Reentrancy, Lost in the transfer, and Unpredictable state. The resultant TLA+ specifications are called secure models. We illustrate our approach to detect the vulnerabilities using a real-estate contract example at the design level.
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
References
Mohanty, D.: BlockChain: From Concept to Execution. Independently published (2018)
Finley, K.: A 50 million hack just showed that the dao was all too human (2016). https://www.wired.com/2016/06/50-million-hack-just-showed-dao-human/
Meyer, B.: Object-Oriented Software Construction, vol. 2. Prentice Hall, New York (1988)
Meyer, B.: Applying design by contract. J. Comput. 25(10), 40–51 (1992). https://doi.org/10.1109/2.161279
Binder, R.V.: Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison-Wesley, Boston (2000)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)
Sirer, E.G.: Reentrancy woes in smart contracts (2016). http://hackingdistributed.com/2016/07/13/reentrancy-woes/
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
Buterin, V., et al.: A next-generation smart contract and decentralized application platform. White paper (2014)
Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Pearson Education, London (1993)
Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)
Lamport, L.: Computation and state machines, April 2008. https://www.microsoft.com/en-us/research/publication/computation-state-machines/
Newcombe, C.: Why amazon chose TLA+. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 25–39. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-43652-3_3
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)
Mansfield-Devine, S.: The promise of whitelisting. Netw. Secur. 2009(7), 4–6 (2009)
Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)
Grosof, B.N., Poon, T.C.: SweetDeal: representing agent contracts with exceptions using XML rules, ontologies, and process descriptions. In: Proceedings of the 12th International Conference on World Wide Web, pp. 340–349. ACM (2003)
Grosof, B., Poon, T.: SweetDeal: representing agent contracts with exceptions using semantic web rules, ontologies, and process descriptions. Int. J. Electron. Commer. 8(4), 61–97 (2004)
Governatori, G.: Representing business contracts in RuleML. Int. J. Coop. Inf. Syst. 14(02n03), 181–216 (2005)
Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016, pp. 91–96. ACM, New York (2016). https://doi.org/10.1145/2993600.2993611
Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 79–94. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53357-4_6
Bigi, G., Bracciali, A., Meacci, G., Tuosto, E.: Validation of decentralised smart contracts through game theory and formal methods. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 142–161. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25527-9_11
Acknowledgment
This work is supported in part by the Department of Energy and the National Science Foundation under Grant Numbers 1714261.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 International Financial Cryptography Association
About this paper
Cite this paper
Xu, W., Fink, G.A. (2020). Building Executable Secure Design Models for Smart Contracts with Formal Methods. In: Bracciali, A., Clark, J., Pintore, F., Rønne, P., Sala, M. (eds) Financial Cryptography and Data Security. FC 2019. Lecture Notes in Computer Science(), vol 11599. Springer, Cham. https://doi.org/10.1007/978-3-030-43725-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-030-43725-1_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-43724-4
Online ISBN: 978-3-030-43725-1
eBook Packages: Computer ScienceComputer Science (R0)