Abstract
The concept of blockchain was developed with the purpose of decentralizing the trade of assets, suppressing the need for intermediaries during this process, as well as achieving a digital trust between parties. A blockchain consists in a public immutable ledger, constituted by chronologically ordered blocks such that each block contains records of a finite number of transactions.
The Ethereum platform, that this paper builds upon, is implemented using a blockchain architecture and introduces the possibility of storing Turing complete programs. These programs, also known as smart contracts, can then be executed using the Ethereum Virtual Machine. Despite its core language being the EVM bytecode, they can also be implemented using a higher-level language that is later compiled to EVM, being Solidity the most used. Among its applications stand out decentralized information storage, tokenization of assets, and digital identity verification.
In this paper we propose a method for formal verification of Solidity smart contracts in Isabelle/HOL. We start from the imperative language and big-step semantics proposed by Schirmer [23], and adapt it to describe a rich subset of Solidity, implementing it using the Isabelle/HOL proof assistant. Then, we describe the properties about programs using Hoare logic, and present a proof system for the language, for which results on soundness and (relative) completeness are obtained.
Finally, we describe the verification of an electronic voting smart contract, which illustrates the degree of proof complexity that can be achieved using this method. Examples of smart contracts containing overflow and reentrancy vulnerabilities are also presented.
Partially supported by Programa Operacional Competitividade e Internacionalização (COMPETE 2020), Fundo Europeu de Desenvolvimento Regional (FEDER) through Programa Operacional Regional de Lisboa (Lisboa 2020), Project BLOCH - LISBOA-01-0247-FEDER-033823, and Fundação para a Ciência e Tecnologia (FCT) project UID/EEA/50008/2019.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In: CPP 2018, pp. 66–77. ACM (2018)
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.) DPM/CBT 2019. LNCS, vol. 11737, pp. 233–243. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31500-9_15
Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: PLAS 2016, pp. 91–96. ACM (2016)
Buterin, V.: Ethereum: a next-generation cryptocurrency and decentralized application platform
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70–90 (1978)
Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer, Heidelberg (1990). https://doi.org/10.1007/978-1-4612-3228-5
Frade, M.J., Pinto, J.S.: Verification conditions for source-level imperative programs. Comput. Sci. Rev. 5(3), 252–277 (2011)
Grishchenko, I., Maffei, M., Schneidewind, C.: Foundations and tools for the static analysis of Ethereum smart contracts. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 51–78. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_4
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
Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: CSF 2018, pp. 204–217. IEEE Computer Society (2018)
Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_33
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102–116. Springer, Heidelberg (1971). https://doi.org/10.1007/BFb0059696
Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Semantic understanding of smart contracts: executable operational semantics of solidity. In: SP 2020, pp. 1265–1282. IEEE Computer Society (2020)
Lincoln, P., Mitchell, J., Scedrov, A., Shankar, N.: Decision problems for propositional linear logic. Ann. Pure Appl. Logic 56(1), 239–311 (1992)
Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Linear logic proof games and optimization. Bull. Symbolic Logic 2(3), 322–338 (1996)
Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM CCS 2016, pp. 254–269. ACM (2016)
Mateus, P., Mitchell, J., Scedrov, A.: Composition of cryptographic protocols in a probabilistic polynomial-time process calculus. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 327–349. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45187-7_22
Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci. 353(1), 118–164 (2006)
Mythril. https://github.com/ConsenSys/mythril
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2009)
Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: ACSAC 2018, pp. 653–663. ACM (2018)
Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technical University Munich, Germany (2006)
Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., Bünzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: ACM CCS 2018, pp. 67–82. ACM (2018)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper (2019)
Zakrzewski, J.: Towards verification of Ethereum smart contracts: a formalization of core of solidity. In: Piskac, R., Rümmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 229–247. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03592-1_13
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Ribeiro, M., Adão, P., Mateus, P. (2020). Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL. In: Nigam, V., et al. Logic, Language, and Security. Lecture Notes in Computer Science(), vol 12300. Springer, Cham. https://doi.org/10.1007/978-3-030-62077-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-62077-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-62076-9
Online ISBN: 978-3-030-62077-6
eBook Packages: Computer ScienceComputer Science (R0)