Advertisement

A Concurrent Perspective on Smart Contracts

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

Abstract

In this paper, we explore remarkable similarities between multi-transactional behaviors of smart contracts in cryptocurrencies such as Ethereum and classical problems of shared-memory concurrency. We examine two real-world examples from the Ethereum blockchain and analyzing how they are vulnerable to bugs that are closely reminiscent to those that often occur in traditional concurrent programs. We then elaborate on the relation between observable contract behaviors and well-studied concurrency topics, such as atomicity, interference, synchronization, and resource ownership. The described contracts-as-concurrent-objects analogy provides deeper understanding of potential threats for smart contracts, indicate better engineering practices, and enable applications of existing state-of-the-art formal verification techniques.

Notes

Acknowledgements

Sergey’s research is supported by EPSRC grant EP/P009271/1. Hobor’s research is funded by Yale-NUS College R-607-265-045-121.

References

  1. 1.
  2. 2.
  3. 3.
    Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS, pp. 165–175. IEEE Computer Society (1988)Google Scholar
  4. 4.
    Bertani, T.: Oraclize (2016). http://www.oraclize.it
  5. 5.
    Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-Béguelin, S.: Formal verification of smart contracts: short paper. In: PLAS, pp. 91–96. ACM (2016)Google Scholar
  6. 6.
    Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259–270. ACM (2005)Google Scholar
  7. 7.
    Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: ICFP, pp. 133–144. ACM (2013)Google Scholar
  8. 8.
    Brookes, S., O’Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47–65 (2016)Google Scholar
  9. 9.
    Buterin, V.: Critical update re: DAO vulnerability. https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability
  10. 10.
    Dechev, D., Pirkelbauer, P., Stroustrup, B.: Understanding and effectively preventing the ABA problem in descriptor-based lock-free designs. In: ISORC, pp. 185–192. IEEE Computer Society (2010)Google Scholar
  11. 11.
    Dimitrova, E.: Writing upgradable contracts in Solidity. https://blog.colony.io/writing-upgradeable-contracts-in-solidity-6743f0eecc88. Accessed 3 Feb 2017
  12. 12.
    Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14107-2_24 CrossRefGoogle Scholar
  13. 13.
    Emmi, M., Enea, C.: Symbolic abstract data type inference. In: POPL, pp. 513–525. ACM (2016)Google Scholar
  14. 14.
    Ethereum Foundation: The Serpent Contract-Oriented Programming Language. https://github.com/ethereum/serpent
  15. 15.
    Ethereum Foundation: The Solidity Contract-Oriented Programming Language. https://github.com/ethereum/solidity
  16. 16.
    Filliâtre, J.-C., Paskevich, A.: Why3—where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_8 CrossRefGoogle Scholar
  17. 17.
    Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison-Wesley, Boston (2006)Google Scholar
  18. 18.
    Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: POPL, pp. 16–28. ACM (2009)Google Scholar
  19. 19.
    Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Flat combining and the synchronization-parallelism tradeoff. In: SPAA, pp. 355–364 (2010)Google Scholar
  20. 20.
    Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. M. Kaufmann, Burlington (2008)Google Scholar
  21. 21.
    Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst. 12(3), 463–492 (1990)CrossRefGoogle Scholar
  22. 22.
    Hirai, Y.: Formalization of Ethereum Virtual Machine in Lem. https://github.com/pirapira/eth-isabelle. Accessed 3 Feb 2017
  23. 23.
  24. 24.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)Google Scholar
  25. 25.
    Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385–399. ACM (2016)Google Scholar
  26. 26.
    Lin, Y., Dig, D.: CHECK-THEN-ACT misuse of java concurrent collections. In: ICST, pp. 164–173. IEEE Computer Society (2013)Google Scholar
  27. 27.
    Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS, pp. 254–269. ACM (2016)Google Scholar
  28. 28.
    Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. In: ICFP, pp. 175–188. ACM (2014)Google Scholar
  29. 29.
    Nanevski, A., Ley-Wild, R., Sergey, I., Delbianco, G.A.: Communicating state transition systems for fine-grained concurrent resources. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 290–310. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54833-8_16 CrossRefGoogle Scholar
  30. 30.
    O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comp. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Pettersson, J., Edström, R.: Safer smart contracts through type-driven development. Master’s thesis, Chalmers University of Technology, Department of Computer Science and Engineering, Sweden (2016)Google Scholar
  32. 32.
    Reitwiessner, C.: Formal Verification for Solidity Contracts. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts. Accessed 3 Feb 2017
  33. 33.
    Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77–87. ACM (2015)Google Scholar
  34. 34.
    Svendsen, K., Birkedal, L., Parkinson, M.: Modular reasoning about separation of concurrent data structures. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 169–188. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_11 CrossRefGoogle Scholar
  35. 35.
    Swamy, N.,Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: ICFP, pp. 266–278. ACM (2011)Google Scholar
  36. 36.
    Swamy, N., Hritcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P., Kohlweiss, M., Zinzindohoue, J.K., Béguelin, S.Z.: Dependent types and multi-monadic effects in F\(^{*}\). In: POPL, pp. 256–270. ACM (2016)Google Scholar
  37. 37.
    Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377–390. ACM (2013)Google Scholar
  38. 38.
    Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014). http://gavwood.com/paper.pdf

Copyright information

© International Financial Cryptography Association 2017

Authors and Affiliations

  1. 1.University College LondonLondonUK
  2. 2.Yale-NUS College and School of ComputingNational University of SingaporeSingaporeSingapore

Personalised recommendations