Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach

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

doi:10.1007/978-3-030-76352-7_7

Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach

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

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

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.

Original language	English
Title of host publication	Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings
Editors	Hakim Hacid, Fatma Outay, Hye-young Paik, Amira Alloum, Marinella Petrocchi, Mohamed Reda Bouadjenek, Amin Beheshti, Xumin Liu, Abderrahmane Maaradji
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	47-53
Number of pages	7
ISBN (Print)	9783030763510
DOIs	https://doi.org/10.1007/978-3-030-76352-7_7
Publication status	Published - 1 Jan 2021
Event	AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events held in conjunction with 18th International Conference on Service-Oriented Computing, ICSOC 2020 - Virtual, Online Duration: 14 Dec 2020 → 17 Dec 2020

Publication series

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

Conference

Conference	AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events held in conjunction with 18th International Conference on Service-Oriented Computing, ICSOC 2020
City	Virtual, Online
Period	14/12/20 → 17/12/20

Keywords

Blockchain
CTL properties
Coloured Petri nets
Formal verification
Smart contract
Solidity

Access to Document

10.1007/978-3-030-76352-7_7

Cite this

Garfatta, I., Klai, K., Graïet, M., & Gaaloul, W. (2021). Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. In H. Hacid, F. Outay, H. Paik, A. Alloum, M. Petrocchi, M. R. Bouadjenek, A. Beheshti, X. Liu, & A. Maaradji (Eds.), Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings (pp. 47-53). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12632 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-76352-7_7

Garfatta, Ikram ; Klai, Kaïs ; Graïet, Mahamed et al. / Blockchain-Based Business Processes : A Solidity-to-CPN Formal Verification Approach. Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings. editor / Hakim Hacid ; Fatma Outay ; Hye-young Paik ; Amira Alloum ; Marinella Petrocchi ; Mohamed Reda Bouadjenek ; Amin Beheshti ; Xumin Liu ; Abderrahmane Maaradji. Springer Science and Business Media Deutschland GmbH, 2021. pp. 47-53 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d47ce6854e1e4ced88c7fe5f28a09755,

title = "Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach",

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.",

keywords = "Blockchain, CTL properties, Coloured Petri nets, Formal verification, Smart contract, Solidity",

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

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events held in conjunction with 18th International Conference on Service-Oriented Computing, ICSOC 2020 ; Conference date: 14-12-2020 Through 17-12-2020",

year = "2021",

month = jan,

day = "1",

doi = "10.1007/978-3-030-76352-7\_7",

language = "English",

isbn = "9783030763510",

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 = "47--53",

editor = "Hakim Hacid and Fatma Outay and Hye-young Paik and Amira Alloum and Marinella Petrocchi and Bouadjenek, \{Mohamed Reda\} and Amin Beheshti and Xumin Liu and Abderrahmane Maaradji",

booktitle = "Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings",

}

Garfatta, I, Klai, K, Graïet, M & Gaaloul, W 2021, Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. in H Hacid, F Outay, H Paik, A Alloum, M Petrocchi, MR Bouadjenek, A Beheshti, X Liu & A Maaradji (eds), Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12632 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 47-53, AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events held in conjunction with 18th International Conference on Service-Oriented Computing, ICSOC 2020, Virtual, Online, 14/12/20. https://doi.org/10.1007/978-3-030-76352-7_7

Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. / Garfatta, Ikram; Klai, Kaïs; Graïet, Mahamed et al.
Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings. ed. / Hakim Hacid; Fatma Outay; Hye-young Paik; Amira Alloum; Marinella Petrocchi; Mohamed Reda Bouadjenek; Amin Beheshti; Xumin Liu; Abderrahmane Maaradji. Springer Science and Business Media Deutschland GmbH, 2021. p. 47-53 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12632 LNCS).

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

TY - GEN

T1 - Blockchain-Based Business Processes

T2 - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events held in conjunction with 18th International Conference on Service-Oriented Computing, ICSOC 2020

AU - Garfatta, Ikram

AU - Klai, Kaïs

AU - Graïet, Mahamed

AU - Gaaloul, Walid

PY - 2021/1/1

Y1 - 2021/1/1

N2 - 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.

AB - 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.

KW - Blockchain

KW - CTL properties

KW - Coloured Petri nets

KW - Formal verification

KW - Smart contract

KW - Solidity

U2 - 10.1007/978-3-030-76352-7_7

DO - 10.1007/978-3-030-76352-7_7

M3 - Conference contribution

AN - SCOPUS:85111380072

SN - 9783030763510

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

SP - 47

EP - 53

BT - Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings

A2 - Hacid, Hakim

A2 - Outay, Fatma

A2 - Paik, Hye-young

A2 - Alloum, Amira

A2 - Petrocchi, Marinella

A2 - Bouadjenek, Mohamed Reda

A2 - Beheshti, Amin

A2 - Liu, Xumin

A2 - Maaradji, Abderrahmane

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 14 December 2020 through 17 December 2020

ER -

Garfatta I, Klai K, Graïet M, Gaaloul W. Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach. In Hacid H, Outay F, Paik H, Alloum A, Petrocchi M, Bouadjenek MR, Beheshti A, Liu X, Maaradji A, editors, Service-Oriented Computing – ICSOC 2020 Workshops - AIOps, CFTIC, STRAPS, AI-PA, AI-IOTS, and Satellite Events, Proceedings. Springer Science and Business Media Deutschland GmbH. 2021. p. 47-53. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-76352-7_7

Blockchain-Based Business Processes: A Solidity-to-CPN Formal Verification Approach

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this