Advertisement

Temporal Properties of Smart Contracts

  • Ilya SergeyEmail author
  • Amrit Kumar
  • Aquinas Hobor
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11247)

Abstract

Smart contracts—shared stateful reactive objects stored on a blockchain—are widely employed nowadays for mediating exchanges of crypto-currency between multiple untrusted parties. Despite a lot of attention given by the formal methods community to the notion of smart contract correctness, only a few efforts targeted their lifetime properties. In this paper, we focus on reasoning about execution traces of smart contracts. We report on our preliminary results of mechanically verifying some of such properties by embedding a smart contract language into the Coq proof assistant. We also discuss several common scenarios, all of which require multi-step blockchain-based arbitration and thus must be implemented via stateful contracts, and discuss possible temporal specifications of the corresponding smart contract implementations.

References

  1. 1.
  2. 2.
    Alois, J.: Ethereum Parity Hack May Impact ETH 500,000 or \$146 Million (2017). https://www.crowdfundinsider.com/2017/11/124200-ethereum-parity-hack-may-impact-eth-500000-146-million/
  3. 3.
    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_8CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Bansal, K., Koskinen, E., Tripp, O.: Automatic generation of precise and useful commutativity conditions. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 115–132. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_7CrossRefGoogle Scholar
  6. 6.
    Chen, T., Li, X., Luo, X., Zhang, X.: Under-optimized smart contracts devour your money. In: SANER, pp. 442–446. IEEE (2017)Google Scholar
  7. 7.
    Coq Development Team: The Coq Proof Assistant Reference Manual - Version 8.8 (2018). http://coq.inria.fr/
  8. 8.
    Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)MathSciNetCrossRefGoogle Scholar
  9. 9.
    del Castillo, M.: The DAO attack, 16 June 2016Google Scholar
  10. 10.
    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_6CrossRefGoogle Scholar
  11. 11.
    Grossman, S.: Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2(POPL), 48:1–48:28 (2018)Google Scholar
  12. 12.
    Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37(3), 549–587 (1990)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS (2018)Google Scholar
  14. 14.
    Lamport, L.: “Sometime” is sometimes “not never” - on the temporal logic of programs. In: POPL, pp. 174–185. ACM Press (1980)Google Scholar
  15. 15.
    Lamport, L.: The part-time parliament. ACM TOPLAS 16(2), 133–169 (1998)Google Scholar
  16. 16.
    Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42–54. ACM (2006)Google Scholar
  17. 17.
    Mavridou, A., Laszka, A.: Tool demonstration: FSolidM for designing secure ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 270–277. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_11CrossRefGoogle Scholar
  18. 18.
    Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. CoRR, abs/1802.06038 (2018)Google Scholar
  19. 19.
  20. 20.
    Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice-Hall, Upper Saddle River (1987)zbMATHGoogle Scholar
  21. 21.
    Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society (1977)Google Scholar
  22. 22.
    Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. Lisp Symb. Comput. 6(3–4), 289–360 (1993)CrossRefGoogle Scholar
  23. 23.
    Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: 1st Workshop on Trusted Smart Contracts (2017)CrossRefGoogle Scholar
  24. 24.
    Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language (2018). https://arxiv.org/abs/1801.00687
  25. 25.
    Sirer, E.G.: Reentrancy woes in smart contracts, 13 July 2016Google Scholar
  26. 26.
    Solidity: a contract-oriented, high-level language for implementing smart contracts (2018)Google Scholar
  27. 27.
    Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014). https://ethereum.github.io/yellowpaper/paper.pdf

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University College LondonLondonUK
  2. 2.Zilliqa ResearchSingaporeSingapore
  3. 3.Zilliqa ResearchLondonUK
  4. 4.Yale-NUS College and School of ComputingNUSSingaporeSingapore

Personalised recommendations