Abstract
The Ethereum platform supports the decentralized execution of smart contracts, i.e. computer programs that transfer digital assets between users. The most common language used to develop these contracts is Solidity, a Javascript-like language which compiles into EVM bytecode, the language actually executed by Ethereum nodes. While much research has addressed the formalisation of the semantics of EVM bytecode, relatively little attention has been devoted to that of Solidity. In this paper we propose a minimal calculus for Solidity contracts, which extends an imperative core with a single primitive to transfer currency and invoke contract procedures. We build upon this formalisation to give semantics to the Ethereum blockchain. We show our calculus expressive enough to reason about some typical quirks of Solidity, like e.g. re-entrancy.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Solidity documentation. solidity.readthedocs.io/en/v0.5.4/ (2019)
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
Bartoletti, M., Galletta, L., Murgia, M.: A minimal core calculus for Solidity contracts. CoRR arXiv:1908.02709 (2019)
Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: secure derivative contracts for ethereum. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 453–467. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_28
Buterin, V.: Ethereum: a next generation smart contract and decentralized application platform. github.com/ethereum/wiki/wiki/White-Paper (2013)
Crafa, S., Pirro, M.D., Zucca, E.: Is solidity solid enough? In: Financial Cryptography Workshops (2019)
Egelund-Müller, B., Elsman, M., Henglein, F., Ross, O.: Automated execution of financial contracts on blockchains. Bus. Inf. Syst. Eng. 59(6), 457–467 (2017)
Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum Virtual Machine. In: IEEE Computer Security Foundations Symposium (CSF), pp. 204–217 (2018)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3), 396–450 (2001)
Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Executable operational semantics of Solidity. CoRR arXiv:1804.01295 (2018)
López-Pintado, O., García-Bañuelos, L., Dumas, M., Weber, I., Ponomarev, A.: Caterpillar: a business process execution engine on the Ethereum blockchain. Practice and Experience, Software (2019)
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM CCS, pp. 254–269 (2016)
Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: Correct-by-design smart contracts for Ethereum. In: Financial Cryptography and Data Security (2019)
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)
Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 478–493. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_30
Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language. CoRR abs/1801.00687 (2018)
Tran, A.B., Lu, Q., Weber, I.: Lorikeet: A model-driven engineering tool for blockchain-based business process execution and asset management. In: BPM, pp. 56–60 (2018)
Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the Solidity programming language. CoRR arXiv:1803.09885 (2018)
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
Acknowledgements
Partially supported by Aut. Reg. Sardinia projects Smart collaborative engineering and Sardcoin, by IMT Lucca project PAI VeriOSS, and by MIUR PON Distributed Ledgers for Secure Open Communities.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Bartoletti, M., Galletta, L., Murgia, M. (2019). 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. DPM CBT 2019 2019. Lecture Notes in Computer Science(), vol 11737. Springer, Cham. https://doi.org/10.1007/978-3-030-31500-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-31500-9_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31499-6
Online ISBN: 978-3-030-31500-9
eBook Packages: Computer ScienceComputer Science (R0)