Skip to main content
SpringerLink
Log in

A Concurrent Perspective on Smart Contracts

  • Conference paper
  • First Online:
Financial Cryptography and Data Security (FC 2017)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 10323))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This requirement stems from the way the underlying Byzantine distributed ledger consensus protocol enables all involved parties to agree on transaction outcomes.

  2. 2.

    That is, unsynchronized concurrent accesses by different threads to a single memory location when at least one of those accesses is a write.

  3. 3.

    A better term would be “uncooperative multitasking” under the circumstances.

  4. 4.

    For reasons that seem rather strange to us, this modulus is computed very inefficiently in lines 315–338 of the contract, which we elide to save space.

  5. 5.

    This is a standard way in Ethereum to ensure that execution of a contract terminates: by supplying it with a limited amount of “gas”, used as a fuel for execution steps.

References

  1. The DAO. https://en.wikipedia.org/wiki/The_DAO_(organization)

  2. BlockKing contract (2016). https://etherscan.io/address/0x3ad14db4e5a658d8d20f8836deabe9d5286f79e1

  3. Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS, pp. 165–175. IEEE Computer Society (1988)

    Google Scholar 

  4. Bertani, T.: Oraclize (2016). http://www.oraclize.it

  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. 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. Brady, E.: Programming and reasoning with algebraic effects and dependent types. In: ICFP, pp. 133–144. ACM (2013)

    Google Scholar 

  8. Brookes, S., O’Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47–65 (2016)

    Google Scholar 

  9. Buterin, V.: Critical update re: DAO vulnerability. https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability

  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. Dimitrova, E.: Writing upgradable contracts in Solidity. https://blog.colony.io/writing-upgradeable-contracts-in-solidity-6743f0eecc88. Accessed 3 Feb 2017

  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

    Chapter  Google Scholar 

  13. Emmi, M., Enea, C.: Symbolic abstract data type inference. In: POPL, pp. 513–525. ACM (2016)

    Google Scholar 

  14. Ethereum Foundation: The Serpent Contract-Oriented Programming Language. https://github.com/ethereum/serpent

  15. Ethereum Foundation: The Solidity Contract-Oriented Programming Language. https://github.com/ethereum/solidity

  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

    Chapter  Google Scholar 

  17. Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison-Wesley, Boston (2006)

    Google Scholar 

  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. Hendler, D., Incze, I., Shavit, N., Tzafrir, M.: Flat combining and the synchronization-parallelism tradeoff. In: SPAA, pp. 355–364 (2010)

    Google Scholar 

  20. Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. M. Kaufmann, Burlington (2008)

    Google Scholar 

  21. Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst. 12(3), 463–492 (1990)

    Article  Google Scholar 

  22. Hirai, Y.: Formalization of Ethereum Virtual Machine in Lem. https://github.com/pirapira/eth-isabelle. Accessed 3 Feb 2017

  23. Jentzsch, C.: The DAO (2016). https://etherscan.io/address/0xffbd72d37d4e7f64939e70b2988aa8924fde48e3

  24. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

    Google Scholar 

  25. Liang, H., Feng, X.: A program logic for concurrent objects under fair scheduling. In: POPL, pp. 385–399. ACM (2016)

    Google Scholar 

  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. Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS, pp. 254–269. ACM (2016)

    Google Scholar 

  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. 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

    Chapter  Google Scholar 

  30. O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comp. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  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. Reitwiessner, C.: Formal Verification for Solidity Contracts. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts. Accessed 3 Feb 2017

  33. Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77–87. ACM (2015)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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. 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. 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. Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014). http://gavwood.com/paper.pdf

Download references

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.

Author information

Authors and Affiliations

  1. University College London, London, UK

    Ilya Sergey

  2. Yale-NUS College and School of Computing, National University of Singapore, Singapore, Singapore

    Aquinas Hobor

Authors
  1. Ilya Sergey
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aquinas Hobor
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ilya Sergey .

Editor information

Editors and Affiliations

  1. Leibniz Universität Hannover, Hannover, Germany

    Michael Brenner

  2. New Jersey Institute of Technology, Newark, New Jersey, USA

    Kurt Rohloff

  3. New York University, New York, New York, USA

    Joseph Bonneau

  4. University of Illinois at Urbana-Champaign, Urbana, Illinois, USA

    Andrew Miller

  5. University of Luxembourg, Luxembourg, Luxembourg

    Peter Y.A. Ryan

  6. University of Melbourne, Parkville, Victoria, Australia

    Vanessa Teague

  7. University of Stirling, Stirling, United Kingdom

    Andrea Bracciali

  8. University of Trento, Trento, Italy

    Massimiliano Sala

  9. University of Trento, Trento, Italy

    Federico Pintore

  10. Agari Inc., San Mateo, California, USA

    Markus Jakobsson

Rights and permissions

Reprints and permissions

Copyright information

© 2017 International Financial Cryptography Association

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Sergey, I., Hobor, A. (2017). A Concurrent Perspective on Smart Contracts. In: Brenner, M., et al. Financial Cryptography and Data Security. FC 2017. Lecture Notes in Computer Science(), vol 10323. Springer, Cham. https://doi.org/10.1007/978-3-319-70278-0_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-70278-0_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-70277-3

  • Online ISBN: 978-3-319-70278-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation