[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Secure Smart Contracts with Isabelle/Solidity

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2024)

Abstract

Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. The framework consists of a novel formalization of the Solidity storage model, a shallow embedding of Solidity expressions and statements, an implementation of Isabelle commands to support a user in specifying Solidity smart contracts, and a verification condition generator to support a user in the verification. Compliance of the semantics is tested by a set of unit tests and the approach is evaluated by means of three case studies. Our results show that the framework can be used to verify even complex contracts with reasonable effort. Moreover, they show that the shallow embedding significantly reduces the verification effort compared to an alternative approach based on a deep embedding.

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

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 49.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 59.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/dmarmsoler/isabelle-solidity-shallow.

  2. 2.

    https://docs.soliditylang.org/en/v0.8.25/.

  3. 3.

    Bit strings are modelled using Isabelle’s word library [14].

  4. 4.

    https://verifythis.github.io/02casino/.

  5. 5.

    https://docs.soliditylang.org/en/v0.8.25/solidity-by-example.html#voting.

References

  1. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification–the KeY book, vol. LNCS 10001. Springer (2016). https://doi.org/10.1007/978-3-319-49812-6

  2. Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20–30, 2020, Proceedings, Part III, pp. 9–24. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-61467-6_2

    Chapter  Google Scholar 

  3. Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: A survey. Pervasive Mob. Comput. 67, 101227 (2020)

    Article  Google Scholar 

  4. Azaria, A., Ekblaw, A., Vieira, T., Lippman, A.: MedRec: using blockchain for medical data access and permission management. In: 2016 2nd International Conference on Open and Big Data (OBD), pp. 25–30 (2016)

    Google Scholar 

  5. Bahrynovska, T.: History of Ethereum Security Vulnerabilities, Hacks and Their Fixes (2017)

    Google Scholar 

  6. Bartoletti, M., Galletta, L., Murgia, M.: A minimal core calculus for solidity contracts. In: Pérez-Solà, C., Navarro-Arribas, G., Biryukov, A., Garcia-Alfaro, J. (eds.) Data Privacy Management, Cryptocurrencies and Blockchain Technology: ESORICS 2019 International Workshops, DPM 2019 and CBT 2019, Luxembourg, September 26–27, 2019, Proceedings, pp. 233–243. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-31500-9_15

    Chapter  Google Scholar 

  7. Berghofer, S., Wenzel, M.: Inductive datatypes in HOL — lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics, pp. 19–36. Springer Berlin Heidelberg, Berlin, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_3

    Chapter  Google Scholar 

  8. Bhargavan, K., et al.: Formal verification of smart contracts: Short paper. In: Programming Languages and Analysis for Security, pp. 91–96. PLAS, ACM (2016)

    Google Scholar 

  9. Brecknell, M., et al.: Autocorres2. Archive of Formal Proofs (April 2024)

    Google Scholar 

  10. Chavez-Dreyfuss, G.: Sweden tests blockchain technology for land registry (2016)

    Google Scholar 

  11. CipherTrace: Cryptocurrency crime and anti-money laundering report. Tech. rep., Mastercard (2021)

    Google Scholar 

  12. Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, pp. 167–182. Springer Berlin Heidelberg, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71067-7_16

    Chapter  Google Scholar 

  13. Crafa, S., Di Pirro, M., Zucca, E.: Is solidity solid enough? In: Bracciali, A., Clark, J., Pintore, F., Rønne, P.B., Sala, M. (eds.) Financial Cryptography and Data Security: FC 2019 International Workshops, VOTING and WTSC, St. Kitts, St. Kitts and Nevis, February 18–22, 2019, Revised Selected Papers, pp. 138–153. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-43725-1_11

    Chapter  Google Scholar 

  14. Dawson, J.: Isabelle theories for machine words. ENTCS 250(1), 55–70 (2009), int. Workshop on Automated Verification of Critical Systems (AVoCS 2007)

    Google Scholar 

  15. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (aug 1975)

    Google Scholar 

  16. Foundation, E.: Solidity semantic reference test suite (version 0.8.25). https://github.com/ethereum/solidity/tree/v0.8.25/test/libsolidity/semanticTests (2023)

  17. Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, pp. 99–115. Springer Berlin Heidelberg, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_8

    Chapter  Google Scholar 

  18. Haftmann, F., Bulwahn, L.: Code generation from Isabelle/HOL theories (2023). http://isabelle.in.tum.de/doc/codegen.pdf

  19. Hajdu, Á., Jovanović, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA, July 13–14, 2019, Revised Selected Papers, pp. 161–179. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-41600-3_11

    Chapter  Google Scholar 

  20. Hajdu, Á., Jovanović, D.: SMT-friendly formalization of the solidity memory model. In: ESOP 2020. LNCS, vol. 12075, pp. 224–250. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_9

    Chapter  Google Scholar 

  21. Jiao, J., Kan, S., Lin, S.W., Sanan, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: executable operational semantics of Solidity. In: SP, pp. 1695–1712. IEEE (2020)

    Google Scholar 

  22. Jiao, J., Lin, S.-W., Sun, J.: A generalized formal semantic framework for smart contracts. In: Wehrheim, H., Cabot, J. (eds.) Fundamental Approaches to Software Engineering: 23rd International Conference, FASE 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, pp. 75–96. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-45234-6_4

    Chapter  Google Scholar 

  23. Kelly, J.: Banks adopting blockchain ’dramatically faster’ than expected: IBM (2016)

    Google Scholar 

  24. Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)

    Article  Google Scholar 

  25. Krauss, A.: Recursive definitions of monadic functions. ENTCS 43, 1–13 (2010)

    Google Scholar 

  26. Lammich, P., Wimmer, S.: IMP2 – simple program verification in Isabelle/HOL. Archive of Formal Proofs (2019)

    Google Scholar 

  27. Llama, D.: TVL breakdown by smart contract language (2024). https://defillama.com/languages

  28. Marmsoler, D., Brucker, A.D.: A denotational semantics of Solidity in Isabelle/HOL. In: Calinescu, R., Pasareanu, C. (eds.) SEFM. LNCS 13085, Springer (2021). https://doi.org/10.1007/978-3-030-92124-8_23

  29. Marmsoler, D., Brucker, A.D.: Conformance testing of formal semantics using grammar-based fuzzing. In: Kovacs, L., Meinke, K. (eds.) Tests And Proofs. LNCS 13361, Springer-Verlag (2022)

    Google Scholar 

  30. Marmsoler, D., Brucker, A.D.: Isabelle/Solidity: a deep embedding of solidity in Isabelle/HOL. Archive of Formal Proofs (July 2022)

    Google Scholar 

  31. Marmsoler, D., Thornton, B.: SSCalc: a calculus for solidity smart contracts. In: Ferreira, C., Willemse, T.A.C. (eds.) Software Engineering and Formal Methods, pp. 184–204. Springer, Cham (2023)

    Chapter  Google Scholar 

  32. Matichuk, D., Murray, T., Wenzel, M.: Eisbach: a proof method language for isabelle. J. Autom. Reason. 56, 261–282 (2016)

    Article  MathSciNet  Google Scholar 

  33. Nakamoto, S.: Bitcoin: A Peer-to-Peer Electronic Cash System (2008)

    Google Scholar 

  34. BBC News: Hackers steal \$600m in major cryptocurrency heist (2021)

    Google Scholar 

  35. Nguyen, T.D., Pham, L.H., Sun, J., Le, Q.L.: An idealist’s approach for smart contract correctness. In: Li, Y., Tahar, S. (eds.) Formal Methods and Software Engineering. pp. 11–28. Springer (2023). https://doi.org/10.1007/978-981-99-7584-6_2

  36. Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects Comput. 10(2), 171–186 (1998)

    Article  Google Scholar 

  37. Ribeiro, M., Adão, P., Mateus, P.: Formal verification of ethereum smart contracts using Isabelle/HOL. In: Nigam, V., Ban Kirigin, T., Talcott, C., Guttman, J., Kuznetsov, S., Thau Loo, B., Okada, M. (eds.) Logic, Language, and Security. LNCS, vol. 12300, pp. 71–97. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-62077-6_7

    Chapter  Google Scholar 

  38. Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006)

    Google Scholar 

  39. Schirmer, N.: A sequential imperative programming language syntax, semantics, hoare logics and verification environment. Archive of Formal Proofs (Feb 2008)

    Google Scholar 

  40. Tolmach, P., Li, Y., Lin, S.W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7) (2021)

    Google Scholar 

  41. Tuong, F., Wolff, B.: Clean – an abstract imperative programming language and its theory. Archive of Formal Proofs (Oct 2019)

    Google Scholar 

  42. Wadler, P.: Monads for functional programming. In: Broy, M. (ed.) Program Design Calculi, pp. 233–264. Springer (1993). https://doi.org/10.1007/978-3-662-02880-3_8

  43. Wenzel, M.: The Isabelle/Isar implementation (2013)

    Google Scholar 

  44. Winskel, G.: The formal semantics of programming languages: an introduction. MIT press (1993)

    Google Scholar 

  45. YCharts.com: Ethereum transactions per day (2024)

    Google Scholar 

  46. Yurcan, B.: How blockchain fits into the future of digital identity (2016)

    Google Scholar 

Download references

Acknowledgments

We thank the anonymous reviewers of SEFM 2024 for their careful reading and constructive comments to improve earlier versions of this paper. This work was supported by the Engineering and Physical Sciences Research Council [grant number EP/X027619/1].

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Diego Marmsoler .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Marmsoler, D., Ahmed, A., Brucker, A.D. (2025). Secure Smart Contracts with Isabelle/Solidity. In: Madeira, A., Knapp, A. (eds) Software Engineering and Formal Methods. SEFM 2024. Lecture Notes in Computer Science, vol 15280. Springer, Cham. https://doi.org/10.1007/978-3-031-77382-2_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-77382-2_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-77381-5

  • Online ISBN: 978-3-031-77382-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics