Building Executable Secure Design Models for Smart Contracts with Formal Methods

  • Weifeng Xu
  • Glenn A. FinkEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11599)


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 work is supported in part by the Department of Energy and the National Science Foundation under Grant Numbers 1714261.


  1. 1.
    Mohanty, D.: BlockChain: From Concept to Execution. Independently published (2018)Google Scholar
  2. 2.
    Finley, K.: A 50 million hack just showed that the dao was all too human (2016).
  3. 3.
    Meyer, B.: Object-Oriented Software Construction, vol. 2. Prentice Hall, New York (1988)Google Scholar
  4. 4.
    Meyer, B.: Applying design by contract. J. Comput. 25(10), 40–51 (1992). Scholar
  5. 5.
    Binder, R.V.: Testing Object-Oriented Systems: Models, Patterns, and Tools. Addison-Wesley, Boston (2000)Google Scholar
  6. 6.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)Google Scholar
  7. 7.
    Sirer, E.G.: Reentrancy woes in smart contracts (2016).
  8. 8.
    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). Scholar
  9. 9.
    Buterin, V., et al.: A next-generation smart contract and decentralized application platform. White paper (2014)Google Scholar
  10. 10.
    Jacobson, I.: Object-Oriented Software Engineering: A Use Case Driven Approach. Pearson Education, London (1993)Google Scholar
  11. 11.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Lamport, L.: Computation and state machines, April 2008.
  13. 13.
    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). Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Mansfield-Devine, S.: The promise of whitelisting. Netw. Secur. 2009(7), 4–6 (2009)CrossRefGoogle Scholar
  16. 16.
    Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)CrossRefGoogle Scholar
  19. 19.
    Governatori, G.: Representing business contracts in RuleML. Int. J. Coop. Inf. Syst. 14(02n03), 181–216 (2005)CrossRefGoogle Scholar
  20. 20.
    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).
  21. 21.
    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). Scholar
  22. 22.
    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). Scholar

Copyright information

© International Financial Cryptography Association 2020

Authors and Affiliations

  1. 1.College of Public AffairsUniversity of BaltimoreBaltimoreUSA
  2. 2.Cyber Security GroupPacific Northwest National LaboratoryRichlandUSA

Personalised recommendations