Skip to main content
SpringerLink
Log in

Contracts over Smart Contracts: Recovering from Violations Dynamically

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (ISoLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11247))

Included in the following conference series:

Abstract

Smart contracts which enforce behaviour between parties have been hailed as a new way of regulating business, particularly on public distributed ledger technologies which ensure the immutability of smart contracts, and can do away with points of trust. Many such platforms, including Ethereum, come with a virtual machine on which smart contracts are executed, described in an imperative manner. Given the critical nature of typical smart contract applications, their bugs and vulnerabilities have proved to be particularly costly. In this paper we argue how dynamic analysis can be used not only to identify errors in the contracts, but also to support recovery from such errors. Furthermore, contract immutability means that code cannot be easily fixed upon discovering a problem. To address this issue, we also present a specification-driven approach, allowing developers to promise behavioural properties via smart contracts, but still allowing them to update the code which implements the specification in a safe manner.

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.

    Needless to say, this terminology has been used in a wide variety of contexts, and not all usages correspond to the neatly compartmentalised descriptions we give. In case of disagreement with our use of terminology, kindly read the rest of the paper replacing the terms with your preferred ones.

  2. 2.

    Since DLTs vary in design and in their take on smart contracts, we particularly focus on the Ethereum blockchain platform [27], even if many of the ideas presented herewith can be extended for other takes on smart contracts and other DLTs.

  3. 3.

    Atomic transactions rely on locking to isolate themselves from external observation—which is impractical with transactions which have a long lifespan. If the environment reacts to intermediate results after which the transaction fails, then the transaction cannot simply be wiped out. Rather, the effects it had on the environment in its lifetime need to be managed. This is done through compensations.

References

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

    Chapter  Google Scholar 

  2. 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. ACM, New York (2016)

    Google Scholar 

  3. Chen, F., Rosu, G.: Towards monitoring-oriented programming: a paradigm combining specification and implementation. Electr. Notes Theor. Comput. Sci. 89(2), 108–127 (2003)

    Article  Google Scholar 

  4. Chen, F., Roşu, G.: Java-MOP: a monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_36

    Chapter  MATH  Google Scholar 

  5. Colombo, C., Pace, G.J.: Recovery within long-running transactions. ACM Comput. Surv. 45(3), 28:1–28:35 (2013)

    Article  Google Scholar 

  6. Colombo, C., Pace, G.J.: Comprehensive monitor-oriented compensation programming. In: Proceedings 11th International Workshop on Formal Engineering approaches to Software Components and Architectures, FESCA 2014, Grenoble, France, 12 April 2014, pp. 47–61 (2014)

    Google Scholar 

  7. Colombo, C., Pace, G.J., Abela, P.: Safer asynchronous runtime monitoring using compensations. Form. Methods Syst. Des. 41(3), 269–294 (2012)

    Article  Google Scholar 

  8. Colombo, C., Pace, G.J., Schneider, G.: LARVA—safer monitoring of real-time Java programs (tool paper). In: IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, Hanoi, Vietnam, 23–27 November 2009 (2009)

    Google Scholar 

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

    Chapter  Google Scholar 

  10. Ellul, J., Pace, G.J.: Runtime verification of ethereum smart contracts. In: Workshop on Blockchain Dependability (WBD), in conjunction with 14th European Dependable Computing Conference (EDCC) (2018)

    Google Scholar 

  11. Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification: Introductory and Advanced Topics. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_4

    Chapter  Google Scholar 

  12. Fröwis, M., Böhme, R.: In code we trust?—measuring the control flow immutability of all smart contracts deployed on ethereum. In: Garcia-Alfaro, J., Navarro-Arribas, G., Hartenstein, H., Herrera-Joancomartí, J. (eds.) ESORICS/DPM/CBT -2017. LNCS, vol. 10436, pp. 357–372. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67816-0_20

    Chapter  Google Scholar 

  13. Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7(5), 323–334 (1992)

    Article  Google Scholar 

  14. Garcia-Molina, H., Gawlick, D., Klein, J., Kleissner, K., Salem, K.: Modeling long-running activities as nested sagas. IEEE Data Eng. Bull. 14(1), 14–18 (1991)

    Google Scholar 

  15. Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89722-6_10

    Chapter  Google Scholar 

  16. Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.J.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1–16:58 (2012)

    Article  Google Scholar 

  17. Hayes, I., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–338 (1989)

    Article  Google Scholar 

  18. Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine. Technical report (2017)

    Google Scholar 

  19. Idelberger, F., Governatori, G., Riveret, R., Sartor, G.: Evaluation of logic-based smart contracts for blockchain systems. In: Alferes, J.J.J., Bertossi, L., Governatori, G., Fodor, P., Roman, D. (eds.) RuleML 2016. LNCS, vol. 9718, pp. 167–183. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-42019-6_11

    Chapter  Google Scholar 

  20. Lessig, L.: Code 2.0, 2nd edn. CreateSpace, Paramount (2009)

    Google Scholar 

  21. Luu, L., Chu, D.-H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24–28 October 2016, pp. 254–269 (2016)

    Google Scholar 

  22. Meyer, B.: Design by contract: the Eiffel method. In: TOOLS (26), p. 446. IEEE Computer Society (1998)

    Google Scholar 

  23. Pratt, V.: Anatomy of the pentium bug. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) CAAP 1995. LNCS, vol. 915, pp. 97–107. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-59293-8_189

    Chapter  Google Scholar 

  24. Randell, B., Lee, P.A., Treleaven, P.C.: Reliability issues in computing system design. ACM Comput. Surv. 10(2), 123–165 (1978)

    Article  Google Scholar 

  25. Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: Brenner, M. (ed.) FC 2017. LNCS, vol. 10323, pp. 478–493. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_30

    Chapter  Google Scholar 

  26. Szabo, N.: Smart contracts: building blocks for digital markets. Extropy (16) (1996)

    Google Scholar 

  27. Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1–32 (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre for Distributed Ledger Technologies, University of Malta, Msida, Malta

    Joshua Ellul & Gordon J. Pace

  2. Department of Computer Science, University of Malta, Msida, Malta

    Christian Colombo, Joshua Ellul & Gordon J. Pace

Authors
  1. Christian Colombo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joshua Ellul
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Gordon J. Pace
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gordon J. Pace .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Colombo, C., Ellul, J., Pace, G.J. (2018). Contracts over Smart Contracts: Recovering from Violations Dynamically. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03427-6_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03426-9

  • Online ISBN: 978-3-030-03427-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation