Model Checking of Solidity Smart Contracts Adopted for Business Processes

Ikram Garfatta; Kaïs Klai; Mohamed Graïet; Walid Gaaloul

doi:10.1007/978-3-030-91431-8_8

Model Checking of Solidity Smart Contracts Adopted for Business Processes

Ikram Garfatta
, Kaïs Klai
, Mohamed Graïet
, Walid Gaaloul

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this paper we propose a formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.

Original language	English
Title of host publication	Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings
Editors	Hakim Hacid, Odej Kao, Massimo Mecella, Naouel Moha, Hye-young Paik
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	116-132
Number of pages	17
ISBN (Print)	9783030914301
DOIs	https://doi.org/10.1007/978-3-030-91431-8_8
Publication status	Published - 1 Jan 2021
Event	19th International Conference on Service-Oriented Computing, ICSOC 2021 - Virtual, online Duration: 22 Nov 2021 → 25 Nov 2021

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13121 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Conference on Service-Oriented Computing, ICSOC 2021
City	Virtual, online
Period	22/11/21 → 25/11/21

Keywords

Blockchain
Business process management
Hierarchical coloured petri nets
Model checking
Smart contracts
Solidity
Temporal properties

Access to Document

10.1007/978-3-030-91431-8_8

Cite this

Garfatta, I., Klai, K., Graïet, M., & Gaaloul, W. (2021). Model Checking of Solidity Smart Contracts Adopted for Business Processes. In H. Hacid, O. Kao, M. Mecella, N. Moha, & H. Paik (Eds.), Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings (pp. 116-132). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13121 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-91431-8_8

Garfatta, Ikram ; Klai, Kaïs ; Graïet, Mohamed et al. / Model Checking of Solidity Smart Contracts Adopted for Business Processes. Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings. editor / Hakim Hacid ; Odej Kao ; Massimo Mecella ; Naouel Moha ; Hye-young Paik. Springer Science and Business Media Deutschland GmbH, 2021. pp. 116-132 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6d9f96b7a0e24cd9ae8c2772186bb109,

title = "Model Checking of Solidity Smart Contracts Adopted for Business Processes",

abstract = "Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this paper we propose a formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.",

keywords = "Blockchain, Business process management, Hierarchical coloured petri nets, Model checking, Smart contracts, Solidity, Temporal properties",

author = "Ikram Garfatta and Ka{\"i}s Klai and Mohamed Gra{\"i}et and Walid Gaaloul",

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 19th International Conference on Service-Oriented Computing, ICSOC 2021 ; Conference date: 22-11-2021 Through 25-11-2021",

year = "2021",

month = jan,

day = "1",

doi = "10.1007/978-3-030-91431-8\_8",

language = "English",

isbn = "9783030914301",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "116--132",

editor = "Hakim Hacid and Odej Kao and Massimo Mecella and Naouel Moha and Hye-young Paik",

booktitle = "Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings",

}

Garfatta, I, Klai, K, Graïet, M & Gaaloul, W 2021, Model Checking of Solidity Smart Contracts Adopted for Business Processes. in H Hacid, O Kao, M Mecella, N Moha & H Paik (eds), Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13121 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 116-132, 19th International Conference on Service-Oriented Computing, ICSOC 2021, Virtual, online, 22/11/21. https://doi.org/10.1007/978-3-030-91431-8_8

Model Checking of Solidity Smart Contracts Adopted for Business Processes. / Garfatta, Ikram; Klai, Kaïs; Graïet, Mohamed et al.
Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings. ed. / Hakim Hacid; Odej Kao; Massimo Mecella; Naouel Moha; Hye-young Paik. Springer Science and Business Media Deutschland GmbH, 2021. p. 116-132 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13121 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Model Checking of Solidity Smart Contracts Adopted for Business Processes

AU - Garfatta, Ikram

AU - Klai, Kaïs

AU - Graïet, Mohamed

AU - Gaaloul, Walid

PY - 2021/1/1

Y1 - 2021/1/1

N2 - Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this paper we propose a formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.

AB - Several features of the Blockchain technology are well aligned with critical issues in the Business Process Management (BPM) field, and yet adopting Blockchain for BPM should not be taken lightly. In fact, the security of smart contracts, which are one of the main elements of the Blockchain that make the integration with BPM possible, has proved to be vulnerable. It is therefore crucial for the protection of the designed business processes to prove the correctness of the smart contracts to be deployed on a blockchain. In this paper we propose a formal approach based on the transformation of Solidity smart contracts, with consideration of the BPM context in which they are used, into a Hierarchical Coloured Petri net. We express a set of smart contract vulnerabilities as temporal logic formulae and use the Helena model checker to, not only detect such vulnerabilities while discerning their exploitability, but also check other temporal-based contract-specific properties.

KW - Blockchain

KW - Business process management

KW - Hierarchical coloured petri nets

KW - Model checking

KW - Smart contracts

KW - Solidity

KW - Temporal properties

U2 - 10.1007/978-3-030-91431-8_8

DO - 10.1007/978-3-030-91431-8_8

M3 - Conference contribution

AN - SCOPUS:85120532074

SN - 9783030914301

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 116

EP - 132

BT - Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings

A2 - Hacid, Hakim

A2 - Kao, Odej

A2 - Mecella, Massimo

A2 - Moha, Naouel

A2 - Paik, Hye-young

PB - Springer Science and Business Media Deutschland GmbH

T2 - 19th International Conference on Service-Oriented Computing, ICSOC 2021

Y2 - 22 November 2021 through 25 November 2021

ER -

Garfatta I, Klai K, Graïet M, Gaaloul W. Model Checking of Solidity Smart Contracts Adopted for Business Processes. In Hacid H, Kao O, Mecella M, Moha N, Paik H, editors, Service-Oriented Computing - 19th International Conference, ICSOC 2021, Proceedings. Springer Science and Business Media Deutschland GmbH. 2021. p. 116-132. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-91431-8_8

Model Checking of Solidity Smart Contracts Adopted for Business Processes

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this