Abstract
With its span of applications widening by the day, the technology of Blockchain has been gaining more interest in different domains. It has intrigued many investors, but also numerous malicious users who have put different Blockchain platforms under attack. It is therefore an inescapable necessity to guarantee the correctness of smart contracts as they are the core of Blockchain applications. Existing verification approaches, however, focus on targeting particular vulnerabilities, seldom supporting the verification of domain-specific properties.
In this paper, we propose a translation of Solidity smart contracts into CPNs (Coloured Petri nets) and investigate the capability of CPN Tools to verify CTL (Computation Tree Logic) properties.
Supervised by Kaïs Klai, University Sorbonne Paris North, LIPN UMR CNRS 7030, Villetaneuse, France, and Mahamed Graïet Higher Institute for Computer Science and Mathematics, University of Monastir, Monastir, Tunisia and National School for Statistics and Information Analysis, Rennes, France.
Co-directed by Walid Gaaloul, Institut Mines-Télécom,Télécom SudParis, UMR 5157, SAMOVAR, Paris, France.
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
Similar content being viewed by others
References
Solidity documentation. https://solidity.readthedocs.io/en/latest/
Formal verification for solidity contracts - ethereum community forum, October 2015. https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts
Amani, S., Bégel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in isabelle/hol. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 66–77 (2018)
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@CCS 2016, Vienna, Austria, 24 October 2016, pp. 91–96 (2016)
Chen, T., Li, X., Luo, X., Zhang, X.: Under-optimized smart contracts devour your money. In: IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER 2017, Austria, 20–24 February 2017, pp. 442–446 (2017)
Evangelista, S.: High level petri nets analysis with helena. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 455–464. Springer, Heidelberg (2005). https://doi.org/10.1007/11494744_26
Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 1st edn. Springer, Heidelberg (2009). https://doi.org/10.1007/b9511210.1007/b95112
Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18–21 February 2018 (2018)
Klai, K., Poitrenaud, D.: MC-SOG: an LTL model checker based on symbolic observation graphs. In: 29th International Conference Applications and Theory of Petri Nets, PETRI NETS 2008, China, 23–27 June, Proceedings. pp. 288–306 (2008)
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. Softw. Pract. Exp. 49(7), 1162–1193 (2019)
Luu, L., Chu, D., 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, p. 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 - 23rd International Conference, St. Kitts and Nevis, 18–22 February 2019, p. 446–465 2019)
Mendling, J., Weber, I.: Blockchains for business process management - challenges and opportunities. EMISA Forum 38(1), 22–23 (2018)
Torres, C.F., Schütte, J., State, R.: Osiris: hunting for integer bugs in ethereum smart contracts. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, PR, USA, 03–07 December 2018, p. 664–676 (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Garfatta, I., Klai, K., Graïet, M., Gaaloul, W. (2021). Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. In: Hacid, H., et al. Service-Oriented Computing – ICSOC 2020 Workshops. ICSOC 2020. Lecture Notes in Computer Science(), vol 12632. Springer, Cham. https://doi.org/10.1007/978-3-030-76352-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-76352-7_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-76351-0
Online ISBN: 978-3-030-76352-7
eBook Packages: Computer ScienceComputer Science (R0)