@inproceedings{5570eb5dcdba41148255b60e44615b86,
title = "A Solidity-to-CPN Approach Towards Formal Verification of Smart Contracts",
abstract = "While Blockchains can open intriguing opportunities of research in many application contexts, they come with the risk of bringing new unconventional problems. In fact, because of the monetary value they hold, Blockchains have been subject to many attacks. Smart contracts, which are at the core of second-generation Blockchains, have been proven to be the origin of such attacks due to the exploitable vulnerabilities their code may hold. It is therefore an essential requirement to prove the correctness of the smart contracts to be deployed on a Blockchain to ensure its protection. The existing approaches have been focusing on targeting generic vulnerabilities like reentrancy, without offering the possibility to check temporal-based contract-specific properties. In this paper, we aim to address smart contracts verification while supporting such properties. We propose and implement a transformation of Solidity smart contracts into Coloured Petri nets and investigate the capability of existing model checking tools to check specific temporal properties of the formally modeled contract.",
keywords = "Blockchain, Coloured Petri Nets, Formal Verification, Smart Contract, Solidity, Temporal properties",
author = "Ikram Garfatta and Kais Klai and Mohamed Graiet and Walid Gaaloul",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 30th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2021 ; Conference date: 27-10-2021 Through 29-10-2021",
year = "2021",
month = jan,
day = "1",
doi = "10.1109/WETICE53228.2021.00024",
language = "English",
series = "Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE",
publisher = "IEEE Computer Society",
pages = "69--74",
booktitle = "Proceedings - 2021 IEEE 30th International Conference on Enabling Technologies",
}