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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
Bit strings are modelled using Isabelle’s word library [14].
- 4.
- 5.
References
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
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
Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: A survey. Pervasive Mob. Comput. 67, 101227 (2020)
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)
Bahrynovska, T.: History of Ethereum Security Vulnerabilities, Hacks and Their Fixes (2017)
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
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
Bhargavan, K., et al.: Formal verification of smart contracts: Short paper. In: Programming Languages and Analysis for Security, pp. 91–96. PLAS, ACM (2016)
Brecknell, M., et al.: Autocorres2. Archive of Formal Proofs (April 2024)
Chavez-Dreyfuss, G.: Sweden tests blockchain technology for land registry (2016)
CipherTrace: Cryptocurrency crime and anti-money laundering report. Tech. rep., Mastercard (2021)
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
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
Dawson, J.: Isabelle theories for machine words. ENTCS 250(1), 55–70 (2009), int. Workshop on Automated Verification of Critical Systems (AVoCS 2007)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (aug 1975)
Foundation, E.: Solidity semantic reference test suite (version 0.8.25). https://github.com/ethereum/solidity/tree/v0.8.25/test/libsolidity/semanticTests (2023)
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
Haftmann, F., Bulwahn, L.: Code generation from Isabelle/HOL theories (2023). http://isabelle.in.tum.de/doc/codegen.pdf
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
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
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)
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
Kelly, J.: Banks adopting blockchain ’dramatically faster’ than expected: IBM (2016)
Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)
Krauss, A.: Recursive definitions of monadic functions. ENTCS 43, 1–13 (2010)
Lammich, P., Wimmer, S.: IMP2 – simple program verification in Isabelle/HOL. Archive of Formal Proofs (2019)
Llama, D.: TVL breakdown by smart contract language (2024). https://defillama.com/languages
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
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)
Marmsoler, D., Brucker, A.D.: Isabelle/Solidity: a deep embedding of solidity in Isabelle/HOL. Archive of Formal Proofs (July 2022)
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)
Matichuk, D., Murray, T., Wenzel, M.: Eisbach: a proof method language for isabelle. J. Autom. Reason. 56, 261–282 (2016)
Nakamoto, S.: Bitcoin: A Peer-to-Peer Electronic Cash System (2008)
BBC News: Hackers steal \$600m in major cryptocurrency heist (2021)
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
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects Comput. 10(2), 171–186 (1998)
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
Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006)
Schirmer, N.: A sequential imperative programming language syntax, semantics, hoare logics and verification environment. Archive of Formal Proofs (Feb 2008)
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)
Tuong, F., Wolff, B.: Clean – an abstract imperative programming language and its theory. Archive of Formal Proofs (Oct 2019)
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
Wenzel, M.: The Isabelle/Isar implementation (2013)
Winskel, G.: The formal semantics of programming languages: an introduction. MIT press (1993)
YCharts.com: Ethereum transactions per day (2024)
Yurcan, B.: How blockchain fits into the future of digital identity (2016)
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2025 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
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)