"Correctness is clearly the prime quality. If a system does not do what it is supposed to do, then everything else about it matters little."

Bertrand Meyer

Acknowledgment ✧ It is difficult to put into words how much gratitude I feel towards the people who have helped me along the way in my journey towards obtaining this PhD degree. It is the least I can do to dedicate these few words to them.

First and foremost, my gratitude goes to my amazing supervisors, Kaïs KLAI and Mohamed GRA ÏET, who have been incredibly supportive and encouraging throughout the course of my research and without whom none of it would have been possible. Their guidance, expertise, and wisdom have been invaluable, and I could not have achieved this without them.

To Kaïs KLAI, thank you for your brilliant insights, tireless dedication, and exceptional mentorship. Your expertise in formal verification and your ability to challenge and inspire me have been instrumental in shaping this work. But most importantly, thank you for simply being the great person that you are, and as clichéd as this may sound, being the role model that I needed. You have definitely left a mark on me that I will forever cherish.

To Mohamed GRA ÏET, thank you for your continuous encouragement, constant support and outstanding teaching. Your knowledge of software engineering and formal methods have helped me develop a rigorous and systematic approach to my research. Thank you for being the one who pushed me out my comfort zone when I needed it and provided me with the opportunities to have the best research experiences.

Together, you have offered me with a unique perspective and a wealth of knowledge that has been essential in the successful completion of this work. I am truly grateful for having crossed your paths. I am grateful to the members of my thesis committee, who have generously contributed their time and expertise to review and evaluate this work.

To Prof. Nathalie PERNELLE, Prof. Leila BEN AYED, Prof. Sara TUCCI, thank you for your brilliant comments and suggestions that have helped me develop a deeper understanding of the challenges and opportunities in my field of study.

I would like to express my deepest gratitude to Prof. Walid GAALOUL who has been really invested in different stages of this research. Thank you for your constructive feedback and critical evaluation of this work which have been instrumental in improving my work, as well as your exceptional guidance, support, and mentorship throughout my doctoral journey.

To Prof. Parisa GHODOUS and Prof. Raimundas MATULEVICIUS, thank you for your valuable insights and feedback which can only testify of a great and meticulous attention to detail, and which have helped me refine my work and improve the quality of this manuscript.

3

I would like to thank the staff and members of the computer science department of USPN who have created a supportive and intellectually stimulating environment that allowed me to flourish as a researcher. I would like to also thank their counterparts at the ENIT who have been the most accommodating and helpful with all of my administrative requests despite my constant tendency to flirt with the deadlines.

To my loving family, especially my mother Chadlia, who has been my rock, my constant source of love and encouragement, and who has sacrificed so much for me. Thank you for always believing in me, even when I didn't believe in myself..

To my father Hassen, who instilled in me a love for learning and a never-give-up attitude and has always been a source of inspiration to me. Your everlasting memory in my heart has guided me through some of the toughest times in my life. I hope I have made you proud..

To my dearest sisters and brothers who have been there for me through thick and thin as well as their partners and kids. Thank you for your unconditional love, support, and laughter. I am blessed to have you all in my life.

And last but not least, to my colleagues and friends, who I will most certainly fail to mention all.

To those who were at the end of their PhD journeys when I started mine: the big-hearted Hayet who was amongst the first people I ever met when I first arrived in France and who has always been there for me whenever I needed her, the superfriendly Mehdi who has been a great help for the socially-inept me to integrate the lab and much more, and the kind-hearted Enrico, Davide, Jawher and Hiba with whom I shared my first PhD memories (and long walks in Paris).

To those who were there throughout this journey, to the cheerful Noor and delightful Yasmine who never failed to bring a smile to my face, to Alec-the-Great who never failed to bring a scowl to it (though it is not much of a challenge, I confess), and to the charming Niama, gracious Reda, athletic Dina and vampirish Aloÿs with whom I shared many laughs. Thank you for your unwavering support, hilarious memes, and constant reminders to take breaks and enjoy life. You have made this journey so much more fun and bearable.

To those who were there before the journey even started, to the lively Marwa, the eloquent Hamza, the warm-hearted Ahmed and the classy Mohamed Amine. Thank you for constantly remembering I exist, and putting up with my frequent radio silence. Distance may have tried to drive a wedge between us but you are always on my mind (I am just not that good at showing it).

To all of you who have contributed to this work, I hope this manuscript does you justice. And to those who didn't contribute at all, but are somehow reading this anyway: thanks for stopping by!

Résumé

La blockchain, qui a d'abord été révélée comme la technologie à l'origine du bitcoin, a dépassé le cadre des crypto-monnaies pour s'étendre à un large éventail de domaines d'application, dont la gestion des processus métier (BPM). En effet, ses propriétés intrinsèques, telles que sa structure décentralisée, sa capacité à donner confiance à des parties non dignes de confiance, son immuabilité et sa transparence financière, semblent fournir les instruments nécessaires pour concevoir des solutions adaptées aux problèmes actuels de la BPM, en particulier pour les collaborations. Cette évolution est principalement due à l'introduction du concept de contrat intelligent dans les blockchains. Un contrat intelligent permet l'exécution de séquences de transactions interdépendantes tout en respectant les règles qui y sont établies. D'autre part, un processus métier peut être considéré comme un ensemble d'activités interconnectées par des relations causales dans le but d'atteindre un objectif métier. Par conséquent, les contrats intelligents semblent être d'excellents candidats pour la mise en oeuvre et l'automatisation des processus métier (BPs).

Malgré les avancées significatives dans l'adoption de la Blockchain pour le BPM, la technologie n'en est encore qu'à ses débuts, et le déploiement des contrats intelligents pour la mise en oeuvre des BPs ne peut être considéré comme sûr. Par conséquent, prouver la correction des contrats intelligents à déployer sur une blockchain est crucial pour l'intégrité des processus métier spécifiés.

Dans notre travail, nous proposons une approche formelle basée sur la transformation des contrats intelligents écrits en Solidity, en tenant compte du contexte BPM dans lequel ils sont utilisés, en un réseau de Petri coloré hiérarchique. Nous exprimons un ensemble de vulnérabilités des contrats intelligents sous forme de formules en logique temporelle et utilisons le vérificateur de modèles Helena pour, non seulement détecter ces vulnérabilités tout en discernant leur exploitabilité, mais aussi vérifier d'autres propriétés spécifiques aux contrats basées sur le temps. L'approche que nous proposons est basée sur la vérification des modèles représentés en CPN et comprend principalement trois phases:

1. transformer le code Solidity des contrats intelligents en sous-modèles CPN correspondant à leurs fonctions.

Plus précisément, nous optons pour un modèle CPN hiérarchique pour représenter l'exécution et l'interaction des contrats intelligents considérés dans le cadre de la spécification du contexte BPM éventuellement fournie. Pour ce faire, nous représentons chaque fonction d'un contrat intelligent par une transition agrégée qui encapsule un sous-modèle correspondant au flux de travail interne de la première. En fait, notre objectif à cette première étape est d'obtenir des blocs de construction pour le modèle hiérarchique qui sera fourni au vérificateur de modèles. Ensuite, étant donné une spécification de contexte (transformée en CPN) et une propriété LTL à vérifier, le modèle CPN final est construit en (1) reliant la transition agrégée représentant la fonction ciblée au modèle comportemental et (2) construisant une hiérarchie en représentant explicitement les appels de fonction dans le sous-modèle en question (si la propriété vérifiée le requiert).

Nous avons implémenté un outil graphique appelé Solidity2CPN qui met en oeuvre et automatise les différentes étapes de l'approche proposée et la rend accessible à un plus grand nombre d'utilisateurs qui ne sont pas nécessairement familiers avec les aspects de la vérification formelle.

Abstract

Blockchain, which was first introduced as the technology driving Bitcoin, has now outgrown the confines of cryptocurrencies to find its way into a wide range of application areas, including Business Process Management (BPM). Indeed, its intrinsic properties, such as its decentralized structure, capacity to give trust among untrustworthy parties, immutability, and financial transparency, appear to provide the necessary instruments for devising suitable solutions for current BPM issues, particularly for collaborations. This evolution has been mainly owed to the concept of smart contracts being introduced to Blockchains. A smart contract allows the execution of interdependent transaction sequences while adhering to the rules established in it. On the other hand, a business process may be considered as a set of activities connected by causal relationships with the purpose of attaining a business goal. As a result, smart contracts appear to be excellent candidates for implementing and automating BPs.

Despite significant advancements in Blockchain adoption for BPM, the technology is still in its infancy, and deploying smart contracts to carry out BPs cannot be deemed safe. As a result, proving the correctness of the smart contracts to be deployed on a blockchain is critical for the integrity of the specified business processes.

In our work 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 temporalbased contract-specific properties. Our proposed approach is based on model checking of CPN models and comprises mainly three phases:

1. transforming the smart contracts' Solidity code into CPN sub-models corresponding to their functions.

2. transforming the BPM context into a CPN model 3. constructing a CPN model w.r.t an LTL property that can express: (i) a vulnerability in the code or (ii) a contract-specific property, linking it to a CPN model representing the behavior to be considered, and feeding it the model checker to verify the targeted property.

More precisely, we opt for a hierarchical CPN to represent the considered smart contracts' execution and interaction w.r.t the provided BPM context specification. To do so, we represent each function of a smart contract by an aggregated transition that encapsulates a sub-model corresponding to the internal workflow of the former. In fact, our aim at this first step is to get building blocks for the hierarchical model that will be fed to the model checker. Then, given a context specification (transformed into CPN) and an LTL property to be verified, the final CPN model is built by (1) linking the aggregated transition representing the targeted function to the behavioral model and (2) building a hierarchy by explicitly representing function calls in the submodel in question (if the checked property requires it).

We have implemented a graphical tool called Solidity2CPN that automates the different steps of the proposed approach and makes it accessible to a broader range of users who are unfamiliar with the aspects of formal verification.

Table of contents

General Introduction

List of Tables

Research context

It is not often that an emerging technology acquires an impact that goes beyond what it had been initially intended, and yet as much can be said of the Blockchain. Initially featured as the technology behind Bitcoin [START_REF] Nakamoto | A peer-to-peer electronic cash system[END_REF], Blockchain has soon after escaped the box of cryptocurrencies to find its way into a multitude of application domains and become an integral ingredient of our daily lives. In fact, within the span of the two last decades, the Blockchain has known many advances that took it from being merely a database recording transactions between parties to being a computational platform on which small programs can be invoked as transactions. This leap has significantly expanded the power of Blockchain systems, and increased their reach to many application fields. This can be particularly observed in the growing interest Blockchains are gaining as part of IT systems, in domains such as health records, banking, voting, personal identity, etc [START_REF] Staples | Risks and opportunities for systems using blockchain and smart contracts[END_REF]. According to healthcare statistics [START_REF]Top 10[END_REF], Blockchain is in the top-5 priorities of 40% of senior health executives, mainly thanks to its ability to provide a seamless exchange of patient data between healthcare facilities while maintaining its confidentiality. Additionally, 13% of senior IT leaders expressed their intentions to integrate Blockchain into their daily business processes, driven essentially by its prospects to lower their system maintenance costs and raise their security levels [START_REF]Top 10[END_REF]. This diversity in application fields, however, does not take away from the importance of cryptocurrencies as in the year 2020, the market size of the Blockchain technology was estimated at $3.7 billion [START_REF]Numbers about blockchain -fujitsu blockchain innovation center : Fujitsu belgium[END_REF]. The technological research and consulting firm, Gartner, Inc., predicts that Blockchain's business valueadd will be over $176 billion by 2025 and will approach $3.1 trillion by 2030. Such numbers are a clear indication of the weight of this technology in the Business world.

Currently, the Blockchain technology has witnessed the rise of three generations: the first one as a digital currency, the second as a digital economy, and the third as a digital society [START_REF] Efanov | The all-pervasiveness of the blockchain technology[END_REF]. Conceptually, a Blockchain is a distributed ledger that keeps records of transactions happening among a network of participants. A consensus mechanism is used to confirm valid transactions and reject fraudulent ones. Once a transaction is confirmed and added to a record in the Blockchain, it is no longer possible to alter nor delete it. This definition gives the basic idea of a firstgeneration Blockchain which focuses solely on cryptocurrencies transfer. The emergence of second-generation Blockchains occurred when the distributed ledgers were embedded by so-called smart contracts that enable them to function as distributed computing platforms. Blockchain was then able to support new economic and financial applications beyond simple payments (e.g., traditional banking and legal services like loans, stocks, contracts, monetized assets, etc). The transition to third-generation Blockchains was only a matter of time as it became clear that what the concept of smart contracts brought to this technology could take its applications beyond any economic activity and into a variety of fields including art, health, science, identity, governance, etc [START_REF] Efanov | The all-pervasiveness of the blockchain technology[END_REF]. As a matter of fact, the Blockchain technology is regarded as the second-most important innovation, behind the internet. If the latter could be used to establish online business processes by connecting people, the former resolves the trust problems using peer-to-peer networking and public-key cryptography.

One of the most interesting applications of the Blockchain technology is the domain of Business Process Management (BPM) [START_REF] Mendling | Blockchains for business process management -challenges and opportunities[END_REF]. The concept of Business processes (BPs) emerged in the early 20 th century and has been evolving ever since. By the early 1990s, researchers were already talking about Business Process Management (BPM) as a discipline that reigns upon enterprises seeking both effectiveness and efficiency and striving for innovation and flexibility especially within the world of IT. Many definitions have been proposed to clearly determine the meaning of this discipline and its boundaries. According to [START_REF] Bpm | What is bpm?[END_REF][START_REF] Coalition | What is bpm?[END_REF][START_REF] Von Rosing | The Complete Business Process Handbook: Body of Knowledge from Process Modeling to BPM[END_REF], BPM is a discipline that encompasses all types of modeling, automation, execution, control, measurement, and optimization of business activity flows in support of organizational goals, spanning systems, personnel, clients, and partners both inside and outside the enterprise. This discipline is therefore centered around these Business activity flows which are commonly referred to as Business Processes. A Blockchain platform can indeed provide a reliable execution of Business processes even within a trustless network, especially thanks to the concept of smart contracts. In fact, its inherent characteristics, namely its decentralized nature, ability to provide trust among trustless parties, immutability and financial transparency seem to put on the table the right tools to contrive adequate solutions for existing problems in the BPM research field, especially (but not exclusively) when it comes to collaborations [START_REF] Mendling | Blockchains for business process managementchallenges and opportunities[END_REF]. One of the promising integration possibilities of these two fields is the design of Blockchain-based business processes. So far, the general preference has been to use an existing modeling language for BPs and adopt Blockchain for different aspects of their management. For instance, Lorikeet [START_REF] Tran | Lorikeet: A model-driven engineering tool for blockchain-based business process execution and asset management[END_REF] is a tool that leverages Blockchain as a message exchange mechanism for BP choreographies. Caterpillar [START_REF] López-Pintado | Caterpillar: A business process execution engine on the ethereum blockchain[END_REF], on the other hand, is used to implement the BP model and deploy it on the chain. This has been possible thanks to the concept of smart contracts introduced by Ethereum, which allow the execution of sequences of interdependent transactions while complying to the rules implemented within. In general, a BP can be analogously viewed as a sequence of tasks linked by causal relationships with the aim of achieving a particular business goal. Therefore, smart contracts seem to be ideal candidates for the implementation and automation of business processes. Moreover, the intended behaviour of smart contracts can intuitively be represented using a business process representation that would characterize the context in which the smart contracts are supposed to be executed. Such a behavioural context can either come directly as a description of a business model or be derived from a script that would be used to invoke the smart contracts. In fact, smart contracts are pieces of code that act like autonomous software agents, used to enforce management rules on the execution of transactions on the Blockchain. They are stored on and executed by the Blockchain and therefore inherit its characteristics, particularly its immutability. This same feature can, however, turn into a weak spot for such contracts. In fact, as a smart contract cannot be altered once it has been deployed on the Blockchain, it cannot be corrected either, which makes verifying its correctness prior to its deployment an indispensable necessity. Furthermore, the correctness verification is an important aspect for the design of Blockchain-based BPs. The assessment of such processes involves both requirements validation and consistency.

In light of this context, the ultimate goal of this thesis is to provide a solution that would aid smart contract designers, especially (but not exclusively) those involved in the BPM world, to correctly design and implement their contracts. This includes helping them avoid well-known vulnerabilities that may threaten the security of their smart contracts (and therefore their Blockchain-based applications), as well as providing the necessary support to define their own correctness criteria and make sure their smart contracts shall abide by them.

Motivation and problem statement

Blockchain is still considered an evolving technology whose extent has not been fully revealed. Working towards new ways of exploiting it, though can lead to valuable exploits, is undoubtedly a risky endeavor. In fact, despite the advance in the adoption of Blockchain for the BPM context, its state is still nascent, and using smart contracts to carry on BPs cannot be considered safe. Many attacks with significant consequences on several Blockchain platforms, exploiting hidden vulnerabilities in deployed smart contracts and exposing the defectiveness of the targeted applications bear witness to such a risk. The first dangerous attack on a Blockchain can be traced back to August 2010, when 92 billion BTC were generated out of thin air by exploiting an integer overflow vulnerability in the Bitcoin Blockchain [START_REF]Overflow incident[END_REF], which resulted in cancelling all relevant transactions and rolling back the Blockchain to a previous state. The DAO (a Decentralized Autonomous Organization built upon Ethereum) attack in June 2016, caused by a reentrancy vulnerability, is one of the most infamous attacks Ethereum has ever had to suffer [START_REF] Siegel | The dao attack: Understanding what happened[END_REF]. On top of the tangible loss that evaluated to 3.6M of stolen ether (around 55M USD at the time) the attack resulted in a hard fork in the Ethereum Blockchain which could have easily resulted in a community fallout, the worst possible nightmare for Ethereum. The Parity multisig wallet has been subject to two substantial attacks. The first happened in July 2017 when more than 150K ETH were stolen (32M USD). The attacker used a vulnerability in the code (a bad practice) that allowed him to change the ownership of an important contract and take possession of its ether. The second attack which happened in November 2017, and which was more of an unintentional accident caused by a self-destruct vulnerability, did not result in stolen funds but caused 513K ETH to be locked in the attacked contracts (160M USD) [START_REF] Team | Parity multi-sig wallets funds frozen (explained)[END_REF]. The damages were obviously serious, so much as to push Blockchain foundations to propose bug bounty programs [3,[START_REF]Parity bug bounty program[END_REF] offering rewards for uncovering vulnerabilities.

From an academic point of view, numerous methods and tools have therefore emerged to both support the development of secure smart contracts and aid the analysis of already deployed ones. This panoply of studies comprises approaches that use non-formal techniques to detect bugs in certain execution scenarios, as well as approaches based on formal techniques and aim for an automatic formal verification of smart contracts. While informal techniques can test a certain requirement under certain scenarios, they cannot prove the correctness of a smart contract in general (e.g., absence of integer overflow vulnerabilities, deadlock-freedom). That's why researchers turned to formal verification which has proved to be efficient to reach such correctness goals [START_REF] Garavel | The 2020 expert survey on formal methods[END_REF].

We note that in our research work, we are interested in Ethereum smart contracts as it is currently the second largest cryptocurrency platform after Bitcoin besides being the inaugurator of smart contracts, and more particularly those written in Solidity [START_REF]Solidity documentation[END_REF] as it is the most popular language used by Ethereum. We also note that while Ethereum allows smart contracts to be written in a 'Turing complete' language that facilitates semantically richer applications than Bitcoin which allows very simple forms of smart contracts, the former also enlarges the threat surface, as evidenced by the many high-profile attacks.

As will be detailed later in Chapter 3, many studies have proposed formal approaches for the verification of Solidity smart contracts. The majority of these propositions, however, aim to detect some of the well-known vulnerabilities of Solidity, with only a minority giving the possibility to check for some other predefined properties and none allowing the specification of user-defined properties. Not only is the de-tection of a number of vulnerabilities not enough to decide the correctness of smart contracts in general, but also the possibility of defining contract-specific properties can come very handy especially if the users have a specification of the behavioural context in which they intend to use their smart contracts. Moreover, no studies have yet treated the verification of smart contracts used in the context of BPM despite the growing use of Blockchain in this discipline.

The work presented in this PhD thesis is motivated by the previously described challenges and shortcomings, and aims to tackle the following research issue: the formal verification of Solidity smart contracts in a BPM context. To address this research problem, we need to answer the following main research questions:

• RQ1: How to verify Solidity smart contracts in general?

• RQ2: How to describe the behaviour of Solidity smart contracts using a BP context specification?

• RQ3: How to verify Solidity smart contracts with a BP context specification?

To better clarify the problems that we will be dealing with in this PhD work, we furthermore define other questions that derive from the previous ones:

• RQ4: How to homogenize a behavioural context specification with that of Solidity smart contracts

• RQ5: What vulnerabilities can hinder the correct execution of Solidity smart contracts and how to detect them?

• RQ6: What kind of properties need to be verified to ensure the correctness of Solidity smart contracts used in a BPM context?

Objectives and contributions

In view of the previously described challenges and shortcomings, the main objectives of this PhD thesis can be summarized as follows:

• Obj1: provide a formal model for Solidity smart contracts

• Obj2: provide formal models for possible behavioural contexts that may accompany the smart contracts

• Obj3: formally define well-known vulnerabilities

• Obj4: provide a full approach to formally verify smart contracts while supporting the possibility of behavioural context specifications

In this PhD thesis, we propose a formal approach for the verification of Solidity smart contracts with a particular focus on those used in the BPM context. Herein we give a global overview of this approach that combines our contributions that will be detailed in Chapters 4-7, and whose technical elements will be explained in Chapter 2.

Our approach is based on model checking as a formal verification method applied on Coloured Petri Net as a representation formalism and using Linear Temporal Logic to express the properties to be verified. In fact, model checking is technique whose goal is to check the satisfaction of some properties expressed in a formal logic in a system specified as some sort of finite-stat model. We choose to use this technique on Coloured Petri Nets (CPNs) [START_REF] Jensen | Coloured Petri Nets: Modelling and Validation of Concurrent Systems[END_REF]. Thanks to their ability to combine the analysis power of Petri nets with the expressive power of programming languages, CPNs are suitable candidates for the modeling and verification of large and complex systems, and therefore they are employed in our approach to model the smart contracts execution with respect to a behavioral context specification defining the workflow within which they are used. In layman's terms, we use the CPN formalism to represent Solidity smart contracts and behavioural context specifications, and we leverage the model checking method to see if properties defined on these contracts actually hold.

To explain our approach in more detail, we depict its different stages in Figure 1.1. This approach comprises mainly five steps:

1. transformation of the smart contracts' Solidity code into CPN sub-models corresponding to their functions. This step comes as a contribution to achieve Obj1 which is part of the response to RQ1 .

2. transformation of the behavioural context specification into a CPN model. This step comes as a contribution to achieve Obj2 which is part of the response to RQ2 and RQ4 .

3. expression of the property to be verified in LTL. This step comes as a contribution to achieve Obj3 which is part of the response to RQ5 and RQ6 .

4. generation of a Hierarchichal CPN (HCPN) model. This step comes as a contribution to achieve Obj4 which is part of the response to RQ3 and RQ4 .

5. model checking of the generated HCPN model w.r.t to the specified LTL property. This is the final step that puts together all the pieces of the approach to achieve our final goal.

Thesis outline

The remainder of this PhD thesis manuscript will be organized as follows:

• Chapter 2: Preliminaries introduces the basic concepts related to our research and needed to understand the details of the work. In this chapter, we first present the technology of Blockchain, with a focus on the Ethereum platform and its main smart contracts language Solidity. Then, we introduce both imperative and declarative approaches for the representation of Business Processes. Finally, we shift the focus onto the formal methods and models leveraged in our work, namely model checking as a formal verification technique, Coloured Petri Net as a representation formalism and Linear Temporal Logic as a means for the expression of properties to be verified.

• Chapter 3: State of The Art provides an exploration and a thorough analysis of the state of the art around the problematic of our research work. Herein we mainly focus on studies related to the formal verification of Solidity smart contracts. We then give an overview of the application of formal methods for the verification of different aspects of Business process models.

• Chapter 4: Formal Modeling of Solidity Smart Contracts presents our approach to formally model Solidity smart contracts using Coloured Petri Net as a representation formalism.

• Chapter 5: Formal Modeling of Behavioural Contexts introduces our approach to formally represent two kinds of contexts that can be used for the description of the behaviour of smart contracts. We start by the formalization of the free context which is used when no restrictions are provided for the execution of such contracts. Then we give a formalization for a constrained context which is used when some restrictions are provided for the execution of the smart contracts.

• Chapter 6: Expression of Properties to be Verified using Linear Temporal Logic details our approach to formalize six of the most common vulnerabilities in Solidity using LTL and explains how this logic can also be used for the specification of contract-specific properties.

• Chapter 7: Application and Implementation of our Approach illustrates how the contributions presented in the three previous chapters are put together to bring forth and end-to-end tool for the formal verification of smart contracts with a behavioural context specification.

• Chapter 8: Conclusion and Future Work summarizes the proposed contributions and presents an outlook on the potential perspectives that we intend to tackle in the short-medium term.

Chapter 2

Preliminaries Contents

Introduction

This chapter introduces the main concepts and background required for the understanding of the contributions described in the remainder of this manuscript. We start by introducing the Blockchain technology in Section 2.2, with a focus on the Ethereum platform and Solidity as a smart contracts implementation language. Then, in Section 2.3 we discuss both the imperative and declarative paradigms for Business process modeling while focusing on Dynamic Condition Response (DCR) Graphs as a representation for BPs. Finally, Section 2.4 comes to introduce the formal methods and models that will be used throughout our proposed contributions, namely model checking, Coloured Petri Net and Linear Temporal Logic.

Blockchain Technology

The idea for the first decentralized Blockchain goes back to 2008 when Satoshi Nakamoto proposed a design for a peer-to-peer electronic cash network that would solve the problem of double-spending without the need for a trusted third-party. This network timestamps transactions by hashing them into an ongoing chain of hashbased proof-of-work, forming a record that cannot be changed without redoing the proof-of-work. This idea was then put into use as fundamental part of the Bitcoin cryptocurrency where it serves as the network's main public ledger for all transactions [START_REF] Nakamoto | A peer-to-peer electronic cash system[END_REF]. Numerous applications have emerged since the advent of Bitcoin, all of which aim to make use of the capabilities and principles of the public ledger technology. As a result, a considerable number of Blockchain platforms have emerged over the course of history.

The Ethereum Platform

Co-founder of Bitcoin Magazine in 2011, Vitalik Buterin was among the many engineers who believed that Bitcoin had not yet fully used the potential of the Blockchain technology. He began developing what he thought would be a flexible Blockchain that could serve a variety of purposes in addition to serving as a peer-to-peer network. A crucial turning point in the history of the Blockchain came when Ethereum [2] was introduced as a brand-new public Blockchain in 2013 with more features than Bitcoin. Buterin was able to position Ethereum in a different league from its predecessor Bitcoin by introducing two main additions: the possibility to keep track of assets other than cryptocurrencies, and the renowned concept of smart contracts. These new features were what allowed Ethereum's capabilities to go beyond those of a cryptocurrency to those of a platform for the development of decentralised applications. The Ethereum Blockchain, which was formally introduced in 2015, ended up being one of the most significant uses of Blockchain technology thanks to its smart contracts that can be used for a variety of tasks. The Blockchain technology for Ethereum has also been successful in attracting a vibrant developer community, which has helped it build a real ecosystem. The Ethereum Blockchain conducts the most daily transactions and its market cap has also notably grown [1].

Solidity Smart Contracts

Smart contracts take the famous saying "code is law" into a new perspective where law becomes code. They can be seen as the equivalent of contracts written on paper, where the agreed upon terms are transcribed in lines of code. The faithful execution of a smart contract is governed and guaranteed by the laws of the Ethereum Virtual Machine (EVM) semantics and its immutable nature gives it a sense of finality.

The most commonly-used high-level programming language for Ethereum smart contracts is Solidity [START_REF]Top 5 programming languages to build smart[END_REF]. A Solidity smart contract is a collection of code and data, residing at a specific address on the Ethereum Blockchain, which can be invoked either by an internal account (i.e., a smart contract) or directly by an external account (i.e., user). Every account is characterized by a persistent storage (null in case of an external account) and a balance in Ether which is adjusted by transactions. A transaction is message used to send ether from one account to another and/or invoke a smart contract's function if the message includes a payload and the targeted account is an internal one. The execution of such a payload is carried out according to a stack machine called the EVM. Every smart contract features a memory which is cleared at each message call, and it can access certain properties of the current block (e.g., number, timestamp...). Besides the storage, stack and memory, Ethereum has an externally accessible indexed data structure that can be used by Solidity to implement events and acts as a log.

A Solidity smart contract may look like a JavaScript or C program syntax-wise, but they are actually dissimilar since the underlying semantics of Solidity functions differently from traditional programs. This naturally calls on more vigilance from the programmers who might be faced by unconventional security issues as vulnerabilities in smart contracts seem to often stem from this gap between the semantics of Solidity and the intentions of the programmer [START_REF] Atzei | A survey of attacks on ethereum smart contracts (sok)[END_REF].

Solidity Smart Contract Example -Blind Auction

We consider the following example which we adapted from [START_REF]Solidity documentation[END_REF].

Participants in a blind auction have a bidding window during which they can place their bids. A participant can place more than one bid (function bid in Listing 2.1 -Lines 17 to 19) and the placed bid is blinded. The bidder has to make a deposit with the blinded bid, with a value that is supposedly greater than the real bid. Once the bidding window is closed, the revealing window is opened. Participants proceed to reveal their bids (function reveal in Listing 2.1 -Lines 20 to 30) by sending the actual values of the bids along with the used keys. The system verifies whether the sent values correspond with the placed blinded bids and potentially updates the highest bid and bidder's values. If the revealed value of a bid does not correspond with its blinded value, or is greater than the deposit, the said bid is considered invalid. Once the revealing window is closed, participants can proceed to withdraw their deposits (function withdraw in Listing 2.1 -Lines 31 to 42). A deposit made along a nonwinning, invalid or unrevealed bid is wholly restored. In case of a winning bid, the difference between the deposit and the real bid is restored. The auction is terminated when all participants withdraw their deposits. As we have mentioned before in Section 1.1, smart contracts bear some resemblance to Business processes, which stems from the fact that both can be regarded as a set of activities or operations, executed in a certain logical order to achieve a certain functional goal. This, in addition to the compatibility of the Blockchain's characteristics (e.g., immutability, decentralization, etc) with the needs in BPM, makes the integration of these two fields a propitious idea. The next section of this manuscript will introduce the basics on Business Process representations, these will later on be used as means to the modeling of behavioural contexts for smart contracts.

Business Process Model Representations

The representation of Business process models follows mainly two paradigms: an imperative one which is considered the traditional way to represent Business process models, and a declarative one that has been witnessing a widespread use recently [START_REF] Fahland | Declarative versus imperative process modeling languages: The issue of understandability[END_REF].

Controversy arises as to whether imperative or declarative modeling approaches are better. An empirical investigation [START_REF] Pichler | Imperative versus declarative process modeling languages: An empirical investigation[END_REF] states that while imperative languages can be considered superior in terms of comprehensibility by end-users, this fact's accuracy can be influenced by the experimental subjects' familiarity with imperative modeling languages as they are traditionally and more profusely used in business process modeling. On the other hand, declarative modeling approaches are loosely considered less rigid than their counterpart and therefore more suitable for rapidly evolving business processes. This difference in flexibility emanates from the fact that imperative models represent how a process is executed by explicitly defining its control flow while declarative models focus on why a process is executed in such a way by implicitly defining its control flow as a set of rules. Consequently, making changes to an imperative model is more time-consuming and complex than altering a declarative one, since the former would entail explicitly adding/deleting execution alternatives (which can call into question the correctness of the model) while the latter could be achieved by adding/deleting constraints from the model to discard/add execution alternatives.

In our work, we do not support any claims for the supposed superiority of any paradigm over the other, but we rather aim to exploit the best in both of them.

Imperative Representations

Imperative process models are also referred to as workflow models since they are a representation of the control flow of the process. A workflow is a description of an algorithm used to carry out a business process. As a result, it necessitates that the modeler be fully aware of every step required to achieve the intended outcomes in each and every scenario. A wide range of graphical process modelling languages has been proposed over the last decades to represent a business process such as Business Process Model and Notation (BPMN) [START_REF]OMG: Business process model and notation (bpmn) 2.0[END_REF], Event-Driven Process Chain (EPC) [START_REF] Scheer | ARIS -vom Geschaftsprozess zum Anwendungssystem[END_REF], Yet Another Workflow Language (YAWL) [START_REF] Van Der Aalst | Yawl: Yet another workflow language[END_REF], UML Activity Diagram [START_REF]OMG. Unified modelling language[END_REF], etc. Despite their variances in expressiveness and modelling notations, they all share the common concepts of tasks, events, gateways, artifacts and resources, as well as relations between them, such as transition flows [101].

Business Process Model and Notation

The Business Process Model and Notation (formerly known as Business Process Modelling Notation) (BPMN) was first released in 2004 by the Business Process Management Initiative (BPMI) [START_REF]OMG: Business process model and notation (bpmn) 2.0[END_REF]. BPMN is a standard for business process modelling that allows to create and document process models. It is considered as the de facto process modelling notation that is widely used in industry. In its latest versions, BPMN has been enhanced with executable semantics enabling the execution of the modelled process. It provides a rich set of elements to capture different perspectives of the business process at different levels of detail. These elements can be categorized into a core set which contains the basic elements to model a business process and an extended set which contains more specialized elements to specify more complex business scenarios [START_REF] Muehlen | How much language is enough? theoretical and practical use of the business process modeling notation[END_REF]. Overall, BPMN defines 50 constructs grouped into four categories: Flow objects, Connecting objects, Swimlanes and Artifacts. Flow Objects allow to model the control flow perspective of a business process in terms of activities, events and gateways. An activity is the main element of a process model and describes the kind of work that must be done. It is graphically represented as a rectangle. An event is something that happens during the execution of a business process. There are three main types of events: Start, Intermediate and End events. An event is graphically represented with a circle. A gateway allows to model the splits and joins in the process model. Three main types are used to represent different behaviours in a business process: AN D (parallel forking and synchronization), XOR (exclusive choice and merging) and OR (inclusive choice and merging). Although there exist other more specialized gateways in BPMN such as event-based gateway and complex gateways, they can all be mapped to one of the three main types OR, AN D or XOR. The flow objects elements are connected through the Sequence flow element in the Connecting objects category. They determine the order in which the activities are supposed to be performed in a process.

In Figure 2.1, we propose a design for the blind auction system whose smart contract was described in Section 2.2.2 (Listing 2.1) using a BPMN choreography diagram. In this example, we chose to separate the tasks performed by the Bidder from those performed by the Auction Holder, who in our case is the smart contract itself, hence the use of two swimlanes. The tasks of the Bidder represent therefore calls to the functions of the Blind Auction smart contract (e.g., the activity Place blinded bid represents a bidder's call to the function bid in Listing 2.1), whereas the tasks of the Auction Holder represent the execution of these functions (e.g., the activity Receive blinded bid represents the execution of the function bid in Listing 2.1). Start Reveal and End Reveal are two intermediate events used to indicate the opening and closing of the revealing window as per the description given for the Blind Auction smart contract. The XOR split and join gateways (lozenge shapes with X inside) are used to allow a bidder to make the exclusive choice to either reveal and then withdraw their bid, or directly withdraw it.

Declarative Representations

Imperative modeling languages for Business processes are viewed as being somewhat strict and restrictive since they do not offer strategies for dealing with unanticipated circumstances. New adaptive business processes have then been developed in response to the need for more adaptable management systems [START_REF] Dadam | Towards truly flexible and adaptive process-aware information systems[END_REF]. This marked a paradigm change compared to the traditionally-used modeling techniques. Declarative languages are distinguished by their ability to express "what" has to be done without determining the specifics of "how" to do so. They therefore enable context-aware decision-making by process participants during the execution of business processes. Contrarily, restricting business rules are established to stop members from engaging in actions that the organization forbids or deems undesirable [START_REF] Pesic | A declarative approach for flexible business processes management[END_REF]. ConDec [START_REF] Pesic | A declarative approach for flexible business processes management[END_REF] and DecSerFlow [START_REF] Van Der Aalst | Decserflow: Towards a truly declarative service flow language[END_REF] are amongst the first declarative languages proposed for process modeling and are both supported by DECLARE [START_REF] Pesic | DECLARE: full support for loosely-structured processes[END_REF], a prototype workflow management system. In our work, we are interested in Dynamic Condition Response (DCR) graphs [START_REF] Hildebrandt | Declarative event-based workflow as distributed dynamic condition response graphs[END_REF] as a means for business process representation as this language was proposed to improve on the execution efficiency problems encountered in the former languages [START_REF] Van Der Aalst | Declarative workflows: Balancing between flexibility and support[END_REF].

In the following, we start by the definition of DCR graphs before giving the definition of DCR choreographies.

Dynamic Condition Response Graphs

Syntax Definition 2.3.1. A DCR graph is a tuple G = (E, M, Act, →•, •→, →+, →%, →⋄, l)
where M(G) = def P(E) × P(E) × P(E) is the set of all markings:

1. E is the set of events, ranged over by e.

2. M ∈ M(G) is the marking of the graph (explained below).

3. Act is the set of actions.

→•,

•→⊆ E × E are the condition and response relations, respectively. In general, e is a condition for e ′ (e →•e ′ ) means that e must have been executed at least once before executing e ′ . Having e ′ as a response for e (e•→e ′ ) means that e ′ should be executed at least once after having executed e.

5. →+, →% ⊆ E × E are the dynamic include and exclude relations, respectively, satisfying that ∀e ∈ E . e →+ ∩ e →% = ∅.

6. →⋄⊂ E × E is the milestone relation.

7. l : E → Act is a labelling function mapping every event to an action.

Semantics A marking M = (Ex, Re, In) ∈ M(G) is a triplet of event sets where Ex represents the set of events that have previously been executed, Re the set of events that are pending responses required to be executed or excluded, and In the set of events that are currently included. The idea conveyed by the dynamic inclusion/exclusion relations is that only the currently included events are considered in evaluating the constraints. In other words, if e is a condition for e ′ (e →•e ′ ), but is excluded from the graph then it no longer restricts the execution of e ′ . Moreover, if e ′ is the response for e (e•→e ′ ) but is excluded from the graph, then it is no longer required to happen for the flow to be acceptable. The inclusion relation e →+ e ′ (resp. exclusion relation e →% e ′ ) means that, whenever e is executed, e ′ becomes included in (resp. excluded from) the graph. The milestone relation is similar to the condition relation in that it is a blocking one. The difference is that it is based on the events in the pending response set. In other words, if e ′ is a milestone of e (e ′ →⋄ e), then e cannot be executed as long as e ′ is in Re.

In Figure 2.2, we propose a design for the blind auction system whose smart contract was described in Section 2.2.2 (Listing 2.1) using a DCR graph. Visually, such a model can be represented as a directed graph with events (boxes) as nodes and five types of arrows for the five types of relations that can link them. This DCR graph follows the same idea as the BPMN choreography model proposed in Figure 2.1. That is to say, an event in our graph can either represent a call to a function from the Blind Auction smart contract (Listing 2.1) or the execution of that function itself. Relations are used to define which events can or have to be executed at each step of the process. For example, initially only the Place blinded bid event can be executed (the initial marking M 0 indicates that we only have that event in the set of included events In). The execution of the said event would include the Receive blinded bids and Reveal bids events which have the former event as a condition. The Receive blinded bids event is also a milestone for the Reveal bids event, which means that at this step, only the Receive blinded bids event can be executed. In this proposed graph, the execution of the Reveal bids event marks the start of the revealing window by excluding the Place blinded bid event, and the execution of the Request withdrawal marks the end of that window by excluding the Reveal bids event.

Dynamic Condition Response Choreographies

Syntax A DCR choreography [START_REF] Hildebrandt | Declarative choreographies and liveness[END_REF] is a DCR graph that can be executed in a distributed way between a number of participants. An event in a DCR choreography has an initiator and can potentially have one or more receivers. In the following, we adapt the definition given in [START_REF] Hildebrandt | Declarative choreographies and liveness[END_REF] on account of simplicity and better adequacy with our work. Definition 2.3.2. A DCR choreography is a couple (G, R) where R is a set of roles and G is DCR graph whose labelling function l is instead defined as follows:

• l : E → (Act × R × P(R))
Semantics A DCR choreography has the same semantics as a DCR graph with the added condition that only the initiator of an event can execute it. For more details on DCR Graphs we refer the readers to [START_REF] Mukkamala | A Formal Model For Declarative Workflows Dynamic Condition Response Graphs[END_REF].

An example of a distributed DCR choreography for our Blind Auction system is given in figure 2.3. As a continuation to the previous DCR graph in Figure 2.2 and to keep the harmony with the BPMN choreography in Figure 2.1, we keep the events and relations of the former and introduce the participants of the latter (i.e.,Bidder A primordial phase in the life cycle of a business process is its verification. In order to avoid execution mishaps whose gravity may vary with the level of criticality of the modeled system, the designer needs to make sure that the model will actually satisfy a set of requirements/specifications that define the correctness of the system. In the following section, we will present a basic introduction to formal methods and models, with a focus on model checking as a verification technique and coloured Petri net as a formal model.

Formal Methods and Models

Formal methods are methodologies to specify, develop, and verify software and hardware systems that are rigorously mathematical in nature. The idea that completing adequate mathematical analysis may, like in other engineering disciplines, contribute to the dependability and robustness of a design is what drives the adoption of formal techniques [START_REF] Holloway | Why engineers should consider formal methods[END_REF]. When it comes to formal verification, such techniques are used to check the conformance of the developed system to a predefined specification. They are based on formal methods of mathematics and are able to provide formal proof of the correctness of the investigated system with reference to its formally specified behavior. We can distinguish two main branches of formal verification methods: first, those based on theorem proving, where a prover is used to discharge proofs on a math-ematically modeled system. Such approaches however cannot be fully automated, as the user usually has to intervene to assist the prover; and second, those based on model checking. Besides being automatable, model checking techniques can also provide counter examples which are basically execution traces that show how a property of the modeled system is violated. This can be a valuable information for designers especially in reassessing their model. The basic idea of model checking is to model the system as a formal model (e.g., finite state machine), generate its state space, and then explore it to check some specification that is supposed to define the correctness of the system.

In this PhD thesis, we rely on model checking to verify Linear Temporal Logic properties on coloured Petri net models.

Coloured Petri Nets

A Petri net [START_REF] Murata | Petri nets: Properties, analysis and applications[END_REF] is a formal model with mathematics-based execution semantics. It is a directed bipartite graph with two types of nodes: places (drawn as circles) and transitions (drawn as rectangles). Despite its efficiency in modelling and analysing systems, a basic Petri net falls short when the system is too complex, especially when representation of data is required. To overcome such limitations, extensions to basic Petri nets were proposed, equipping the tokens with colours or types and hence allowing them to hold values. A large Petri net model can therefore be represented in a much more compact and manageable manner using a Coloured Petri net [START_REF] Jensen | Coloured Petri Nets: Modelling and Validation of Concurrent Systems[END_REF]. The formal definition of a CPN is given in Definition 2.4.1.

Syntax

Definition 2.4.1 (Coloured Petri net). A Coloured Petri Net is a nine-tuple CP N = (P, T, A, Σ, V, C, G, E, I), where:

1. P is a finite set of places.

T is a finite set of transitions such that

P ∩ T = ∅. 3. A ⊆ (P × T ) ∪ (T × P ) is a set of directed arcs.
4. Σ is a finite set of non-empty colour sets.

5. V is a finite set of typed variables such that T ype[v] ∈ Σ, ∀v ∈ V .
6. C : P → Σ is a colour set function that assigns a colour set to each place. 7. G : T → EXP R V , where EXP R V is the set of expressions with variables in V , is a guard function that assigns a guard to each transition t.

8. E : A → EXP R V is an arc expression function that assigns an arc expression to each arc a such that T ype[E(a)] = C(p) M S .

9. I : P → EXP R ∅ is an initialisation function that assigns an initialisation expression to each place p such that T ype[I(p)] = C(p) M S .

Semantics

For CPN (P, T, A, Σ, V, C, G, E, I), we note:

• A marking is a function M that maps each place into a multiset of tokens.

• The initial marking M 0 is defined by M 0 (p) = I(p)⟨⟩ for all p ∈ P .

• The variables of a transition t are denoted by V ar(t) ⊆ V .

• A binding of a transition t is a function b that maps each variable v ∈ V ar(t) into a value b(v) ∈ T ype[v]. It is written as ⟨var 1 = val 1 , ..., var n = val n ⟩.
The set of all bindings for a transition t is denoted B(t).

• A binding element is a pair (t, b) such that t ∈ T and b ∈ B(t). The set of all binding elements BE(t) for a transition t is defined by

BE(t) = {(t, b)|b ∈ B(t)}.
The set of all binding elements in a CPN model is denoted BE.

A transition is said to be enabled if a binding of the variables appearing in the surrounding arc inscriptions exists such that the inscription on each input arc evaluates to a multiset of token colours present on the corresponding input place. Firing a transition consists in removing (resp. adding), from each input (resp. to each output) place, the multiset of tokens corresponding to the input (resp. output) arc inscription. The semantics of a CPN can be represented by a graph (reachability graph) where the initial state is the initial marking and an arc, labeled with a transition t, connects a marking m to a marking m ′ when t is firable from m and its firing leads to m ′ . For more details on CPN we refer readers to [START_REF] Jensen | Coloured Petri Nets: Modelling and Validation of Concurrent Systems[END_REF].

CPN Example

P1

Pn t1

(x, y) (x, y, x + y) Couple T ype T riplet T ype 1'(2, 5) + + 1'(4, 7) + + 1'(3, 2)
3

Figure 2.4: A simple example of a CPN model

To better explain the basic concepts of CPN, we use the simple CPN model of Fig. 2.4. Couple T ype is defined as the product of two integers and T riplet T ype as the product of three integers. x and y are two integer variables. In a CPN model, each place has a colour that determines the kind of data it can contain. We say that p1 is of colour (or type) Couple T ype and p2 is of colour T riplet T ype. Initially, the place p1 contains three tokens with different values (three different couples). The expressions on the arcs have to correspond to the colours of their respective places (e.g., the expression on the outgoing arc of p1 has to conform to its colour Couple T ype). In this CPN, (x, y) can be bound to any of the tokens in p1. For example, if it is bound to the first token (2,5), the firing of transition t1 results in consuming that token from p1 and producing a token with the value (2, 5, 7) in p2.

Figure 2.5 shows an example of a CPN model that could represent the previously described blind auction system (Listing 2.1). Evidently, the transitions bid, reveal and withdraw (in green) represent the execution of their namesake Blind Auction smart contract functions. The transitions in the user's behaviour box (i.e., bid Call, bid ACK, etc) are the equivalent of the activities/events that represent the smart contract's functions invocation by the bidder in the previous BPMN and DCR examples.

Linear Temporal Logic

The approach presented in this PhD work is primarily based on model checking of CPN models w.r.t formulae expressed in Linear Temporal Logic (LTL). This logic was first introduced in [START_REF] Pnueli | The temporal logic of programs[END_REF] as a means to reason about concurrent programs. In LTL, a classical timeline that starts "now" is considered, where every moment has a unique possible future. In other words, a model of LTL is an infinite sequence of indexed states (i = 0, 1, 2, ...) where each point in time has a unique successor. An LTL formula is evaluated over such a sequence of states starting from an i'th state. It contains a finite set P rop of atomic propositions, the usual Boolean operators ¬, ∧, ∨, and →, in addition to temporal operators:

• Until (U): φ U ψ is true if ψ is true now or φ is true now and remains so until ψ holds.

• Next (X or e ): X φ is true if φ is true in the next step.

• Globally (G or □): Gφ is true if φ is true in every step.

• Future (F or ♢): F φ is true if φ is true now or in some future time step.

Definition 2.4.2 (LTL formula). An LTL formula can be inductively defined as follows:

• ∀p ∈ P rop, p is an LTL formula.

• If φ and ψ are two LTL formulae, then

¬ φ, φ ∧ ψ, φ ∨ ψ, φ → ψ, φ U ψ, X φ, G φ and F φ are LTL formulae too.
The technique of model checking checks that a system, starting at a start state, satisfies a specification [START_REF] Rozier | Linear temporal logic symbolic model checking[END_REF].

An atomic proposition could be a state or event-based basic property. In this work, we consider hybrid linear-time temporal logic (hybrid LTL) formulae where both state-and event-based atomic propositions can occur. Therefore, we chose to represent the semantics (behavior) of a system by a Labeled Kripke Structure (LKS ).

Definition 2.4.3 (Labeled Kripke Structure (LKS)). Let AP be a finite set of atomic propositions and Act be a set of actions. An LKS over AP is a 5-tuple ⟨Γ, Act, L, →, s 0 ⟩ where:

• Γ is a finite set of states,

• L : Γ → 2 AP is a labeling (or interpretation) function, • → ⊆ Γ × Act × Γ is a transition relation, and • s 0 ∈ Γ is the initial state.
Given a CPN N and an initial marking m 0 the reachability graph of N could be considered as a LKS where the states are labeled with atomic propositions related to the places and where the set of actions Act is the set of transitions. Definition 2.4.4 (Hybrid LTL). Given a set of atomic propositions AP and a set of actions Act, a hybrid LTL formula is defined inductively as follows:

• each member of AP ∪ Act is a formula,

• if ϕ and ψ are hybrid LTL formulae, so are ¬ϕ, ϕ ∨ ψ, Xϕ and ϕ U ψ.

Other temporal operators, e.g. F (futur) and G (globally) can be derived as follows: F ϕ = true ∪ ϕ and Gϕ = ¬F ¬ϕ.

An interpretation of a hybrid LTL formula is an infinite run w = s 0 s 1 s 2 . . . (of some LKS ), assigning to each state s i a set of atomic propositions and a set of actions that are satisfied within that state. A p ∈ AP is satisfied by a state s i if it belongs to its label (i.e. L(s i )), while an action a ∈ Act is said to be satisfied within a state s i if it occurs from this state in w (i.e. (s i , a, s i+1 ) ∈→). In our case, where a single action can occur at a time (i.e. interleaving model of concurrency), at most one action can be assigned to a state of a run.

We write w i for the suffix of w starting from s i . Moreover, we say that p ∈ s i , for p ∈ AP ∪ Act, when p is satisfied by s i . The hybrid LTL semantics is then defined inductively as follows:

• w |= p iff p ∈ s 0 , for p ∈ AP ∪ Act, • w |= ϕ ∨ ψ iff w |= ϕ or w |= ψ, • w |= ¬ϕ iff not w |= ϕ, • w |= Xϕ iff w 1 |= ϕ, and • w |= ϕ U ψ iff ∃i ≥ 0 such that w i |= ψ and ∀ 0 ≤ j < i, w j |= ϕ.
An LKS K satisfies a hybrid LTL formula φ (K |= φ), iff all its runs do.

Model Checking

The goal of model checking is to verify that properties (specified in a temporal logic) are satisfied w.r.t a system (represented as a finite-state model). The general idea here is to construct the state space of the model, and to explore it in order to check a specification that is supposed to define the correctness of the system, and potentially generate counterexamples in case the specification was not met. The standard approach to do that would be to generate all the reachable states of the system, represent them individually and then exhaustively explore the state space to check for the specified property. The application of such a method would face a state space explosion problem in case of complex systems which constrains its application. That's why other model checking approaches appeared. BDD-based symbolic model checking (e.g., SMV [START_REF] Mcmillan | Symbolic model checking[END_REF]) presents a different way to store the states of the system, grouping them into sets of states represented by predicates on its state variables in the form of BDDs (Binary Decision Diagram). Such an approach reduces the size of the state space to be explored, making for a more efficient exhaustive exploration, yet it limits the nature of the variables that can be manipulated. Bounded model checking (e.g., SAT [START_REF] Biere | Symbolic model checking without bdds[END_REF], SMT [START_REF] Tinelli | Smt-based model checking[END_REF]) is another form of symbolic model checking that does not rely on a symbolic representation of the states of the system, but rather on applying decision procedures on prepositional logic. Such an approach turns the verification problem into a satisfiability problem. The goal here is to check if there exists values that can be assigned to the variables in the formula to be verified, so as it evaluates to false, within a certain number of exploration steps. While this approach overcomes the state space explosion problem, it cannot be considered complete since variable assignations under which the evaluation is false could exist beyond the considered search depth.

Complementary Techniques Symbolic model checking is often seen allied to other techniques in order to improve its efficiency or widen its application range. Abstractions (e.g., [START_REF] Anand | Symbolic execution with abstraction[END_REF]) can be used with symbolic model checking to deal with state space explosion in software analysis. An abstraction can be either sound, in which case properties of the abstract specification are also properties of the original one, or complete, in which case properties of the original specification are properties of the abstract one. While a sound (resp. complete) abstraction guarantees false positive-free (resp. false negative-free) results it cannot guarantee the absence of false negatives (resp. false positives). Symbolic execution (e.g., [START_REF] Khurshid | Generalized symbolic execution for model checking and testing[END_REF]) can be placed as the crossover between a formal verification technique and a testing technique for programs. Its underlying idea is to represent input variables using symbols over which the program is symbolically executed instead of assigning concrete values, which yields symbolic formulae instead of concrete results. Hence, one result of the symbolic execution encompasses a set of test cases. In such a context, SMT solvers are often used to check for the reachability of some part of the code, which amounts to checking the satisfiability of the conjunction of the formulae encountered on its corresponding path.

In this PhD work, we will be using the Helena model checker [START_REF] Evangelista | High level petri nets analysis with helena[END_REF] which is based on the automata-theoretic approach [START_REF] Vardi | An automata-theoretic approach to linear temporal logic[END_REF] for explicit model checking of LTL properties. As described in Figure 2.6, this approach starts by translating the LTL property φ to be verified into a Büchi automaton of its negation A ¬φ , and generation of the state space automaton A M of the input model M on the fly. The synchronized product of the two automata is then computed and used for the an emptiness check. This test indicates whether the synchronized product accepts an infinite word, in which case this word is returned as a counter example. We say that φ is satisfied under M if and only if the language of the synchronization product L(A ¬φ ⊗ A M ) is empty.

Conclusion

This chapter provided the background that helps position our contributions in the three main involved research fields. In fact, it introduced Solidity, the smart contracts language of Ethereum in which we are interested in this PhD work. Then, it presented different existing representation approaches for Business process models

LTL property φ

High-level model M

LTL translation

Negated property automaton A ¬φ

On-the-fly generation of state-space automaton A M On-the-fly synchronized product The last section of this chapter presented the arsenal of techniques that will be used throughout our contributions, namely model checking as formal verification method, Coloured Petri Net as a representation formalism and Linear Temporal Logic for the specification of the properties to be verified for the correctness of smart contracts.

L(A ¬φ ⊗ A M ) = L(A ¬φ ) ∩ L(A M ) On-the-fly emptiness check L(A ¬φ ⊗ A M ) ? = ∅ M |= φ or counter example

Chapter 3

State of The Art

Introduction

In this PhD thesis, we aim to provide a solution to support the formal verification of Solidity smart contracts used in a BPM context. Therefore, in this chapter, we review the current state of the art in order to justify our problem statement and to have a clear position regarding the existing work. We start by identifying various studies touching on the verification of smart contracts in Section 3.2, among which we select a few to present in detail and compare. Then, in Section 3.3 we shift the focus onto studies that treat the formal verification of diverse aspects of Business processes.

On the Verification of Solidity Smart Contracts

The different attacks on the different second-generation Blockchain platforms brought light on the various vulnerabilities that they may suffer from and acted as an effective incentive for experts to work on finding suitable solutions to the errors that may be at the source of such weaknesses. The efforts put into this quest took different directions (cf. Figure 3.1). Some solutions were based on informal methods while others aimed for more formal verification approaches. In this section, we start by an overview of the main informal techniques used for the verification of smart contracts and then we explore the formal techniques used for this purpose. We try to put together an exhaustive list of approaches for the verification of Solidity smart contracts. We resorted essentially to two sources in our quest, namely the Google Scholar search engine and the DBLP computer science bibliography, and used combinations of the following keywords for the search: smart contract, formal verification, Solidity and Ethereum. We then recursively pursued the references included in these papers' related work citations. We came out with a plethora of material, from which we selected 13 studies based on their relevance to the subject, the uniqueness of the proposed approach and the number of citations. Our selection was also guided by previous surveys that were conducted on more generic scopes. For instance, some studies did not focus on the formal aspect of the proposed verification approaches for Solidity smart contracts but rather on their analysis capabilities [START_REF] Angelo | A survey of tools for analyzing ethereum smart contracts[END_REF], while others chose to cover more smart contract languages [START_REF] Dwivedi | Formal-verification of smartcontract languages: A survey[END_REF] to the detriment of being exhaustive in their papers selection. In this section, we only explore studies related to Solidity as it is the language considered in this PhD thesis, and focus on verification proposals that use formal approaches, hence offering a more in-depth analysis of the existing formal verification approaches for Solidity smart contracts.

Informal Verification of Solidity Smart Contracts

Informal techniques are usually associated with validation rather than verification [START_REF] Adrion | Validation, verification, and testing of computer software[END_REF]. The most common techniques that fall under this category are testing and simulation.

In fact, one straightforward way to minimize the risk of deploying a vulnerable smart contract is to take advantage of one of the many existing testnets which are, as their name suggests, alternate Blockchains dedicated for testing purposes. A smart contract can, for example, be run on Ropsten [START_REF]Ropsten[END_REF] before its deployment on the mainnet, which may help with plain defects but not with imperceptible ones. A user can also resort to security companies such as MagicBlock-chainQA [6]. Such services are, however, both time-and money-consuming and do not guarantee in any case a fault-free smart contract. The Solcover testing tool [START_REF] Rea | SolCover: Code coverage for solidity smart-contracts[END_REF] was developed to offer a free and automatic testing experience of smart contracts. According to the tool's associated blog article, it "should only be treated as another arrow in a collective quiver", as it is unable to fully ensure the correctness of a smart contract. Instead of trying out scenarios that may or may not instigate erroneous behaviors, other researchers worked on enforcing security and best practices rules through linters [START_REF]Ethlint: (formerly solium) linter to identify and fix style & security issues in solidity[END_REF][START_REF]Solhint: Solhint project[END_REF][START_REF] Bond | Solcheck: A solidity linter written in js[END_REF][START_REF] Dodson | Solint: A linting utility for ethereum solidity smart-contracts[END_REF], which are tools that analyze the code to identify and flag programming and stylistic errors or suspicious constructs.

Such informal techniques may offer the convenience of quickly checking whether a system would meet some requirements if executed within a specific scenario (or set of scenarios), but they cannot, however, offer any guarantees of correctness as one cannot be expected to manually test all possible scenarios or predict them for that matter.

Formal Verification of Solidity Smart Contracts

While informal methods may reduce the risk of bugs in smart contracts, relying solely on such techniques cannot be enough to get a full insurance that a smart contract would be correct. Formal verification techniques can overcome this weakness, though it may come at the expense of other challenges such as scalability. Such techniques are used to check the conformance of the developed system to a predefined specification. They are based on formal methods of mathematics and are able to provide formal proof of the correctness of the investigated system with reference to its formally specified behavior. We can distinguish mainly two families of formal verification methods, namely those based on theorem proving and those based on model checking.

Verification Approaches Based on Theorem Proving

Some researchers proposed theorem proving-based approaches for the verification of Solidity smart contracts. The authors in [START_REF] Bhargavan | Formal verification of smart contracts: Short paper[END_REF] propose Solidity* a prototype tool, implemented in OCaml, that allows the translation of a restricted subset of Solidity into F*, a functional programming language for program verification. In order to detect dangerous patterns, the user then needs to define effects in F* code which are discharged by the F* type-checker. They also propose EVM*, a decompiler for EVM bytecode into F*, along which they propose a model for the cost of bytecode operations which can be used by creating annotations for gas-related violations that can be discharged by the F* type-checker. Using this approach requires, not only expertise in F*, but also an understanding of the proposed translation in order to be able to express the patterns to be checked and understand the generated typechecking errors. Members of the Ethereum community present a prototype for verification integrated into the Solc compiler of Solidity [4]. Their proposition leverages the Why3 IDE, a theorem prover which can be used on the WhyML code generated by calling Solc with specific attributes. Other partial translations of the EVM bytecode based on assisted proofs like Coq [START_REF] Hirai | Ethereum vm for coq (v0.0.2)[END_REF] and Isabelle/HOL [START_REF] Amani | Towards verifying ethereum smart contract bytecode in isabelle/hol[END_REF] exist. We note that none of these approaches offer automatic verification of smart contracts.

Verification Approaches Based on Model Checking

Other researchers proposed model-checking-based approaches for the verification of Solidity smart contracts. Table 3.1 presents a categorization of these works depending on the used techniques. Oyente [START_REF] Luu | Making smart contracts smarter[END_REF] was the first attempt at formal smart contract verification. It uses symbolic execution applied at the EVM bytecode of the contract to generate symbolic execution traces among which it looks for certain conditions that translate the presence of one of the four vulnerabilities it targets. This proposition actually paved the way for other researchers who wanted to do better in several subsequent studies. Some of them reused it as part of their own tools, like in GASPER [START_REF] Chen | Under-optimized smart contracts devour your money[END_REF] which exploits the by-product of Oyente (CFG) in its detection of costly bytecode patterns in terms of gas consumption. Other researchers opted for extending Oyente to detect different/additional bugs (e.g., MAIAN [START_REF] Nikolic | Finding the greedy, prodigal, and suicidal contracts at scale[END_REF], SASC [START_REF] Zhou | Security assurance for smart contract[END_REF] and Osiris [START_REF] Torres | Osiris: Hunting for integer bugs in ethereum smart contracts[END_REF]). Securify [START_REF] Tsankov | Securify: Practical security analysis of smart contracts[END_REF] is a security analysis tool for Solidity smart contracts. It starts by decompiling the EVM bytecode into a static-single assignment form and symbolically encoding the corresponding dependence graph in stratified DataLog, leverages the Soufflé solver to derive semantic facts on the contract's data-and control-flow dependencies using declarative inference rules and then checks for the presence of predefined patterns that correspond to the properties the user wants to verify. In fact, the authors use a designated DSL to define compliance (resp. violation) patterns for a number of properties to capture sufficient conditions in a given code to satisfy (resp. violate) such properties. Even though the user can define other patterns to check for additional security properties, it is not possible to define patterns that match a contract-specific property, or arithmetic properties. Besides, in some cases the code does not match any defined pattern and cannot decide on the safety of the contract. Vandal [START_REF] Brent | Vandal: A scalable security analysis framework for smart contracts[END_REF] follows the same spirit and adopts a logic-driven program analysis approach. It starts by translating the EVM bytecode into an abstract register transfer language exposing its data-and control-flow structures. This language is then translated into logic relations which are then fed to security analyses written in Soufflé to detect certain vulnerabilities in the contract.

A Selection of Prominent Tools for the Formal Verification of Solidity Smart Contracts

Among the studies that we have collected on formal verification of Solidity smart contracts, four can be categorized as theorem proving-based approaches and 9 make use of model checking-related techniques. We note that, despite this second category representing a majority, only one work proposed an approach fully based on model checking in the proper sense of the word (cf. Table 3.1). Such propositions are rather walking the line between being formal verification-based and testing-based approaches.

In the following subsections, we present four selected approaches proposed for formal verification of smart contracts, presented in bold in Table 3.1. We choose to detail the two approaches presented in [START_REF] Luu | Making smart contracts smarter[END_REF] and [START_REF] Kalra | ZEUS: analyzing safety of smart contracts[END_REF], the two approaches with the most cited papers, as well as [START_REF] Mavridou | Designing secure ethereum smart contracts: A finite state machine based approach[END_REF][START_REF] Mavridou | Verisolid: Correct-bydesign smart contracts for ethereum[END_REF] for being the single approach based on model checking. We also single out the approach in [START_REF] Torres | Osiris: Hunting for integer bugs in ethereum smart contracts[END_REF] as one of the propositions based on the veteran Oyente [START_REF] Luu | Making smart contracts smarter[END_REF].

Throughout the rest of this section we will be using the illustrative contracts in Listings 3.1 and 6.2 to test the different tools proposed in the selected studies. We note that these contracts are written for illustration and do not exhibit a logical functionality.

contract Approach In [START_REF] Mavridou | Designing secure ethereum smart contracts: A finite state machine based approach[END_REF] the authors propose an FSM-based approach for the design of secure smart contracts. The premise of their work is that writing smart contracts in a language such as Solidity is error-prone because the smart contract writer may not fully grasp the semantics driving the execution process which often leads to a contract that does not reflect the actual intentions of its creator. They hence aim at closing this semantic gap by developing the FSolidM tool which allows users to design a smart contract as an FSM (Finite State Machine) which is then automatically transformed into a Solidity smart contract. To do so, they propose a definition of a smart contract as an FSM and outline the transformation process that generates the corresponding Solidity smart contract.

To improve the generated smart contract's security, the authors propose so called "plugins" that prevent some common vulnerability patterns [START_REF] Atzei | A survey of attacks on ethereum smart contracts (sok)[END_REF]. These plugins actually translate into modifiers appended to the contract's functions to be secured. In Solidity, a modifier is used to change the behavior of the functions with which it is associated. In this context, modifiers are used to implement security patterns into the generated Solidity functions, e.g., by adding preconditions to check prior to their execution.

The work presented in [START_REF] Mavridou | Designing secure ethereum smart contracts: A finite state machine based approach[END_REF] was in fact laying ground for the next paper [START_REF] Mavridou | Verisolid: Correct-bydesign smart contracts for ethereum[END_REF] in which the authors present VeriSolid, the improved version of FSolidM. In fact, [START_REF] Mavridou | Verisolid: Correct-bydesign smart contracts for ethereum[END_REF] extends [START_REF] Mavridou | Designing secure ethereum smart contracts: A finite state machine based approach[END_REF] in that it adds formal operational semantics to the formerly proposed FSolidM model and therefore extends the Solidity code generator. This upgrade introduces the aspect of formal verification into the tool, which provides the user with the ability to specify intended behavior in the form of liveness, deadlock freedom and safety properties. It offers customizable templates to express and check some CTL properties by a backend symbolic model checker.

Tool The FSolidM tool offers four plugins to deal with four types of vulnerabilities:

(1) a locking plugin against the reentrancy attack pattern, (2) a transition counter plugin to enforce transition ordering and avoid falling into unpredictable states, (3) an automatic timed transitions plugin to implement time-constraint patterns and (4) an access control plugin to manage authorization for the execution of certain functions.

While VeriSolid extends FSolidM, it does not take into account the same vulnerabilities as the latter since it offers the possibility to express CTL properties through templates such as "transition b will eventually happen after transition a" which can be used to check for a denial-of-service vulnerability. Additionally, the authors chose to deal with the reentrancy vulnerability intrinsically by automatically introducing an In-Transition state into which the system goes at the beginning of each transition, thus prohibiting any overlapping calls.

In order to incorporate the formal verification aspect, the authors resort to using the NuXmv symbolic model checker [START_REF] Cavada | The nuxmv symbolic model checker[END_REF] which features SMT-based techniques for the verification of infinite state systems. For that, they opt for augmenting the initial FSM model to take in the semantics of the Solidity functions' statements, transforming the resulting augmented model into a BIP (Behavior-Interaction-Priority) transition system [START_REF] Basu | Rigorous component-based system design using the BIP framework[END_REF] (which is guaranteed to be deadlock-free), using an existing BIP2NuSmv transformation tool and feeding the result to the NuXmv model checker along with the CTL formulae following the provided properties templates. For lack of an underlying Figure 3.2: Screenshot of the VeriSolid tool -1 business logic in our example in Listing 3.1, we choose to test the tool on a small example for reentrancy. We note that in this model we distinguish the first call to deposit (InitialDeposit) from the rest to get around a modeling restriction that requires the system to contain a minimum of 2 states. We tested this code and confirmed its insusceptibility to reentrancy. Figure 3.3 shows the representation using VeriSolid of the property stating that the function Withdraw can only be called after the InitialDeposit function had been called, along with its verification result.

Discussion

In the attempt to integrate the formal verification aspect into the approach, the first premise of closing the semantic gap of Solidity got disregarded since the statements constituting the functions' bodies need to be provided by the user in Solidity. On the practical side, it may feel counter-intuitive and even restrictive for the user to have to think about the smart contracts they want to write in terms of states at design time, only to find themselves writing the code themselves nonetheless. Moreover, despite the help that may come with the proposed templates for CTL properties for some users, they might as well be seen as an unnecessary restriction to some other more experienced users who would like to verify more complicated properties that cannot be expressed within the limits of the provided templates. As much as some guidance is appreciated, it should not turn into a barrier to expressivity.

Last but not least, it is important to mention that the models in both FSolidM and VeriSolid do not take into account any variables. Therefore, no properties on the evolution of the values of the variables during the execution of the smart contract can be verified, which also cuts back considerably on the range of properties the user can check.

ZEUS

Approach Zeus [START_REF] Kalra | ZEUS: analyzing safety of smart contracts[END_REF] is a framework based on symbolic model checking for the verification of smart contracts. It takes as input a smart contract written in a high-level language along with a so-called policy that contains the criteria to be checked and which the user needs to specify in an XACML-styled template. The input smart contract code is then instrumented with assertion instructions according to its corresponding policy by means of static analysis and is passed on to a translator that the authors had devised to convert it into a low-level intermediate representation (LLVM bitcode) which is then fed to an existing verification engine in order to assert the safety of the smart contract. This is based on the primary description of the approach. As more details are later presented in the paper, we realize that this is not actually the exact right ordering of steps since the static analysis is afterwards said to be performed on top of the intermediate representation rather than the highlevel code and the same goes for the added assertions. Later on, we also realize that the high-to-low level transformation is not straightforward. The authors propose an abstract language into which Solidity code is transformed before undergoing the first transformation into LLVM bitcode.

As to the considered properties, the authors distinguish two main families of vulnerable smart contracts: incorrect and unfair smart contracts. They define correctness as the adherence to safe programming practices and fairness as the adherence to agreed upon higher-level business logic. An incorrect smart contract can have one of the following vulnerabilities: (1) reentrancy, (2) unchecked sends, (3) failed sends, (4) integer overflow/underflow or (5) transaction state dependence. An unfair smart contract can have one of the following vulnerabilities: (1) absence of logic, (2) incorrect logic or be (3) logically correct but unfair. Besides vulnerabilities that fall under these two categories, two more vulnerabilities which can actually be caused by the miner's influence are introduced: (1) block state dependence (BSD) and (2) transaction order dependence (TOD).

Tool Zeus was not made available online, but the authors state that they have implemented a prototype in C++. The tool's main components are the policy builder and the Solidity-to-LLVM bitcode translator. For the former, they leverage the AST output produced by the Solc compiler and taint analysis on the source code to extract the information needed to assist the user in forming the conditions to verify. As for the translator, it takes as input the smart contract and uses existing LLVM APIs to generate the bitcode, which will then be instrumented by adding assertions according to the built policy. As a backend verifier, they opt for Seahorn [START_REF] Gurfinkel | The seahorn verification framework[END_REF].

Discussion Proposing an abstract interpretation language for Solidity to go through before obtaining an LLVM bitcode contributes in improving the scalability of Zeus. In fact, using over-approximations and reducing functions into summaries and loops into data domains results in a reduced state space for the symbolic model checker to be used later. However, a formal reasoning still needs to be established to prove the actual semantic equivalence between the two languages (Solidity and the proposed abstract language). Furthermore, the authors mention that using the abstract language allows the support of multiple Blockchain platforms, yet we think that using this bridge language constrains the high-level languages the tool can support. To integrate a language other than Solidity, new correspondences with the proposed abstract language would have to be defined (if not the whole language), the translation into LLVM would have to be revised and the automation of the assertions insertions would have to be reimplemented.

Leveraging the use of the LLVM bitcode extends the reach of Zeus in the sense that it can make use of any backend symbolic model checker supporting that standard. Seahorn [START_REF] Gurfinkel | The seahorn verification framework[END_REF] is the first choice of the authors but not the only one. It was chosen for its ability to generate verification conditions using CHCs (Constrained Horn Clauses) over LLVM bitcode. Other symbolic model checkers can be used, such as SMACK [START_REF] Rakamaric | SMACK: decoupling source language details from verifier implementations[END_REF], but that may require some modifications on the LLVM bitcode as for example some model checkers might use different lengths for the same type which needs to be taken into account when switching the verifier. The authors state that CHCs are suitable for the representation of verification conditions, but do not elaborate. We think that the tool may be able to verify a wider range of properties if it were to support the representation of properties using other logics besides CHC.

Another point to mention is that Zeus can only account for parameters that can be computed at the source code level and hence cannot verify properties relating to parameters as gas consumption.

OYENTE

Approach Besides the smart contracts analysis tool they call Oyente, the authors of [START_REF] Luu | Making smart contracts smarter[END_REF] also propose refinements/recommendations to Ethereum's protocol in the form of improvements to its operational semantics (e.g., new rules for transactions execution) in order to fix certain security problems. In this survey, we are only interested in the Oyente tool that they propose as a "pre-deployment mitigation". It is based upon symbolic execution and it functions over the contract's bytecode which needs to be provided as input along with Ethereum's global state. The latter would serve as an initialization for the contract's variables. Message call-related variables are however treated as input symbolic values. The general idea behind Oyente is to symbolically explore a control flow graph corresponding to the contract's bytecode by symbolically executing instructions within states of that graph and using a symbolic constraint solver to decide on the feasibility of branching conditions. The possible presence of certain vulnerabilities is detected by checking for specific conditions in the generated symbolic traces.

This tool targets four specific vulnerabilities: (1) TOD, (2) timestamp dependence, (3) mishandled exceptions and (4) reentrancy.

Oyente signals whether the contract in question has one of the aforementioned problems and provides an example of a symbolic path to illustrate the possible problem to the user. The authors hope to turn Oyente into an interactive debugger as future work.

Tool Oyente [START_REF] Luu | Making smart contracts smarter[END_REF] is implemented in Python, uses Z3 [START_REF] De Moura | Z3: an efficient SMT solver[END_REF] as a backend SMT solver and detects the four discussed problems (see 3.2.3.3). Its design has four main components:

• CFGBuilder: it outputs a Control Flow Graph of the bytecode. This graph is only partly constructed statically as some edges are later added after symbolic execution.

• Explorer: this is mainly an interpreter loop that symbolically executes one instruction at one state at a time, starting from the entry node of the CFG generated by the previous component. The Explorer actually simulates the behaviour of EVM instructions and makes use of Z3 to decide on path conditions. The loop ends when no more unexplored states exist or when a timeout is reached.

The CFG is potentially enriched by the end of this phase and a set of symbolic traces is outputted.

• CoreAnalysis: it in turn comprises four components to detect the four previously introduced bugs. These components work by checking specific conditions when analyzing the symbolic traces resulting from the Explorer in order to flag the possible presence of the corresponding bugs.

• Validator: this step is added to further reduce the rate of false positives. The user, however, still needs to intervene to confirm that the flagged bugs are a real threat.

The tool has been in active development up until May 2018, and some unreported features were added to the updated version. Mainly, in its latest version, Oyente can supposedly detect the following issues (in addition to the previously mentioned issues): (1) integer overflow/underflow, (2) Parity Multisig bug 2 and (3) callstack depth attack. Despite its ability to detect important vulnerabilities in smart contracts, Oyente is not a complete verifier. Its major drawback is that its reported errors may be spurious. In other words, its results may contain false positives. One example for that is flagging a false reentrancy vulnerability in a code that uses a send function, which should not pose a threat unless its default gas were altered. This can actually be explained by the fact that Oyente relies on the bytecode of the smart contract, in which both functions send and call are mapped to the same CALL bytecode, which translates into contextual information loss. To detect reentrancy, the tool checks the path condition before each CALL it comes across and checks if it still holds after the bytecode's execution, in which case it is registered as a vulnerability.

OSIRIS

Approach Like in the previous study, in addition to proposing a verification approach, the authors in [START_REF] Torres | Osiris: Hunting for integer bugs in ethereum smart contracts[END_REF] indicate some ways to protect smart contracts against certain attacks by introducing modification to the EVM semantics as well as the Solidity compiler. We are only interested in their main contribution which is the proposed verification framework. This work specifically targets integer vulnerabilities in Solidity smart contracts. More precisely, the authors investigate the presence of 3 types of bugs in such contracts: (1) arithmetic bugs like integer underflows/overflows and bugs caused by divisions where the denominator is zero, (2) truncation bugs which can happen when converting a value into a new type with a shorter range than that of its initial type and (3) signedness bugs that can occur when converting a signed integer typed value into an unsigned integer type (or the opposite). This approach works on integer bugs detection at the bytecode level and is based on two techniques, namely symbolic execution and taint analysis. It comprises 3 phases:

• Integer type inference: even though Solidity is a statically typed language, typing information is supposed to get lost at the bytecode level. The compiler, however, leaves behind discrete trails (e.g., AND bitmask, SIGNEXTEND opcode, etc) that the authors track down to deduce the size and sign of integers in the bytecode.

• Integer bugs detection: a different detection technique is proposed for each of the targeted integer bug types:

arithmetic bugs: a constraint is emitted to the backend solver for each arithmetic instruction. This constraint is formed so that it is only satisfied if a set of predefined in-bounds requirements specific to the instruction in question are not totally met. Consequently, a bug is detected if one of the emitted constraints under some path conditions is found to be satisfiable by the solver.

truncation bugs: such bugs are detected by tracking the instructions used by Solidity to perform truncation (i.e., AND and SIGNEXTEND for signed and unsigned integers). A constraint is formed for such instructions as to be satisfied if the input value is larger than the output. Consequently, a truncation bug is detected if one of the emitted constraints under some path conditions is found to be satisfiable by the solver, all while ignoring two specific patterns for intentional truncation corresponding to truncation due to a conversion to type address and truncation as a technique to fit more than one variable into the same storage slot.

signedness bugs: for this type of bugs, the authors reuse an approach that was initially proposed for Linux programs [START_REF] Molnar | Dynamic test generation to find integer bugs in x86 binary linux programs[END_REF] and adapt it for Solidity smart contract. The gist of the applied method is to infer information on signed and unsigned types on the values from the executed EVM instructions and spot the symbolic variables that can be assigned both types.

• False positives reduction: the authors actually consider this as two separate steps, since they use two different techniques to reduce the rate of generated false alarms. The first step is to apply taint analysis in order to check only instructions whose input data is tainted (can be manipulated by an attacker) and further validate only the ones that touch sensitive locations (can be harmful in that they may alter the execution path, storage and ether flow). The second step of false positives reduction is recognizing detected integer bugs which originate from unharmful code such as an intentional check (if condition) meant to catch an overflow bug.

Tool The implemented tool called Osiris is written in Python. It operates over the bytecode but can accept Solidity code as input which it internally compiles into bytecode. It consists of 3 main components: (1) symbolic analysis is basically a reuse of the previously presented Oyente tool, used to generate the bytecode's CFG and symbolically execute its instructions, (2) taint analysis checks, for each executed instruction, whether it pertains to a specific set of instructions defined by the authors as susceptible of being used by an attacker, in which case the locations it affects (in the stack, memory and storage) are tagged and the propagation is carried out according to the EVM semantics. It then checks if this instruction can be impactful on sensible locations and (3) integer error detection is called upon the instructions detected by the taint analysis, implements the errors detection methods discussed above and uses Z3 to check for the feasibility of the created constraints.

Figure 3.5 shows the result for running Osiris on our example in Listing 3.1. The tool detected an overflow bug as well as a truncation bug and located them in the code.

Figure 3.5: Screenshot of the Osiris tool

Discussion This work focuses on a restrictive range of vulnerabilities, covering specific integer-related bugs. On the one hand, the approach shows better results than other existing approaches dealing in part with such vulnerabilities, yet its range of application is thereby restricted. Additionally, Osiris points out the origin of the detected vulnerability in the analysed code but does not provide an example of an execution that may lead to an error, which would make it easier for the contract writer to revise the code. commercialized version of Securify [START_REF] Tsankov | Securify: Practical security analysis of smart contracts[END_REF]. We also note that 4 approaches give the user the ability to express customized properties to check. None of them, however, supports contract-specific properties. Moreover, we underline that only single function reentrancy is considered in all of the existing approaches. Furthermore, none of the proposed approaches deals with the verification of interacting contracts. This means that the verification of smart contracts is a field that, despite having been investigated at an early stage, still needs to be further studied to achieve correctness in smart contracts and consolidate the desired trust in the Blockchain environment.

In the following we report tools comparisons included in their corresponding papers.

Zeus vs Oyente in [START_REF] Kalra | ZEUS: analyzing safety of smart contracts[END_REF] The evaluation of Zeus was done on a dataset of 1524 smart contracts and its results were compared to Oyente's for the commonly treated vulnerabilities (reentrancy, unchecked send, BSD and TOD). 54 contracts were reported by Zeus to be vulnerable to reentrancy against 265 by Oyente. The undetected bugs by Zeus were said to be false positives caused by Oyente considering reentrancy possible with send calls. This is not totally true, as using send can still be susceptible to reentrancy if the allocated amount of gas were to be manually increased. For the unchecked send vulnerability, Zeus was reported to detect 324 bugs with 3 false positives, against 112 bugs by Oyente with 89 false positives. The results for BSD show more detected bugs by Zeus than Oyente, which is only logical since the former considers multiple block variables while the latter only considers the block's timestamp. Zeus is also reported to detect more TOD bugs (607) than Oyente (126) with a lower false alarm rate.

Osiris vs Zeus in [START_REF] Torres | Osiris: Hunting for integer bugs in ethereum smart contracts[END_REF] The authors of [START_REF] Torres | Osiris: Hunting for integer bugs in ethereum smart contracts[END_REF] evaluated their tool using a subset of the dataset of smart contracts previously used by Zeus (they retrieved 883 out of 1524 contracts), and compared it to the latter for their commonly detectable bugs. Their reported results show a big difference in the number of detected integer overflow/underflow bugs with Zeus detecting 628/883 and Osiris detecting 172/883. They claim that this difference can be explained by Zeus prioritizing completeness over the real exploitability of its reported bugs. They also bring into question Zeus's soundness by manually investigating 5 contracts that were reported as containing bugs by Osiris but not by Zeus and confirming their unsafety. [START_REF] Zhou | Security assurance for smart contract[END_REF] In their comparison with Oyente, the authors in [START_REF] Zhou | Security assurance for smart contract[END_REF] report more detected timestamp dependence bugs using their tool (866 by SASC against 292 by Oyente out of 2952 contracts). In fact, this can be explained by the different ways both tools use to target such a vulnerability. While Oyente detects the use of timestamp whenever it is related to ether transfer only, SASC proceeds differently by targeting its use in other operations as well. We also note that SASC is able to locate the bugs in the corresponding code, unlike Oyente that only signals their presence.

SASC vs Oyente in

Securify vs Oyente in [START_REF] Tsankov | Securify: Practical security analysis of smart contracts[END_REF] Results were compared to Oyente in [START_REF] Tsankov | Securify: Practical security analysis of smart contracts[END_REF] for the detection of reentrancy, TOD and mishandled exceptions. The authors report better results overall for Securify. Reentrancy was detected in the same number of contracts by both tools, with presence of false positives with Oyente but not with Securify. As for the other two vulnerabilities, Securify was reported to detect more valid occurrences than Oyente and no false negatives at all, albeit with a slightly higher number of false positives.

Coloured Petri Nets for Smart Contracts

More recently, attempts have been made to use Coloured petri net for the verification of smart contracts. The work in [START_REF] Liu | Formal verification of blockchain smart contract based on colored petri net models[END_REF] shows an example of verification of behavioural properties on a CPN model for a crowdfunding smart contract. It does not, however, propose a complete and generic approach to apply on any smart contract as the work merely presents case study of a manual passage from the use case's contract to the CPN model without defining general rules for the transformation. Another CPN-based proposition was presented in [START_REF] Duo | Formal analysis of smart contract based on colored petri nets[END_REF]. The authors start from the contract's bytecode and use Hoare's logic to generate the corresponding CPN model which is then used for the security analysis of the contract. This approach, despite being based on CPN, cannot be used for the verification of data-flow related properties as the generated model focuses on the representation of the workflow extracted from the contract's CFG.

On the Verification of Business Process Models

A primordial phase in the life cycle of a business process is its verification. In order to avoid execution mishaps whose gravity may vary with the level of criticality of the modeled system, the designer needs to make sure that the model will actually satisfy a set of requirements/specifications that define the correctness of the system. This matter has been studied extensively in the case of imperative representations, as can be seen by the survey conducted in [START_REF] Morimoto | A survey of formal verification for business process modeling[END_REF]. BPMN being one of the most widely used modeling languages for business processes, it is fairly easy to find in the literature many studies that focus on the formal verification of various aspects of BPMN models [START_REF] Bryans | Formal analysis of BPMN models using event-b[END_REF][START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF][START_REF] Gaaloul | Event-based design and runtime verification of composite service transactional behavior[END_REF][START_REF] Ou-Yang | Bpmn-based business process model feasibility analysis: a petri net approach[END_REF][START_REF] Puhlmann | Using the pi -calculus for formalizing workflow patterns[END_REF][START_REF] Ye | Formal semantics of bpmn process models using yawl[END_REF]. In such studies, it is frequent to encounter Petri nets as a formalism used to add a formal aspect to the semantics of BPMN. In [START_REF] Dijkman | Semantics and analysis of business process models in BPMN[END_REF], the authors propose a mapping of the core elements of the BPMN language into labelled Petri nets patterns. This mapping was then implemented into a tool that automated the generation of the Petri net and helped the semantic analysis of the modeled process. Another Petri-net-based approach was proposed in [START_REF] Ou-Yang | Bpmn-based business process model feasibility analysis: a petri net approach[END_REF] with the aim of analysing the feasibility of BPMN processes, this time using Colored Petri nets as a target formal representation and a modified BPEL4WS representation as a pivot language. YAWL is another important modeling language for business processes. It is based on Petri nets and extended with specific concepts to easily model complex workflows. An automation of the transformation of BPMN models into YAWL was proposed in [START_REF] Ye | Formal semantics of bpmn process models using yawl[END_REF] with the aim of verifying them using specific tools such as Woflan [START_REF] Verbeek | Woflan 2.0: A petri-net-based workflow diagnosis tool[END_REF]. The aforementioned studies merely mark the starting point of the research on the verification of business processes. Several other studies followed on the same path, using extensions of Petri nets to take into account more complex models [START_REF] Kheldoun | Formal verification of complex business processes based on high-level petri nets[END_REF], and focusing on specific aspects such as in [START_REF] Boubaker | A formal model for business process configuration verification supporting or-join semantics[END_REF][START_REF] Houhou | A first-order logic verification framework for communication-parametric and time-aware BPMN collaborations[END_REF].

Other formal methods have been used for the verification of business processes like π-calculus in [START_REF] Puhlmann | Using the pi -calculus for formalizing workflow patterns[END_REF], event calculus in [START_REF] Gaaloul | Event-based design and runtime verification of composite service transactional behavior[END_REF] and theorem proving in [START_REF] Bryans | Formal analysis of BPMN models using event-b[END_REF].

Similar to the imperative languages of business process modelling, the emergence of the declarative modelling mode needs to be accompanied by suitable tools that would allow the verification of its models. In fact, the implicit nature of the representation of the workflow makes it less obvious to be interpreted by the designers and therefore makes it easier for simple modelling errors to pass unnoticed. Moreover, the dynamic and complex nature of the domains that require flexible models puts more at stake and adds to the importance of having a verification tool that would insure the correctness of the process model. However, compared to the rich state of the art on the verification of imperative business process models, we notice a significant scarcity in research on the verification of declarative models.

Conclusion

This chapter serves to present different approaches that are relevant to our work. First, we reviewed the existing work on the verification of Solidity smart contracts. We gave an overview of the solutions that use informal techniques and focused on those that use formal techniques. We classified those into two main categories: (1) approaches based on theorem proving and (2) approaches based on model checking, which we then sub-categorized based on i the exact technique used for the verification and ii their ability to verify the common vulnerabilities and possibility to verify other properties. We selected four studies based on their relevance to our work and their citation score, to present in detail, discuss and compare. Then we provided an overview of the use of formal verification in context of BPM, showcasing the importance of this phase in relation to different aspects of the Business processes.

Despite the multiple studies proposing formal verification approaches for Solidity smart contracts, we showed that most of them use symbolic execution which leads to incomplete verification results, and that none of them gives the users the possibility to freely express the properties to be verified on their smart contracts, especially properties that can depend on the data-flow of these contracts. This last point can be very useful particularly if the behavioural context in which the smart contracts are to be used is well specified, in which case it would be interesting to verify the smart contracts with regard to properties expressed on this context. Given that such a context can intuitively be specified as a Business process, we also showed the significant attention bestowed on the formal verification of Business process models and highlighted the contrast between the literature on imperative representations against that on declarative representations to conclude that the formal verification of declarative models is still not mature. This further corroborates the need for the verification of smart contracts especially when accompanied with a behavioural context specification. We lead off by setting some notations on the elements of the model in Section 4.2 before getting into the algorithms in Section 4.3.

Defining the Elements and Notations for our CPN Models

In this section, we give details on the different elements that we use in our proposed algorithms for the construction of the our CPN building blocks.

Transitions T

We distinguish two types of transitions in the sub-models:

1. aggregated transitions (T A ): used for the modular representation of function calls. They are transitions that can be substituted by sub-models.

2. regular transitions (T R ): are simple unsubstitutable CPN transitions.

For a transition t ∈ T we note: We define 4 types of places according to the role they play:

• t.
• Control flow places P CF are places created to implement the order of execution of the workflow. We also use them to carry data related to the state of the smart contract which can be defined by its balance and the values of its state variables. Such places have a metaColour defined at each aggregated transition of level-0 as the concatenation of the state and the input parameters: [uint: contractBalance, type v 1 : stateVariable 1 , ..., type vn : stateVariable n , type p 1 : inputParameter 1 , ... , type pn : inputParameter n ].

• Data places P data (for internal local variables) where each place is of a colour corresponding to the represented variable's type.

• Parameter places P P that convey potential inputs of function calls. Each function call has an associated parameter place whose colour is as follows [type p 1 : inputParameter 1 , ..., type pn : inputParameter n ].

• Return places P R that communicate potential functions' returned data. Each function call has an associated return place whose colour corresponds to the return type of the called function.

Expressions E

An expression is a construct that can be made up of literals, variables, function calls and operators, according to the syntax of Solidity, that evaluates to a single value.

For ease of representation, we define three types of expressions:

• expressions with variables E V : are expressions that make use of at least one local variable. In such an expression e v , the set of variables used is accessible via e v .vars.

• expressions with function calls E F : are expressions that make use of at least one function call. In such an expression e v , the set of function calls used is accessible via e v .f ctCalls

• constant expressions E C : are expressions that do not make use of any variables nor function calls.

We note that an expression e can of course have both variables and function calls (e ∈ E V ∩ E F ).

Statements S

In this work, we cover the core features of the Solidity language according to the definition of its grammar [5]. While we do not take into account all the Solidity elements, the ones that we support can be considered exhaustive in the sense that they can be used to rewrite smart contracts that include more syntactic sugar. We note however, that we do not support smart contracts that include raw assembly code in them as our main focus is the verification of the Solidity high-level code.

A statement st ∈ S can be either a compound statement {st [1]; st [2]; . . . ; st[N ]} (where ∀i ∈ [1..N ], st[i] ∈ S), or a simple statement (st LHS , st RHS ) (where st LHS ∈ E and st RHS ∈ E), or a control statement. A simple statement can be:

• a function call statement, where:

st LHS = ∅ st RHS .vars designates the set of variables used in the arguments of the call (if st RHS ∈ E V )

• an assignment statement, where:

st LHS ∈ E V and st LHS .vars contains only one variable that designates the assigned one st RHS .vars designates the set of variables used in the assignment expression (if st RHS ∈ E V )

st RHS .f ctCalls designates the set of function calls used in the assignment expression (if st RHS ∈ E F )

• a variable declaration statement, where:

st LHS ∈ E V and st LHS .vars contains one variable that designates the declared one st LHS .type designates the type of the declared variable st RHS .vars designates the set of variables used in the variable initialization expression (if the variable is initialized and st RHS ∈ E V ) st RHS .f ctCalls designates the set of function calls used in the variable initialization expression (if the variable is initialized st RHS ∈ E F )

• a sending statement, where:

st LHS designates the destination account st RHS .vars designates the set of variables in the expression of the value to be sent (if st RHS ∈ E V ) st RHS .f ctCalls designates the set of function calls in the expression of the value to be sent (if st RHS ∈ E F )

• a returning statement, where:

st LHS = ∅ st RHS .vars designates the variables in the expression of the returned value (if st RHS ∈ E V ) st RHS .f ctCalls designates the function calls in the expression of the returned value (if st RHS ∈ E F )

A control statement can be:

• a requirement statement of the form require(c)

• a selection statement which can have:

a single-branching form: if (c) then st T a double-branching form: if (c) then st T else st F

• a looping statement which can be:

a for loop: f or(init; c; inc) st T a while loop: while(c) st T

• where:

c is a boolean expression c.vars designates the set of variables used in the condition (if c ∈ E V ) c.f ctCalls designates the set of function calls used in the condition (if c ∈ E F ) st T , st F , init and inc are statements (or blocks of statements)

Additional Notations

For a smart contract SC we note:

• SC.vars, the set of state (i.e., global) variables of SC • SC.f cts, the set of functions of SC For a place p ∈ P we note:

• p.name, the name of the place p • p.colour, the clour of the place p For a transition t ∈ T we note:

• •t[cf ] ∈ P CF ∪ P S , the input control flow place of t • •t[input] ∈ P P , the input parameters place of t • •t[data] ⊆ P data , the input data places of t • t • [cf ] ∈ P CF ∪ P S , the output control flow place of t • t • [output] ∈ P R , the output return place of t • t • [data] ⊆ P data ,
the output data places of t

Solidity-to-CPN: Preparing the Building Blocks

In the following, we present our proposed algorithms for the transformation of each of the statement types in Solidity. It is worth mentioning that in our approach we assume that the input smart contracts are syntactically correct as our aim is to verify behavioural properties rather than syntactical ones. If the input contracts are syntactically incorrect then our algorithms will evidently generate incorrect CPN submodels. We do not think that this is a heavy assumption as any Solidity compiler is capable of detecting syntactical errors.

Generation of the Aggregated Transitions

The first step is to create an aggregated transition for each of the contract's functions. To do so, we propose the algorithm generateAggregations. end for 18: end procedure

Preparing the Data Places

getLocalVariables creates a set of places to be used in the sub-model of a transition t a , corresponding to the local variables used in its function. To do so, the statements in the function's body are recursively investigated in search for variable declaration statements. For each variable declaration statement found, a place bearing the name of the variable and its type as its name and colour is created and added to the set P data . In addition to standalone variable declarations, we note that we can also find variables declared in the initialization of a For loop.

We opt for the construction of this set of places beforehand, as opposed to on the fly during the construction of the sub-model, for the following reason. In Solidity, a variable can be used before its declaration (as long as a declaration does exist). Creating its corresponding place on the fly while creating the sub-model of a transition would consequently require testing for its existence every time the variable is used in a statement, as the creation of the place in question may have to happen prior to the declaration statement, in any other statement using it (as part of st LHS or st RHS ) for the first time. On this account, we judge it more efficient to sweep the code first for the construction of P data .

1: procedure getLocalVariables(st; P data )

2:

Input: statement st, set of places P data being created

Creation of the Building Blocks

We see a smart contract function as a set of statements. To each one of the statement types we define a corresponding pattern in CPN, according to which a snippet of a CPN model is generated. The resulting snippets are linked according to the function's internal workflow. The createSubModel implements such correspondences1 . case compound statement {st [1]; st [2] Assignment statement (st LHS , st RHS ): to represent such a statement, a transition t ′ is created with input and output links to, respectively, the input (p in ) and output (p out ) places passed as parameters. t ′ is also connected to the places in P data that correspond to the variables used in the statement's RHS with input/output links (to read the data). In case of a local variable assignment (Figure 4.3), an input/output link is created with the place corresponding to the assigned variable in the statement's LHS with the new value (st RHS ) inscribed on the output link. In case of a state variable assignment (Figure 4.4), the new value (st RHS ) is given in the variable's corresponding placement in the inscription on the link to the output (p out ) place. create arc from t ′ to p out with inscription outInsc ← inInsc in which the variable corresponding to the sender's (respectively the contract's) balance is incremented (respectively decremented) by st RHS 9: end procedure

The Returning Statement Block

Returning statement (-, st RHS ): this is also treated similarly to a global variable assignment statement, but with the following differences. t ′ is linked to t • [cf ] instead of p out with the same inscription of its input link with p in , and has an additional output link with the output return place t • [output] with the return value set to st RHS in its inscription, with the same sender's address and balance from its input inscription. Requirement statement require(c): such a statement is transformed by creating two transitions t revert and t !revert , with !c and c as respective guards, input links with p in and input/output links with the places representing local variables used in c. Transition t revert has •t[cf ] as output place whereas p out is the output place of t !revert . We note that, as a requirement statement is often placed at the beginning of the function, p in and •t[cf ] are usually the same. Selection statement if (c) then st T [else st F ]: the algorithm creates two transitions, t T with guard c and t F with guard !c, that respectively represent the activation of the true and false (or default) branches of the selection statement. Both transition are linked to the input place p in and any places representing local variables used in c. createSubModel is then recursively called for the true-branch statement. In case of a one-branch selection, t F is linked directly to the output place p out . In case of a double-branch selection, a new place p F is created to be the output place of t F and the input place in a recursive call for createSubModel on the false-branch statement. t T .guard ← c end if 24: end procedure 4.3.3.9 The For Loop Statement Block For Looping statement f or(init; c; inc) st T : three places, p init , p c and p T , are created to respectively represent initialization, increments and one pass of the loop's body. Transitions t T with guard c and t F with guard !c are created and linked to the input place p in and any places representing local variables used in c. t T is linked to p c as output to trigger a counter increment while t F is linked to p o ut as output to leave the loop. createSubModel is recursively called with three statements: init which is usually a variable declaration statement with initialization, st T to develop the CPN snippet for one run of the loop, and inc which is usually an assignment to a local variable type of statement. While Looping statement while(c) st T : for this loop the algorithm proceeds by creating one new place p T which will be the output for a new transition t T with guard c.

P in P out •t[cf] [!c] t revert [!c] t revert t !revert [c] t !revert [c] P data [c.v 1 ] P data [c.v
P in P T [!c] t F [!c] t F t T [c]
P in P T [!c] t F [!c] t F t T [c] t T [c] P out P data [c.v
P init P c [!c] t F [!c] t F t T [c] t T [c
Another transition t F is also created with !c as guard and p out as output place. Both transition are linked to the input place p in and any places representing local variables used in c. A recursive call to createSubModel on st T with p T for input and p in for output places is responsible for the generation of the loop's body corresponding CPN snippet. Input: transition t, a while looping statement st = while(c) st T st T , control flow input place p in , control flow output place p out

P data [c.v 1 ] P data [c.v n ] P T [!c] t F [!c] t F t T [c]

3:

Output: sub-model for statement st create arc from p param f to t f with inscription in which every element of f RHS is replaced by its corresponding argument The buildCompoundStatement is first called on the body of the function, creating the places P 1 and P 2 and then recursively calling createSubModel on all the statements it comprises. The algorithm corresponding to the statement's type is invoked each time, adding the necessary places and transitions in conformance to the defined patterns.

P F 2 P 2 T 1 T T T F T T 2 T F 2 T 2 T 3 T 4

Conclusion

In this chapter, we achieved our objective Obj1 mentioned in Section 1.3 which is providing a formal model for Solidity smart contracts. To do so, we have defined a CPN model for a Solidity smart contract by defining a CPN pattern for each statement type of the language. We have automated this transformation by providing a set of transformation algorithms that would generate the corresponding CPN sub-model according to the type of the statement they get as input and its corresponding CPN pattern. These CPN sub-models will be used as building blocks in the rest of our approach.

Chapter 5

Formal Modeling of Behavioural Contexts

Introduction

This chapter represents the second contribution of our work, which consists in the second step towards our end-goal approach (Figure 5.1). With this contribution we aim to achieve Obj2 which is part of the response to RQ2 and RQ4 . We recall that the desired behavior of smart contracts can be intuitively depicted using a business process representation that would describe the context in which the smart contracts are intended to be used. Such a behavioral context may easily originate from a description of a business model. Herein we are interested in the generation of the context's CPN sub-model for such business models. We consider two types of behavioral context specifications for smart contracts:

1. completely-free if no information is provided on the execution context of a contract (Section 5.2)

2. constrained if the context in which a smart contract is used is provided (e.g., as a DCR Graph or a BPMN model)(Section 5.3).

Level-1 Level-3 {f1 si ,..,fi si ,..,fn si , ... f1 sj ,..,fi sj ,..,fn sj }

Completely Free Behavioural Context

In case no behavioural context specification is provided with the smart contracts to be verified, we define a CPN model to represent the execution of these contracts in a completely-free way. In such a model (see Figure 5.2) a place S is used to represent the global state of the blockchain environment shared by all of the smart contracts' functions. For each function f i a place P i is used to represent its input parameters.

The initial marking of a place P i corresponds to all the possible calling arguments for f i . In the following we give the formal definition of CPN4Free, the CPN model that we propose for the representation of a a free context.

Definition 5.2.1 (CPN4Free). Given a set of smart contracts SSC = {SC i , ∀i ∈ [1, n]}, such that n is the number of smart contracts to be verified and

∀SC i ∈ SSC, SC i = (f ji , v hi ), ∀j ∈ [1, n i ], ∀h ∈ [1, m i ]
where n i is the number of functions in SC i and m i is the number of global variables in SC i , we denote by P aram ji = {param k ji , ∀k ∈ [1, n ji ]}, the set of input parameters of the function f ji such that n ji is the number of such parameters. A corresponding CPN model CP N 4F ree = (P, T, A, Σ, V, C, G, E, I) (depicted in figure 5.2) is defined as follows:

• P = {S} ∪ P param , where P param = i∈[1,n] P i , such that ∀i ∈ [1, n], P i = {p ji , ∀j ∈ [1, n i ]} • T = i∈[1,n] T i , such that ∀i ∈ [1, n], T i = {t ji , ∀j ∈ [1, n i ]} • A = {(t i , S), ∀t i ∈ T } ∪ {(S, t i ), ∀t i ∈ T } ∪ {(p ji , t ji ), ∀p ji ∈ P i , ∀t ji ∈ T i , ∀i ∈ [1, n]} • Σ = {C S }∪{C P ji , ∀i ∈ [1, n], ∀j ∈ [1, n i ]},
: v mnn ]× C P 11 × ... × C Pm nn • V = {x, x ′ } ∪ {vp ji , ∀i ∈ [1, n], ∀j ∈ [1, n i ]}, with T ype[x] = T ype[x ′ ] = C S and T ype[vp ji ] = C P ji , ∀i ∈ [1, n], ∀j ∈ [1, n i ] • C = {S → C S } ∪ {p ji → C P ji , ∀p ji ∈ P i , ∀i ∈ [1, n]} • G = ∅ • E = {a → x, ∀a ∈ A ∩ ({S} × T )} ∪ {a → x ′ , ∀a ∈ A ∩ (T × {S})} ∩ E param , where E param = i∈[1,n] {a → p ji , ∀j ∈ [1, n i ]} • I = {p → init p , ∀p ∈ P },
where init p is a predefined initialisation that depends on the type of the place.

Constrained Behavioural Context -A CPN Model for DCR Choreographies

The behavior of smart contracts can be captured either imperatively or declaratively.

Existing BPMN-to-CPN transformations [START_REF] Dechsupa | Transformation of the BPMN design model into a colored petri net using the partitioning approach[END_REF][START_REF] Meghzili | An approach for the transformation and verification of BPMN models to colored petri nets models[END_REF], as well as CPN models could be leveraged for an imperative representation, which is why in the following we will focus on the integration of declarative representations, namely DCR graphs, into our work. The approach that we propose for the verification of smart contracts with a DCR graph/choreography as a behavioral context specification is based on the transformation of the latter into a CPN model that holds the same semantics.

To this end, we start by presenting, in Section 5.3.1 a CPN model for a DCR graph. This model being only adequate for the verification of state-based LTL properties, we propose an extension in Section 5.3.2, that can be seen as a generalization to the first model and that would allow the verification of both state-and event-based LTL properties. Finally, we present in Section 5.3.3 a second extension to our model that consists in a transformation of a DCR choreography by taking into account the concept of roles.

CPN4DCR -Initial Model

In the following we give the formal definition of the initial CPN4DCR model that we propose and showcase its capabilities and limitations for LTL model checking.

Definition 5.3.1 (CPN4DCR). Given a DCR graph G = (E, M, Act, →•, •→, ±, l), a corresponding CPN model CP N 4DCR = (P, T, A, Σ, V, C, G, E, I) (depicted in fig- ure 5.
3) is defined as follows:

• P = {S} • T = {t i , ∀i ∈ [1, n]}, with n = |E| the number of events in G • A = {(t i , S), ∀t i ∈ T } ∪ {(S, t i ), ∀t i ∈ T } • Σ = {C E , (C E × C E × C E )},
where C E is a colour defined as an integer type (C E = range IN T ) where each event e i ∈ E is represented in C E by its index.

• V = {Ex, Re, In, Ex ′ , Re ′ , In ′ }, with T ype[v] = C E , ∀v ∈ V • C = {S → (C E × C E × C E )} • G = {t i → guard i , ∀i ∈ [1, n]}, with n = |E| • E = {a → ⟨Ex, Re, In⟩, ∀a ∈ A ∩ (P × T )} ∪ {a → ⟨Ex ′ , Re ′ , In ′ ⟩, ∀a ∈ A ∩ (T × P )} with ⋆ Ex ′ = Ex ∪ e i , ⋆ Re ′ = (Re\e i ) ∪ e•→ and
⋆ In ′ = (In ∪ e i →+)\e →%

• I = {S → ⟨S 1 , S 2 , S 3 ⟩} with ⟨S 1 , S 2 , S 3 ⟩ the initial marking M of G
For all t i ∈ T representing an event e i in the DCR graph, we further precise that:

• guard i is the conjunction of the conditions defining the enabling of the corresponding event e i :

1. i ∈ In, • the expression ⟨Ex ′ , Re ′ , In ′ ⟩ on its output arc is defined such that:

1. Ex ′ = Ex ∪ i, 2. Re ′ = (Re\i) ∪ i•→ and 3. In ′ = (In ∪ i →+)\i →% ⟨S 1 , S 2 , S 3 ⟩ S t 1 [guard 1 ] t n [guard n ] ⟨Ex, Re, In⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex, Re, In⟩ • • • Figure 5.3: Initial CPN4DCR
The application of this definition on the DCR graph that would be obtained from the DCR graph example in figure 2

= ⟨t i , ..., t j ⟩ of a CPN model C iff ⟨S 1 , S 2 , S 3 ⟩ t 1 [grd 1 ] t 2 [grd 2 ] t 3 [grd 3 ] t 4 [grd 4 ] t 5 [grd 5 ] t 6 [grd 6 ] x 1 x ′ 1 x 2 x ′ 2 x 3 x ′ 3 x 4 x ′
• (M G 1 ≡ M C 1 ∧ M G 1 σ G k --→ M G 2 ∧ M C 1 σ C k --→ M C 2 ) =⇒ M G 2 ≡ M C 2 We note σ G k ≡ σ C k .
Proposition

G k ≡ σ C k , ∀k ∈ [1, m]
with m the length of the longest execution sequence. We start by proving (1):

• Let P (n) be the statement: ∀σ G n = ⟨e 1 , ..., e n ⟩, ∃σ C n = ⟨t 1 , ..., t n ⟩ such that σ G n ≡ σ C n . • P (1) : ∀σ G 1 = ⟨e 1 ⟩, ∃σ C 1 = ⟨t 1 ⟩ such that σ G 1 ≡ σ C 1 .
This can be derived from Definition 5.3.1. In fact, the initial marking of C (M C 0 ) being defined as equivalent to that of G (M G 0 ), and the guard of each transition t i ∈ T being defined as to correspond to the enabling conditions of the relative event e i ∈ E, we can deduce that the set of fireable transitions (M C 0 →) corresponds to the set i are defined as to correspond to the effect of the execution of e i in G.

• Assume that P (k) :

∀σ G k = ⟨e 1 , ..., e k ⟩, ∃σ C k = ⟨t 1 , ..., t k ⟩ such that σ G k ≡ σ C k is true for some k ∈ [2, m -1]
. We will prove that P (k + 1) :

∀σ G k+1 = ⟨e 1 , ..., e k+1 ⟩, ∃σ C k+1 = ⟨t 1 , ..., t k+1 ⟩ such that σ G k+1 ≡ σ C k+1 is true. σ G k+1 ≡ σ C k+1 =⇒ ∃e k+1 ∈ E, t k+1 ∈ T such that σ G k • e k+1 ≡ σ C k • t k+1 (5.1) σ G k ≡ σ C k ⇐⇒ (M G 0 σ G k --→ M G k ∧ M C 0 σ C k --→ M C k ∧ M G k ≡ M C k ) (5.2)
Analogously to the reasoning in the previous point, we can deduce that:

∀e k+1 ∈ E such that M G k e k+1 ---→ M G k+1 , ∃t k+1 ∈ T such that (M C k t k+1 ---→ M C k+1 ∧ M G k+1 ≡ M C k+1 ) (5.3)
And therefore:

∀σ G k+1 = ⟨e 1 , ..., e k+1 ⟩, ∃σ C k+1 = ⟨t 1 , ..., t k+1 ⟩ such that σ G k+1 ≡ σ C k+1 (5.4)
The second part (2) is provable following a similar reasoning.

Discussion

It is evident to see that a DCR graph is a model based on events or tasks, which in our corresponding CPN model we represent by transitions. It is therefore sensible to assume that the users would want to formulate the properties to be verified based on those tasks. Such properties can refer to (i) the execution of an event, which would translate into a property about the firing of its corresponding transition in the CPN model, or to (ii) the possibility of executing an event, which would translate into a property about the fireability of its corresponding transition. The nuance between the two cases might seem subtle, but the difference is rather plain when it comes to their expression in LTL. To explain this, we will refer to the simple example in figure 5. 5.

In fact, it would be easy to express a property on the firing of a transition (e.g., if transition t 1 is fired, transition t 2 will eventually be fired in the future) using eventbased LTL. Such a property would be, in that case, simply expressed as follows: G(t 1 =⇒ Ft 2 ). Expressing the same property using state-based LTL cannot be accomplished in such a straightforward and intuitive way. In general, to express the firing of a transition in state-based LTL we would have to resort to markings. Thus, "a transition t is fired" is expressed by the fact that we reach a marking m ′ that is the immediate successor of a marking m and where the difference between the two markings corresponds to the effects of firing t. More rigorously, t is fired if ∃m ′ s.t m → m ′ with m ∧ X m -pre(t) + post(t). On the other hand, it can be intuitive to express properties on the fireability of a transition (e.g., transition t 2 may be fired in the future) using state-based LTL as follows: G(Fp 1 ). In general, the fireability of a transition is expressed as having the conditions for its firing satisfied and therefore as a property on its input places. Trying to express the same property in event-based LTL would result in a formula on the transitions that need to be fired for the transition in question to be fireable which can be very hard to do in complex models as it is a counter-intuitive reasoning. To be able to express both kinds of properties, we would ideally have a model checker that supports both event-based and state-based LTL formulae. In reality, model checkers only support one kind of LTL properties.

To get around this technical limitation, we propose a second CPN model for DCR graphs that allows to easily and efficiently express event-based properties as statebased ones (without having to resort to markings). Consequently, we allow the users to express both kinds of properties on the events of their DCR graph and support their verification without forcing the users to express them in a counter-intuitive way.

CPN4DCR -Generalization for event-based properties

If we go back to the example in figure 5.5, we note that, if we remove the transition t ′ 1 , we can find a much simpler state-based LTL property to express the event-based one that we had given as example (G(t 1 =⇒ Ft 2 )). In fact, we would not have to resort to expressing a property on the markings of the model, and the following expression: G(p 1 =⇒ Fp 2 ) would be enough to express an equivalent state-based property to the former one. This is mainly due to the fact that by removing the transition t ′ 1 , the place p 1 can only be marked by the firing of t 1 , and therefore having a token in that place forcibly implies that t 1 has been fired. The idea behind our second model is inspired by this particular case, and it consists mainly in introducing a set of additional places P T to the first proposed model, such that we would have one and only one place p T ∈ P T marked when a transition (corresponding to an event in the DCR graph) is fired. We also add a set of fake transitions T F whose role is solely to connect the added places to the main place S of our first model. The definition of our second model can therefore be given as follows: Definition 5.3.4 (CPN4DCR2). Given a DCR graph G = (E, M, Act, →•, •→, ±, l) and its corresponding initial CPN4DCR model CP N 4DCR = (P, T, A, Σ, V, C, G, E, I) as defined in definition 5.3.1, an event-oriented generalization CPN4DCR model 5.6) is defined s.t.: Adding fake transitions and places to our CPN model would indeed increase the size of its state space since we are basically creating intermediate states between the original states from the initial model. This would affect the performance of the model checker that's supposed to take in charge the verification of the model. In order to minimize the number of extra states to be created, we only create fake transitions for the events involved in the property to be verified. For instance, lets consider the following property on the Blind Auction example in figure 2.2: prop DCR : G(¬RevealCall ∨ ¬FBidCall) which basically expresses the fact that no bids can be placed once the revealing window is opened (i.e., the first revealing bids call happened). The application of this definition on this DCR graph with the aim of verifying the property prop DCR is shown in figure 5.7.

G CP N 4DCR = (P ′ , T ′ , A ′ , Σ ′ , V ′ , C ′ , G ′ , E ′ , I ′ ) (depicted in figure
• P ′ = P ∪ P T • P T = {p T i , ∀i ∈ [1, n]}, with n = |E| the number of events in G • T ′ = T ∪ T F • T F = {t F i , ∀i ∈ [1, n]}, with n = |E| the number of events in G • A ′ = {(S, t i ), ∀t i ∈ T } ∪ {(t i , p T i ), ∀t i ∈ T and p T i ∈ P T } ∪ {(p T i , t F i ), ∀p T i ∈ P T and t F i ∈ T F } ∪ {(t F i , S), ∀t F i ∈ T F } • Σ ′ = Σ • V ′ = V ∪ {X}, with T ype[X] = (C E × C E × C E ) • C ′ = C ∪ {p T i → (C E × C E × C E ), ∀p T i ∈ P T } • G ′ = G • E ′ = {a → ⟨Ex, Re, In⟩, ∀a ∈ A ∩ ({S} × T )} ∪ {a → ⟨Ex ′ , Re ′ , In ′ ⟩,∀a ∈ A∩(T ×P T )}∪{a → X, ∀a ∈ A∩(P T ×T F )∪(T F , {S})} with (1) Ex ′ = Ex∪e i , (2)
⟨S 1 , S 2 , S 3 ⟩ S p T 1 p T i p T n t F 1 t F i t F n t 1 [guard 1 ] t i [guard i ] t n [guard n ] ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ X X X X X X • • • • • • Figure 5.6: Generalized CPN4DCR

CPN4DCR -Extension for DCR choreographies

In order to be able to verify properties on DCR choreographies, we need to take into account the concept of roles in our CPN4DCR model. To do so, we mainly add a place R, initially containing the set of ⟨initiator, receivers⟩ in the DCR choreography model, linked to all transitions representing events.

Definition 5.3.5 (CPN4DCR3). Given a DCR choreography (G, R) where G = (E, M, Act, →•, •→, ±, l), the corresponding initial CPN4DCR model for G: CP N 4DCR = (P, T, A, Σ, V, C, G, E, I) as defined in definition 5.3.1, and its generalization G CP N 4DCR = (P ′ , T ′ , A ′ , Σ ′ , V ′ , C ′ , G ′ , E ′ , I ′ ), the extended CPN4DCR model for choreographies E CP N 4DCR = (P ′′ , T ′′ , A ′′ , Σ ′′ , V ′′ , C ′′ , G ′′ , E ′′ , I ′′ ) (depicted in figure 5.8) is defined s.t.:

• P ′′ = P ′ ∪ {R} • T ′′ = T ′ • A ′′ = A ′ ∪ {(R, t i ), ∀t i ∈ T } ∪ {(t i , R), ∀t i ∈ T } • Σ ′′ = Σ ∪ {C R , (C R × P(C R ))}
, where C R is a colour defined as a string type (C R = ST RIN G) to represent roles in DCR we further precise that ∀t i ∈ T representing an event e i in the DCR graph, the expression ⟨V R , V SR ⟩ on the arcs connecting t i to R is defined such that ⟨V R , V SR ⟩ = l(e i ).

• V ′′ = V ′ ∪ {V R , V SR }, with T ype[V R ] = C R and T ype[V SR ] = P(C R ) • C ′′ = C ′ ∪ {R → (C R × P(C R ))} ⟨S 1 , S 2 , S 3 ⟩ S p T 1 p T 2 t F 1 t F 2 t 1 [guard 1 ] t 2 [guard 2 ] t 3 [grd 3 ] t 4 [grd 4 ] t 5 [grd 5 ] t 6 [grd 6 ] ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ X X X X x 6 x ′ 3 x ′ 6 x 3 x 4 x ′ 5 x ′ 4 x 5
• G ′′ = G ′ • E ′′ = E ′ ∪ {a → ⟨V R , V SR ⟩, ∀a ∈ A ′′ ∩ ({R} × T ) ∪ (T × {R})} • I ′′ = I ′ ∪ {R → {r i , ∀i ∈ [1..k]},
The application of this definition on the DCR choreography in figure 2.3 with the same property as in the previous example in Figure 5.7 gives the CPN model shown in figure 5.9.

⟨S 1 , S 2 , S 3 ⟩ S p T 1 p T i p T n R t F 1 t F i t F n t 1 [guard 1 ] t i [guard i ] t n [guard n ] ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ X X X X X X • • • • • • ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ r 1 r 2 r k Figure 5.8: Extended CPN4DCR for choreographies ⟨S 1 , S 2 , S 3 ⟩ S p T 1 p T 2 R t F 1 t F 2 t 1 [guard 1 ] t 2 [guard 2 ] t 3 [grd 3 ] t 4 [grd 4 ] t 5 [grd 5 ] t 6 [grd 6 ] ⟨Ex, Re, In⟩ ⟨Ex, Re, In⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ ⟨Ex ′ , Re ′ , In ′ ⟩ X X X X x 6 x ′ 3 x ′ 6 x 3 x 4 x ′ 5 x ′ 4 x 5 ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ ⟨V R , V SR ⟩ r 1 r 2

Conclusion

In this chapter, we achieved our objective Obj2 mentioned in Section 1.3 which is providing a formal model for possible behavioural contexts that may accompany the smart contracts. To do so, we have mainly considered two types of behavioural contexts. The first is what we called completely free context, and which is used in case of absence of a behavioural context for the smart contracts in question. In other words, if the users have no idea on how they will be using their smart contracts, we will consider this type of context and accordingly build a CPN model (CPN4Free) to represent a free behaviour based only on the elements of the smart contracts to be verified. The second type of context is what we called constrained context, which is used when the users have restrictions on the way they intend to use their smart contracts and can define this behaviour in the form of a DCR graph or choreography. In this case, we define a CPN model (CPN4DCR) that would be built on the elements of the smart contracts according to the provided DCR model. Regardless of the type of context, by the end of this step we have a CPN model that will represent the level-0 model in the final HCPN to be generated as will be further explained in the following chapters.

Introduction

This chapter represents the third contribution of our work, which consists in the third step towards our end-goal approach (Figure 6.1). With this contribution we aim to achieve Obj3 which is part of the response to RQ5 and RQ6 . Herein we are interested in the expression of the properties to be verified on the Solidity smart contracts in question. In our PhD work, we essentially aim to propose an approach 99 that allows the verification of contract-specific properties on smart contracts as it is important to be able to specify the correctness of smart contracts depending on their intended application, especially (but not only) if their behavioural context is known. This does not, however, mean that the detection of vulnerabilities is irrelevant to our work. For this reason, we propose an LTL formalization of six common Solidity vulnerabilities to showcase the capability of our approach to be used to incidentally detect the presence of vulnerabilities in Solidity smart contracts.

Level-1

Level-3 {f1 si ,..,fi si ,..,fn si , ... f1 sj ,..,fi sj ,..,fn sj }

Vulnerabilities Through Examples

A Solidity smart contract may look like a JavaScript or C program syntax-wise, but they are actually dissimilar since the underlying semantics of Solidity is different from traditional programs. This naturally calls on more vigilance from programmers who might be faced by unconventional security issues as vulnerabilities in smart contracts seem to often stem from this gap between the semantics of Solidity and the intentions of the programmer [START_REF] Atzei | A survey of attacks on ethereum smart contracts (sok)[END_REF].

In the following we present two use cases to explain the vulnerabilities treated in this work to provide a better understanding of how we verify them later.

One of the most widespread smart contract applications is delivering gambling services. In fact, thanks to Blockchain's decentralized nature and the transparency of calling this function and eventually draining the contract. This can be illustrated by a call to the function playLotto() with a value of 10 in the MaliciousContract (Listing 6.2) which would start by playing a ticket in the EtherLotto contract by invoking its playTicket() function and then attempting its getPot() function. In the instance where attacker's ticket is a winning one and the contract holds more than twice the amount of the pot in that round, a reentrancy attack can happen. In fact, by sending the jackpot to the winner (line 17 in Listing 6.1), the EtherLotto contract invokes the fallback function of the MaliciousContract, which is an unnamed function used to receive data or Ether. This is where the control flow is handed over to the latter contract whose fallback function recursively calls getPot(), which is allowed since the conditions on its execution are still valid, until the EtherLotto contract's balance is less than the current pot's amount.

Self-Destruction:

The selfdestruct(address) function, when implemented in a contract, removes all bytecode from the contract's address to render it inaccessible and sends all its ether to the specified address. The latter can be another contract's address, in which case, the ether transfer happens forcibly, regardless of the recipient's code (i.e., without invoking its fallback function). Getting back to our second example EtherMilestone, we note the use of this.balance in lines 8 and 16. A player who missed a milestone, could vengefully send an amount of ether using selfdestruct() (e.g., function getRevenge() in MaliciousContract) as to push the contract's balance above the finalMileStone, locking all of the contract's ether and denying the winners who had already reached some milestones their rewards since claimReward() would revert.

Timestamp dependence:

Since the execution on a Blockchain needs to be deterministic for all the miners to get the same results and reach a consensus, users usually resort to block-related variables such as timestamp as a source of entropy. Sharing the same view on the Blockchain, miners would generate the same result, albeit being unpredictable. Even though this seems to be safe, it gives the miners a small room for manipulation given that they can choose a timestamp within a certain range for the new block, which gives them the possibility to tamper with the results and put some bias towards a certain user for example. Such a vulnerability can be exploited by any contract relying on a time constraint to determine its course of action. In our EtherLotto example, the function playTicket() is timestamp-dependent.

Skip Empty Literal:

The source of this vulnerability is the way the encoder of the Solidity compiler treats the arguments in a function call. In fact, when a function call's argument is an empty string literal, it affects the following arguments which are shifted to the right by 32 bytes. This results in a function call with corrupted data.

Uninitialized Storage Variable:

Solidity stores state variables sequentially. So in EtherLotto, the variable bank is stored in slot 0. Since Solidity uses storage for complex data types like structs by default when declared as local variables, they become pointers to storage. Because gr is uninitialized (line 12 in Listing 6.1), it would actually point to the same slot as bank. When setting gr.winner to the first winner's address, this is effectively changing the address stored in bank to the winner's, which results in an unexpected behaviour by this contract. In our example, we present this vulnerability as an error unintentionally introduced by the contract's owner and unintentionally exploited by the first winner. It can, however, be intentionally injected in a contract's code or intentionally exploited by a user, as is the case in the OpenAddressLottery3 honeypot.

Expressing Vulnerabilities in LTL

In the following, M f s i designates the CPN sub-model corresponding to function f in smart contract s i . We note that sometimes we use parameterized propositions to indicate that they are applied to an unspecified aggregated transition. Concretely, such propositions need to be explicitly defined for each transition to be verified4 .

Integer Overflow/Underflow

In our CPN model, we define correspondences between the types used in the Solidity language and those offered by helena so that they cover the same ranges. The model checker is therefore able to detect when the smart contract contains an out-of-range expression. It does not, however, pinpoint the source of the anomaly, so the user does not have much information to go on to track it and try to correct it. To overcome this deficiency, we propose to model integer overflows/underflows as a safety LTL property that can be verified on a specific variable x:

IU O x = □¬xIsOutOf Range
Where xIsOutOfRange is a proposition that evaluates to true if the value of x is not included in the range of its type which we delimit by defining lower and higher thresholds (minThreshold and maxThreshold respectively).

xIsOutOf Range =(x < minT hreshold) ∨ (x > maxT hreshold)

Reentrancy

This vulnerability is related to functions that contain instructions responsible for Ether transfer, and therefore is applied w.r.t a function containing a sending statement. Given such a function, we propose two LTL properties. The first is a safety property defined as follows:

Reentrancy M f s i = □¬reentrant M f s i Where reentrant M f s i
is true if the necessary condition under which a reentrancy vulnerability can be detected in the function f in the smart contract s i is valid. This condition can only be defined when the user indicates the variable x serving as a record for balances and whose assignment should be watched. Such a condition expresses the presence of a sending statement which is not preceded by an assignment to x:

reentrant M f s i = (¬XAssignment)U Sending
Where XAssignment is true when a statement is an assignment to the variable x and Sending is true when a statement is a sending one. A vulnerability is detected when Reentrancy(t f s i ) evaluates to false. This property is used when we only have the code of the smart contract to be verified (i.e., a totally free behaviour). If the code of the interacting contract s j is available, we propose the following LTL property:

Reentrancy M f s i =SendingT o s j → e □((¬SendingT o s j ) U endOf F allback s j )
Using this property we can verify that once the sending statement is executed (SendingTo s j is true), it cannot be executed again until the fallback function of the receiving contract has finished (endOfFallback s j is true) i.e., no reentrancy breach can happen.

Self-destruction

It is checked by detecting the presence of a test containing this.balance in the code of the function:

self Destruction M f s i = ¬testOnBalance M f s i
This detection process can be further enhanced when the code of the interacting smart contract is available. In that case, given a function g in s j that contains a self destruction instruction directing Ether to s i , a function f in s i is considered safe against this vulnerability if it does not contain a test on this.balance or if g cannot be executed prior to f under inspection, which is expressed by the LTL property:

self Destruction M f s i =(¬testOnBalance M f s i ) ∨ (¬self Destruct M g s j U start M f s i )
We note that even though these properties can detect the presence of the self destruction vulnerability, more information on what the function exactly does needs to be provided in order to be able to assess its harmfulness on the execution. This can still be checked by evaluating a contract-specific property.

Timestamp Dependence

In order to check for this vulnerability, we propose an LTL property to detect the accessibility of block.timestamp or its alias now :

T SD M f s i = □¬T imestampDependantStatement
Where TimestampDependantStatement is true if a timestamp is used in a statement. Similarly to the self destruction vulnerability, the presence of timestamp dependence can be detected using the proposed property, but to check the harm it may incur a more appropriate contract-specific property needs to be evaluated.

Skip Empty String Literal

This can be checked for a function f containing function calls by verifying that for any function call with n arguments {a 1 , .., a n } no empty string is passed as an argument (except for the last one a n ). We express this as follows:

SkipEmpty M f s i = □¬F unctionCall
Where FunctionCall is true when the statement is a function call with an empty argument a i (i ̸ = n).

Uninitialized Storage Variable

This is verified for a function f where a variable x of a complex type is defined, by checking the following property:

U nintializedV ariable M f s i = ¬readXUwriteX
Where readX is true when x is read in a statement and writeX is true when it is assigned.

Conclusion

In this chapter, we achieved our objective Obj3 mentioned in Section 1.3 which is the formal definition of well-known vulnerabilities. To do so, we have selected and defined six common Solidity vulnerabilities, namely integer overflow/underflow, reentrancy, self-destruction, timestamp dependence, skip empty literal and uninitialized storage variable. We have then proposed a formalization for these vulnerabilities using Linear Temporal Logic. We recall that our main aim is to allow the verification of LTL properties that reflect characteristics that depend on the smart contracts to be verified. Through the formalization of these vulnerabilities in LTL, we prove that our approach is also capable of detecting the presence vulnerabilities in Solidity smart contracts.

Chapter 7

Application and Implementation of our Approach

Introduction

This chapter represents the fourth contribution of our work, which consists in the last step towards our end-goal approach (Figure 7.1). With this contribution we aim to achieve Obj4 which is part of the response to RQ3 and RQ4 . Herein we are interested in the generation of the final Hierarchical CPN model that will be passed on to the model checker. We will furthermore explain how all of our contributions are linked together to give rise to our full approach, and present our tool Solidity2CPN which automates our approach while offering a user-friendly interface.

Generation of the Final Hierarhical Coloured Petri Net Model

We recall that the end-goal of this PhD work is to implement a full approach for the formal verification of Solidity smart contracts used in a BPM context. Our approach comprises mainly two steps: More precisely, we opt for a hierarchical CPN model to represent the considered smart contracts' execution and interaction with respect to the provided behavioral context specification. As shown in Figure 1.1, we represent each function of a smart contract by an aggregated transition that encapsulates a CPN sub-model corresponding to the internal workflow of the former. These sub-models are initially represented disjointedly. In fact, our aim at this pre-verification phase is to get building blocks for the hierarchical model that will be fed to the model checker. Then, given a behavioral context specification and an LTL property to be verified, the final CPN model is built by (1) linking the aggregated transition representing the targeted function to the behavioral context's model and (2) building a hierarchy by explicitly representing function calls in the sub-model in question (if the checked property requires it). In fact, function calls are initially abstracted and therefore represented by aggregated transitions in the model (e.g., t f j [si] in Figure 1.1) under the assumption that they do not present behavioral problems (deadlock-free and strong-livelock-free) which can be separately verified for each function. Depending on the property to be verified, an aggregated transition may need to be unfolded if any of its corresponding function's instructions or variables are involved in this property, hence the multi-level hierarchy in the model (e.g., t f j [si] in M f i [si] is hidden and replaced by its sub-model M f j [si] ). It is kept folded otherwise (e.g., t f k [si] in M f h [si] ). This abstraction leads to a reduction in the size of the final CPN model, and consequently (in general) a reduction in the size of the state space the model checker needs to explore.

This unfolding mechanism is implemented by the following algorithm.

The unfoldTransition Algorithm hide transition t a and all arcs linked to it 15: end procedure

Application of the Approach

The full application of our end-to-end approach consists in linking the different contributions presented in the previous chapters of this manuscript. Given a set of Solidity smart contracts to be verified, a behavioural context specification that describes the way they are intended to be used, a property that we want to check for, we start by applying our transformation algorithms presented in Chapter 4 on the functions of the smart contracts to generate the different building blocks of the final HCPN model. Then, depending on the type of the provided context specification, we apply the definitions given in Chapter 5 to generate what we call the level-0 CPN model. A hierarchical CPN model is then built upon this initial level-0 CPN model following the unfolding mechanism previously explained in Section 7.2 and using the previously generated building blocks. The hierarchy of this HCPN is derived from the property to be verified, which can be a contract-specific property or a predefined property dedicated to the detection of a vulnerability in the smart contracts as per the for-malizations given in Chapter 6. Once all these steps are carried out, the verification of the targeted property on the contracts would come down to its verification on the final HCPN model by passing the latter to a model checker. For model checking, we chose Helena [START_REF] Evangelista | High level petri nets analysis with helena[END_REF] which is a High LEvel Nets Analyzer available as a command line tool. It offers explicit model checking support for an on-the-fly verification of state and LTL properties over CPN models described in Helena's specification language.

We have automated our approach through a web application that we present in the following section.

The Solidity2CPN Tool for Smart Contracts Verification

We have implemented our approach through a web application1 . The front-end was developed in Javascript with the VueJS framework. As for the back-end, it was developed using the python Django platform. The different modules have been implemented in C++.

Tool Architecture

As shown in figure 7.2, the tool has basically three inputs:

• Solidity Smart contracts: this consists in the .sol file(s) of the Smart contract(s) to be verified.

• Context DCR/CPN: it is a representation of the behavioral context of the provided smart contract(s). It can be either a declarative representation (i.e., a DCR graph/choreography), or an imperative representation (i.e., a CPN model). This input is optional.

• Property to verify: this is the property the user would like to verify on their smart contract(s). This property can either be (i) a Solidity vulnerability, or (ii) a property specific to the smart contract(s).

The tool basically consists of seven modules:

• Solidity2CPN: This is the module responsible for the generation of the CPN sub-models corresponding to the functions of the smart contracts given as input.

• DCR2CPN: This is the module responsible for the generation of the CPN submodel corresponding to the DCR representation of the context (optionally) given as input. • LTL Generation: This is the module responsible for the transformation of the property to be checked, given by the user, and expressed using the elements of the input artifacts (i.e., the contracts and possibly the context), into an LTL property expressed using the elements of the CPN sub-models generated by the other modules, and written according to the Helena model checker specification language.

• HCPN Generation: This is the module responsible for the generation of the final hierarchical CPN model. Initially based on the CPN model of the context, this module unfolds (i.e., replaces an aggregate transition by a CPN sub-model) the transitions concerned by taking into account the LTL property to be checked and using the corresponding CPN sub-models of the smart contracts functions.

• Model Checking: This is the module responsible for invoking the Helena model checker with the final HCPN model and the LTL formula to be checked as inputs.

• Backtracking: This is the module responsible for the interpretation of the result returned by Helena. Indeed, in the case where the model does not satisfy the verified property, Helena returns a counter-example in the form of a sequence of transitions and firings. This sequence should then be transformed into an execution trace expressed on the elements of the smart contracts and the context (if it exists) previously provided as input so that the user can understand, and interpret the verification result and possibly correct his smart contracts accordingly. We note that at the time of writing, this module has not been yet implemented.

Tool Workflow

The tool's workflow can be described by a typical scenario as follows:

• The user begins a verification session by selecting, from his list of smart contracts, the contract(s) concerned by the verification (Fig. 7.3). • The user is then prompted to select a context for his selected contract(s). As was the case for the selection of contracts, the user can either select from his list of contexts or upload a file (.xml in the case of a DCR context, or .lna in the case of a CPN context). Since the context is an optional artifact, the user may as well skip this step (Fig. 7.4). • The user is then invited to select the type of property he would like to verify on his contracts. This property can be:

a property corresponding to a vulnerability. In this case, the tool offers different interfaces to guide the user to provide the necessary information for the selected vulnerability among the following six supported vulnerabilities (Fig. 7.5):

1. integer underflow/overflow 2. reentrency 3. self-destruction 4. timestamp-dependance 5. skip empty string literal 6. unintialiazed storage variable a property specific to the contract(s) to be check (Fig. 7.6). In this case, the tool offers the user two possibilities: * expressing the property using predefined LTL templates for standard and common properties where the user has to only fill predefined fields with contract information (e.g., functions, variables, etc). We note that at the time of writing, this part has not been yet implemented. • The user gives some additional information (e.g., the number of users of his contracts, their balances, etc.) to configure the final verification session (Fig. 7.7).

Conclusion

In this chapter, we achieved our objective Obj4 mentioned in Section 1.3 which is providing a full approach to formally verify smart contracts while supporting the possibility of behavioural context specifications. To do so, we have presented how the generation of the final Hierarchichal CPN model is implemented through the unfolding mechanism for which we have proposed a generic algorithm. The final step that concludes our approach is then too apply model checking on the generated HCPN model w.r.t to the specified LTL property. We have also presented our graphical So-lidity2CPN tool which automates our end-to-end approach and provides user-friendly interfaces to bring our approach closer to as a wide a range of users as possible.

Chapter 8 Being an important pillar for Blockchain technology, smart contracts need to provide certain guarantees in terms of correctness to support its foundation built on trust. Formal approaches for the verification of Solidity smart contracts have been proposed, but they are generally designed to target specific vulnerabilities known in the literature (e.g., reentrancy) which have been reported to be the root of some attacks or malfunctions. Checking the absence of such vulnerabilities in a smart contract does not guarantee its correctness as a faulty behaviour may stem from a flaw specific to that contract. Moreover, the need to verify contract-specific properties has proven increasingly necessary in the light of the expanding reach of smart contracts in many application fields. In fact, the combination of the Blockchain technology and the BPM domain has been an evident step, especially considering the assets that the former brings to the latter. It is still crucial, however, to guarantee the correctness of the smart contracts involved in this association in order to ensure its safety. To the best of our knowledge, there are no studies that focused on the verification of smart contracts in the context of BPM despite the fact that Business processes can be intuitive representations to describe the context in which smart contracts are used.

Conclusion an

Our proposed approach comes as an effort to bring a solution to this research issue of formal verification of Solidity smart contracts in a BPM context by providing a way to formally model contracts along with their behavioural context specification (while also considering the case where no such specification is provided). We do that by both checking for vulnerabilities in the code and offering the possibility to express additional contract-specific properties to check. Moreover, we take into account the context in which the smart contracts to be verified are executed as a behavior specification.

In this manuscript, we presented in details our contributions to tackle the problems specified in Section 1.2. In this concluding chapter, we summarize our work in section 8.1 and present our future research directions Section 8.2. 121

Fulfillment of Objectives

The ultimate goal of this PhD work was to provide a solution that would allow Solidity developers of the BPM community to make sure that their smart-contracts-based applications are correct. This correctness characterization can be in the form of vulnerabilities detection. In fact, the semantics of Solidity can be at times obscure even to domain experts, and many documented attacks on Blockchain platforms prove that seemingly-correct smart contracts can be susceptible to malicious manipulations. The correctness of smart contracts can also be defined as some contract-specific property that is specific to the use case at hand. This is especially important when the designers have some knowledge on the context in which their smart contracts will be used and are able to formulate properties that they would expect their application to satisfy/hold. Our solution, despite being oriented to business process designers, can also be used for the mere objective of verifying smart contracts in general (i.e., without having to provide a behavioural context).

To achieve such a goal, we proposed a model-checking-based approach using Coloured Petri Net as a formalism for the representation of smart contracts and their behavioural contexts and Linear Temporal Logic to express properties on the modeled Blockchain-based application. To do so, we had to divide our problem into a set of challenges and therefore touch on a number of milestones.

The first contribution aimed to provide a formal representation for Solidity smart contracts in the form of Coloured Petri Nets. This choice of formalism emanated from its capability to represent both control-and data-flows of systems which is an important aspect to consider when aiming to verify contract-specific properties. To achieve this aim, we proposed CPN patterns for each type of statement of the Solidity language along with well-defined algorithms that would serve for the automation of the transformation Solidity code into CPN.

The second contribution had as a goal the formalization of the behavioural specifications that may describe the context in which the smart contracts to be verified are to be used. Our approach being oriented towards smart contracts used in the BPM domain, we focused on declarative representations that Business process designers may use to express constraints on their Blockchain-based applications, especially considering the scarcity of studies on formal verification of such models. We singled out DCR graphs and choreographies as our main representation of choice for a constrained context as they are one the modeling techniques that are gaining popularity in the field of BPM, and proposed semantically-equivalent formal CPN models to integrate them in our ultimate solution. To keep our approach as generic as possible, we also proposed a CPN model, dubbed as a free context in our work, that would be used as a context in case none has been provided. This model is built on the elements of the smart contracts to be verified and makes no assumptions on their behaviour, therefore it can be used in our approach as a basis for the general verification of smart contracts.

The third contribution had in view the formalization of vulnerabilities. Having established that the detection of flaws in Solidity smart contracts is not to be neglected as part of checking for their correctness, we selected six of the commonly-present vulnerabilities in Solidity to target in our work. Since our approach is based on the verification of Linear Temporal Logic properties, we represented the selected vulnerabilities in the form of different LTL formulae, the verification of which would enable designers to detect the corresponding vulnerabilities in their code. We note that in our work, the six vulnerabilities that we considered are given as mere examples to prove that the expressiveness of LTL formulae can cover vulnerabilities from the literature even though our focus is on the verification of contract-specific properties.

The last contribution sought to put all the pieces of our approach together to achieve our final goal. This consisted in the generation of the final hierarchical CPN model by 1 generating the different CPN sub-models corresponding to the smart contracts functions as per the first contribution, 2 generating the level-0 CPN model depending on the provided behavioural context specification (or lack thereof) as per the second contribution, 3 the definition of the properties to be verified on the Blockchainbased application as per the third contribution, and 4 using the level-0 CPN model as the initial start and building a hierarchy upon it based on the property to verify and using the previously-generated sub-models. To prove the feasibility of our approach we have developed a fully-fledged tool that provides users with a graphical interface that allows them to specify the property to be verified on the smart contracts, be it contract-specific or corresponding to a common vulnerability, as well as to potentially indicate the behaviour according to which the contracts are used as a BP specification. The transformation of the smart contracts and their behaviours are carried out in the background followed by the model checking phase which is performed by transparently invoking Helena and returning the obtained results. The users, oblivious to the running mechanisms behind the scenes, therefore benefit from a seamless experience that allows them to formally verify their smart contracts without any experience requirements on formal modelling nor model checking.

Future Work

Our work opens several research perspectives to accomplish in short and middle terms. The most immediate perspective is rather technical and concerns our Solidity2CPN tool. Then we intend to investigate the possibility of extending our work by focusing on the integration of the Blockchain technology with other domains, mainly that of the Internet of Things (IoT). Lastly, we will work on improving the performance of our approach by exploring the Helena model checker.

Finishing up the Solidity2CPN tool. As was mentioned in Chapter 7, there are still two parts that we are currently working on implementing for our tool, namely adding the support of template-based LTL properties along with the necessary graphical interfaces for that, and the Backtracking module. For the first part, we need to identify standard and/or common properties that would be interesting to check for our target users and then define them in the form of LTL formulae that could be "configured" or "set up" with elements of the smart contracts in question. We will then design corresponding graphical interfaces to include such properties as templates in our tool. For the second part, we need to implement a module that would transform the counter example returned by Helena (in case of violated property), which is a sequence of states and fired transitions, into a result that the users can easily interpret as an execution trace of their smart contracts.

Supporting IoT as a behavioural context. Just like BPM, the integration of the Blockchain technology with the IoT has been a hot topic recently [START_REF] Dai | Blockchain for internet of things: A survey[END_REF]. We intend to extend our current approach for the verification of Blockchain-based IoT applications by additionally supporting behavioural context specifications provided as an IoT design, in particular as a Node-Red [7] application. To do that, we will transform Node-Red applications that use smart contracts to handle and manipulate data from IoT devices into CPN models, and apply the same strategy presented in our work to verify the correctness of such applications.

Improving Helena To further improve the performance of our approach, we plan to work on Helena's model checker by embedding it with an extension to an existing technique based on symbolic observation graphs (SOG) [START_REF] Klai | MC-SOG: an LTL model checker based on symbolic observation graphs[END_REF] previously developed to deal with the state space explosion problem in regular PNs and adapting it to CPNs.

Figure 1 . 1 :

 11 Figure 1.1: Overview of the approach

Figure 2 . 2 :

 22 Figure 2.2: Blind Auction Workflow -DCR Graph

Figure 2 . 3 :

 23 Figure 2.3: Blind Auction Workflow -DCR choreography

Figure 2 . 5 :

 25 Figure 2.5: Blind Auction -CPN Model

Figure 2 . 6 :

 26 Figure 2.6: Automata-theoretic explicit LTL model checking

Figure 3 . 1 :

 31 Figure 3.1: Smart Contracts verification techniques

Figure 3 .

 3 Figure 3.2 shows the model we proposed and Listing 3.3 the generated Solidity code.We tested this code and confirmed its insusceptibility to reentrancy. Figure3.3 shows the representation using VeriSolid of the property stating that the function Withdraw can only be called after the InitialDeposit function had been called, along with its verification result.

Figure 3 . 3 :

 33 Figure 3.3: Screenshot of the VeriSolid tool -2

  Tested on our example in Listing 3.1, the paper's version of Oyente was able to detect the timestamp dependency and the reentrancy vulnerabilities, as shown in the truncated results in Figure3.4.

Figure 3 . 4 :

 34 Figure 3.4: Screenshot of the Oyente tool

65 4. 1 IntroductionFigure 4 . 1 :

 65141 Figure 4.1: Approach overview -Step 1

1 : 2 : 3 :

 123 procedure generateAggregations(SC) Input: a Solidity smart contract SC Output: the aggregated transitions the CPN model of SC 4: metaColour ← [uint : contractBalance]

1 : 2 : 4 :

 124 procedure createSubModel(t; st; p in ; p out ) Input: transition t, statement st, control flow input place p in , control flow output place p out 3: Output: sub-model of transition t switch st do 5:

Figure 4 . 3 :

 43 Figure 4.3: Local variable assignment

Figure 4 . 7 :

 47 Figure 4.7: Returning Statement Pattern

Figure 4 . 9 :

 49 Figure 4.9: One-branch selection Statement Pattern

1 : 2 : 3 :

 123 procedure buildSelectionStatement(t; st; p in ; p out ) Input: transition t, a selection statement st = if (c) then st T [else st F ], control flow input place p in , control flow output place p out Output: sub-model for statement st 4: create place p T 5: create transition t T 6:

Figure 4 . 12 :

 412 Figure 4.12: While Looping Statement Pattern

1 :

 1 procedure buildWhileLoopStatement(t; st; p in ; p out ) 2:

10 :

 10 create arc from t f to p return f with a placeholder inscription

Figure 4 .

 4 Figure 4.13 represents the resulting sub-model obtained by applying our transformation algorithms (initiated by the createSubModel algorithm) on the function withdraw() of the BlindAuction contract (Listing 2.1 -Lines 31 to 42).

Figure 4 .

 4 Figure 4.13: CPN sub-model of the withdraw() function in the Blind Auction contract

Contents 5 . 1

 51 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.2 Completely Free Behavioural Context . . . . . . . . . . . . . . . 86 5.3 Constrained Behavioural Context -A CPN Model for DCR Choreographies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87 5.3.1 CPN4DCR -Initial Model . . . . . . . . . . . . . . . . . . . . . . . 88 5.3.1.1 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . 91 5.3.2 CPN4DCR -Generalization for event-based properties . . . . . . . 92 5.3.2.1 Optimization of the model . . . . . . . . . . . . . . . . . 93 5.3.3 CPN4DCR -Extension for DCR choreographies . . . . . . . . . . 94 5.4 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 98

Figure 5 . 1 :

 51 Figure 5.1: Approach overview -Step 2

Figure 5 . 2 :

 52 Figure 5.2: CPN model for a completely-free behavioural context

2 .

 2 (→•i ∩ In) ∈ Ex and 3. (→⋄i ∩ In) ∈ E\Re

  .2 is shown in figure 5.4. Definition 5.3.2 (Marking Equivalence). A marking M G = ⟨Ex, Re, In⟩ of a DCR graph G is said to be equivalent to a marking M C = ⟨S → ⟨S 1 , S 2 , S 3 ⟩⟩ of a CPN model C iff • ∀e i ∈ Ex (respectively Re and In), ∃i ∈ S 1 (respectively S 2 and S 3 ), and • ∀i ∈ S 1 (respectively S 2 and S 3 ), ∃e i ∈ Ex (respectively Re and In) We note M G ≡ M C . Definition 5.3.3 (Execution Sequence Equivalence). An execution sequence of length k, σ G k = ⟨e i , ..., e j ⟩ of a DCR graph G is said to be equivalent to an execution sequence of length k, σ C k

6 Figure 5 . 4 :

 654 Figure 5.4: Initial CPN4DCR for the Blind Auction example

  Re ′ = (Re\e i ) ∪ e•→ and (3) In ′ = (In ∪ e i →+)\e →% • I ′ = I 5.3.2.1 Optimization of the model

Figure 5 . 7 :

 57 Figure 5.7: Generalized CPN4DCR of the Blind Auction example

  where each r i being a token representing the initiator ans potential receivers of an event e ∈ E with k = | |E| j=1 l(e j )|.

Figure 5 . 9 :

 59 Figure 5.9: Extended CPN4DCR of the Blind Auction example

Figure 6 . 1 :

 61 Figure 6.1: Approach overview -Step 3

1 .Figure 7 . 1 :

 171 Figure 7.1: Approach overview -Step 4

Figure 7 . 2 :

 72 Figure 7.2: Architecture of the Solidity2CPN tool

Figure 7 . 3 :

 73 Figure 7.3: Smart contracts selection interface

Figure 7 . 4 :

 74 Figure 7.4: Context selection interface

Figure 7 . 5 :

 75 Figure 7.5: Vulnerability selection interface

Figure 7 . 6 :

 76 Figure 7.6: Contract-specific property setting interface (without a template)

Figure 7 . 7 :

 77 Figure 7.7: Configuration interface

Figure 7 . 8 :

 78 Figure 7.8: Generation interface

Figure 7 . 9 :

 79 Figure 7.9: Verification interface

Figure 7 .

 7 Figure 7.10: Results interface

  3.1 Smart contracts verification approaches categorized by the used methods 48 3.2 Vulnerabilities supported by the proposed smart contract verification approaches . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59

	Chapter 1
	General Introduction
	13

Contents 1.1 Research context . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 1.2 Motivation and problem statement . . . . . . . . . . . . . . . . . 19 1.3 Objectives and contributions . . . . . . . . . . . . . . . . . . . . 21 1.4 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 1.5 Thesis outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

Table 3 .

 3 1: Smart contracts verification approaches categorized by the used methods

	Approaches based on Theorem Proving	Approaches based on Model Checking-related techniques Symbolic Execution Abstraction SAT/SMT solvers Model Checking
	[26] [4]	[79] [95] [64]	[97] [31]	[79] [95] [64]	[66, 67]
	[52] [21]	[103] [34]		[103] [34] [57]

  name, the name of the transition t • t.statement, the Solidity code associated with transition t • t.metaColour, the metaColour associated with the control flow places of transition t (if t ∈ T

A ) • t.data, the set of data places associated with transition t (if t ∈ T A ) • t.sub -model, the CPN sub-model associated with transition t (if t ∈ T A ), with t.submodel.inT ransitions designating its input (source) transitions and t.submodel.outT ransitions designating its output (sink) transitions • t.guard, the guard of the transition t 4.2.2 Places P

3 :

 3 Output: updated P data with the set of places corresponding to local variables in the statement st else if st is a compound statement {st[1]; st[2]; . . . ; st[N ]} then

	11:	if st is a double-branching selection statement then
	12:	getLocalVariables(st F , P data )
	13:	end if
	14:	else if st is a looping statement then
	15:	if st is a for statement: f or(init; c; inc)st T then
	16:	getLocalVariables(init, P data )
	17:	getLocalVariables(st T , P data )
	18:	else if st is a while statement: while(c)st T then
	19:	getLocalVariables(st T , P data )
	20:	end if
	21:
	22:	for i = 1..N do
	23:	getLocalVariables(st[i], P data )
	24:	end for
	25:	end if
	26: end procedure
	4:	if st is a variable declaration statement then
	5:	create place p
	6:	p.name ← st LHS .vars.name
	7:	p.colour ← st LHS .type
	8:	add p to P data
	9:	else if st is a selection statement then

  ; . . . ; st[N ]} : procedure buildCompoundStatement(t; st; p in ; p out ) Input: transition t, a compound statement st ={st[1]; st[2]; . . . ; st[N ]}, control flow input place p in , control flow output place p out

	2:
	3:	Output: sub-model for statement st
	4:	for i = 1..N -1 do
	5:	create place p i
	6:	end for
	7:	createSubModel(t;st[1];p in ;p 1 )
	8:	for i = 2..N -1 do
	9:	createSubModel(t;st[i ];p i-1 ;p i )
	10:	end for
	11:	createSubModel(t;st[N ];p N-1 ;p out )
	12: end procedure
	4.3.3.2 The Assignment Statement Block
		P data [st RHS .v 1 ] P data [st RHS .v n ]
			…...
		P data_1	…...	P data_n
				st RHS
		P in	t'	P out
	6:	buildCompoundStatement(t;st;p in ;p out )
	7:	case simple statement
	8:	switch st do
	9:	case assignment statement
	10:	buildAssignmentStatement(t;st;p in ;p out )
	11:	case variable declaration statement
	12:	buildVariableDeclarationStatement(tst;;p in ;p out )
	13:	case sending statement
	14:	buildSendingStatement(t;st;p in ;p out )

1P data [st LHS .v] P data

1 :

 1 procedure buildAssignmentStatement(t; st; p in ; p out ) Input: transition t, an assignment statement st = (st LHS , st RHS ), control flow input place p in , control flow output place p out ′ to p out with inscription outInsc ← inInsc in which the variable corresponding to st LHS .vars is replaced by st RHS LHS , st RHS ): the algorithm creates a transition t ′ with input and output links to, respectively, the input (p in ) and output (p out ) places passed as parameters. Input/output links are created from and to the places corresponding to the variables used in the statement's RHS. An output link is also created to the place representing the declared variable with st RHS as inscription.Input: transition t, a variable declaration statement st = (st LHS , st RHS ), control flow input place p in , control flow output place p out create arc from t ′ to t.data[st LHS .vars] with inscription st RHS9:create arc from t ′ to p out 10: end procedure4.3.3.4 The Sending Statement BlockSending statement (st LHS , st RHS ): the CPN snippet for a sending statement is generated in a way that is similar to that of the case of a global variable assignment, except that instead of updating the assigned variable's counterpart on the output link to p out the algorithm updates the contractBalance and balance values from the input of t ′ by decreasing the first and increasing the second by st RHS .Input: transition t, a sending statement st = (st LHS , st RHS ), control flow input place p in , control flow output place p out

	P data [st RHS .v 1 ] P data [st RHS .v n ] P data_1 P data_n …... …... P data Output: sub-model for statement st connectLocalVariables(st RHS .vars;t;t ′ ) Variable Declaration statement (st 3: 6: 7: connectFunctionCalls(st RHS .f ctCalls;t)
	4: 5: 6:	t' connectLocalVariables(st RHS .vars;t;t ′ ) P in […,st LHS .v,…] create transition t ′ […,st RHS ,...] create arc from p in to t ′	P out
	7:	Figure 4.4: Global variable assignment connectFunctionCalls(st RHS .f ctCalls;t)
	8:
	4:	create transition t ′
	5:
	14: 15: end procedure P data [st RHS .v 1 ] end if	…...	P data [st RHS .v n ]
	4.3.3.3 The Variable Declaration Statement Block P data_1 P data_n …...
		P data
		P in	P data [st RHS .v 1 ] P data [st RHS .v n ] …... t' [contractBalance, …,balance, …] [contractBalance-st RHS , P data [st LHS .v] P out …,balance+st RHS , …]
			Figure 4.6: Sending Statement Pattern
			P data_1	…...	P data_n
			P data	st RHS
	2: 3:	t' Output: sub-model for statement st P in	P out
	3: 4: 5:	Output: sub-model for statement st create transition t ′ Figure 4.5: Variable Declaration Statement Pattern create arc from p in to t ′

create arc from p in to t ′ 6: connectLocalVariables(st RHS .vars\{st LHS .vars};t;t ′ ) 7: connectFunctionCalls(st RHS .f ctCalls;t) 8: if st LHS .vars is a local variable then 9: create arc from t.data[st LHS .vars] to t ′ 10: create arc from t ′ to t.data[st LHS .vars] with inscription st RHS 11: create arc from t ′ to p out 12: else 13: create arc from t 1: procedure buildVariableDeclarationStatement(t; st; p in ; p out ) 2: 1: procedure buildSendingStatement(t; st; p in ; p out ) 2: 8:

  Input: transition t, a returning statement st = (st LHS , st RHS ), control flow input place p in , control flow output place p out create arc from t ′ to t • [output] with inscription outInsc ← [inInsc.sender, inInsc.balance, st RHS ] 10: end procedure 4.3.3.6 The Function Call Statement Block 1: procedure buildFunctionCallStatement(t; st; p in ; p out ) Input: transition t, a function call statement st = (st LHS , st RHS ), control flow input place p in , control flow output place p out

	2:
	3:	Output: sub-model for statement st
	4:	create transition t f
	5:	create place p param f
	6:	create arc from p in to t f
	7:	create arc from p param f to t f
	8:	connectLocalVariables(f RHS .vars;t;t f )
	9:	connectFunctionCalls(f RHS .f ctCalls;t)
	10:	create arc from t f to p out with a placeholder inscription
	11: end procedure
	4.3.3.7 The Requirement Statement Block
	3:	Output: sub-model for statement st
	4:	create transition t ′
	5:	create arc from p in to t ′
	6:	connectLocalVariables(st RHS .vars;t;t ′ )
	7:	connectFunctionCalls(st RHS .f ctCalls;t)
	8:	create arc from t ′ to t • [cf ]
	9:

1: procedure buildReturningStatement(t; st; p in ; p out ) 2:

  Input: transition t, a for looping statement st = f or(init; c; inc) st T , control flow input place p in , control flow output place p out

		P in		P out
		P data [c.v 1 ] P data [c.v 1 ]	…... …...	P data [c.v n ] P data [c.v n ]
		P data_1 P data_1	…... …...	P data_n P data_n
		P data P data	]
				P T
		Figure 4.11: For Looping Statement Pattern
	3:	Output: sub-model for statement st
	4:	create place p init
	5:	create place p c
	6:	create place p T
	7:	createSubModel(t;init;p in ;p init )
	8:	create transition t T
	9:	t T .guard ← c
	10:	create arc from p init to t T
	11:	connectLocalVariables(c.vars;t;t T )
	12:	connectFunctionCalls(c.f ctCalls;t T )
	13:	create arc from t T to p c
	14:	create transition t F
	15:	t F .guard ←!c
	16:	create arc from p init to t F
	17:	connectLocalVariables(c.vars;t;t F )
	18:	connectFunctionCalls(c.f ctCalls;t F )
	19:	create arc from t F to p out
	20:	createSubModel(t;st T ;p c ;p T )
	21:	createSubModel(t;inc;p T ;p init )
	22: end procedure
	4.3.3.10 The While Loop Statement Block

1: procedure buildForLoopStatement(t; st; p in ; p out ) 2:

:

  Input: set of local variables V , transition t, transition t ′

	3:	Output: sub-model with connections to local variables
	4:	for v ∈ V do
	5:	create arc from t.data[v] to t ′
	6:	create arc from t ′ to t.data[v]
	7:	end for
	8: end procedure
	4.3.5 Connecting the Function Calls
	1: procedure connectFunctionCalls(FC; t)
	2:	Input: set of function calls F C, transition t
	3:	Output: sub-model with connections to function calls
	4:	for f ∈ F C do
	5:	create transition t f
	6:	create place p return f
	7:	create place p param f
	8:	connectLocalVariables(f RHS .vars;t;t f )
	4:	create place p T
	5:	create transition t T
	6:	t T .guard ← c
	7:	create arc from p in to t T
	8:	connectLocalVariables(c.vars;t;t T )
	9:	connectFunctionCalls(c.f ctCalls;t T )
	10:	create arc from t T to p T
	11:	create transition t F
	12:	t F .guard ←!c
	13:	create arc from p in to t F
	14:	connectLocalVariables(c.vars;t;t F )
	15:	connectFunctionCalls(c.f ctCalls;t F )
	16:	create arc from t F to p out
	17:	createSubModel(t;st T ;p T ;p in )
	18: end procedure
	4.3.4 Connecting the Data Places

1: procedure connectLocalVariables(V; t; t') 29:

  where C P ji = [type param 1 ] and C S = [uint : contractBalance, type v 11 : v 11 , ..., type vm nn

	param n ji	ji	: param 1 ji , ..., type param	n ji ji	:

ji

  5.3.1. Let G be a DCR graph and C the corresponding CPN model generated as per definition 5.3.1, then G and C are semantically equivalent. Proof. Let G be a DCR graph and C the corresponding CPN model generated as per definition 5.3.1. In order to prove that G and C are semantically equivalent we need to prove that 1. ∀σ G k = ⟨e 1 , ..., e k ⟩, ∃σ C k = ⟨t 1 , ..., t k ⟩, and 2. ∀σ C k = ⟨t 1 , ..., t k ⟩, ∃σ G k = ⟨e 1 , ..., e k ⟩ such that σ

  Contents 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109 7.2 Generation of the Final Hierarhical Coloured Petri Net Model 109 7.3 Application of the Approach . . . . . . . . . . . . . . . . . . . . . 111 7.4 The Solidity2CPN Tool for Smart Contracts Verification . . . 112 7.4.1 Tool Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 7.4.2 Tool Workflow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114 7.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119

  Input: aggregated transition t a , input place p in , output place p out ′ with the placeholder inscription replaced by values from •t ′ [cf ]

	3:
	9:	end for
	10:	end for
	11:
	13:	end for
	14:

1: procedure unfoldTransition(t a ;p in ;p out ) 2: Output: submodel replacement of transition t a 4: for t ′ ∈ t a .submodel.inT ransition do 5: replicate (arc from p in to t a ) to t ′ 6: replicate (arc from •t[input] to t a ) to t ′ 7: for p ∈ •t a [data] ∪ •t a [output] do 8: replicate (arc from p to t a ) to t ′ for t ′ ∈ t a .submodel.outT ransition do 12:

replicate (arc from t a to p out ) to t

  Future Work Contents 8.1 Fulfillment of Objectives . . . . . . . . . . . . . . . . . . . . . . . 122 8.2 Future Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 124

transformer le contexte BPM en un modèle CPN.

construire un modèle CPN en référence à une propriété LTL qui peut exprimer: (i) une vulnérabilité dans le code ou (ii) une propriété spécifique au contrat, en le liant à un modèle CPN représentant le comportement à considérer, et en fournissant le modèle obtenu au vérificateur de modèles pour vérifier la propriété ciblée. 5

We note that in case a place does not exist (p = ∅) then any arc creation involving that place does not take effect.

https://etherscan.io/address/0xa11e4ed59dc94e69612f3111942626ed513cb172

https://gist.github.com/vasa-develop/415a17c709d804a4d351485cd1b7c981

https://etherscan.io/address/0x741f1923974464efd0aa70e77800ba5d9ed18902

Not to be confused with first order predicates

https://depot.lipn.univ-paris13.fr/soliditycpn/soliditycpn

List of Figures

Comparison and Discussion

The majority of the discussed approaches are based on the analysis of the EVM bytecode instead of the higher-level Solidity source code which can be explained by Solidity's lack of formal semantics. In fact, Solidity comes with a well-specified grammar [5] that defines its syntax, but there is no official source for a formal definition of its semantics which is only informally specified through textual description in the Solidity documentation [START_REF]Solidity documentation[END_REF] and directly implemented into its compilers. This has led to recent efforts to provide formal semantics to Solidity as in [START_REF] Jiao | Semantic understanding of smart contracts: Executable operational semantics of solidity[END_REF] that proposes an executable operational semantics for Solidity using the K-framework and [START_REF] Marmsoler | A denotational semantics of solidity in isabelle/hol[END_REF] in which the authors propose an executable denotational semantics for Solidity in the Isabelle/HO theorem prover. In general, relying on the bytecode has its own impediment since it leads to the loss of contextual information, hence limiting the range of properties that can be verified on the contract.

Reported detected vulnerabilities

Limited stack size -

We notice that most of the proposed approaches, led by the first proposition [START_REF] Luu | Making smart contracts smarter[END_REF], use symbolic execution to generate the traces that would be used for the verification. Such approaches usually use under-approximation (e.g., by setting loop bounds) which means that critical violations can be overlooked.

A survey on the vulnerabilities in smart contracts [START_REF] Dingman | Defects and vulnerabilities in smart contracts, a classification using the NIST bugs framework[END_REF] reports 49 bugs that can occur in a smart contract, 29 of which were categorized using the Bugs Framework of NIST into 10 bug classes. As shown in Table 3.2, the proposed verification methods only target a limited number of these bugs, with a maximum of 18 claimed by the end switch 35: end procedure createSubModel browses the body of the transition's corresponding function recursively, statement by statement, and creates snippets of a CPN model according to the type of the processed statement (cf. figures 4.2-4.12) that interconnect to create the transition's sub-model. In the following we give the transformation algorithm for each of the statement types, as well as their corresponding CPN patterns.

The Compound Statement Block

Compound statement {st [1]; st [2]; . . . ; st[N ]}: the algorithm is re-executed on each component statement st[i], after creating N -1 control flow places (of the metaColour colour) to interconnect the resulting CPN snippets while merging the entering point of the snippet of st [1] with the entering point of the snippet of st and the exiting point of st[N ] to that of the snippet of st. transactions within it, players can have a clear view of the behaviour of the game and therefore are led and incentivized to put their trust in the system which is determined by the rules implemented by its smart contracts.

Our first Solidity example (Listing 6.1) is based on a published contract 1 implementing a lottery game. It has been tweaked to illustrate more vulnerabilities without altering its purpose. A player participates in this game by sending an amount of ether equal to the TICKET AMOUNT through playTicket(), which is then added to the game's pot. The winner is determined based on a random value calculated using the block's timestamp and the LottoLog is updated accordingly to keep track of the winners. The winner then gets paid by calling getPot() and the game's host (bank ) can start a new round of lotto using RestartLotto(). This contract may seem fair to inexperienced Solidity developers, but it actually presents multiple vulnerabilities as we will later explain. We consider a second Solidity example 2 (Listing 6.3) to emphasize on the harmful effect the self-destruction vulnerability (see next subsection) can have on a contract. It implements another gambling game whereby a player sends 1 ether to the contract by calling play() in hopes to be the one to hit a milestone. Once the game is over (i.e., the finalMileStone is reached) winners can claim their rewards through claimReward().

Integer Overflow/Underflow:

Due to Solidity's lack of safeguards on mathematical operators, errors such as overflows and underflows may occur as a result of violation of value limitations of integer data types. For instance, the uint8 gameNum variable in the EtherLotto contract can be the source of such a vulnerability when the game exceeds 256 rounds. In fact, at the 257 th round, and due to Solidity's wrapping in two's complement representation for integers, gameNum will be set back to 0, causing data errors/overwriting into the critical LottoLog variable.

Reentrancy:

This is by far the most notorious vulnerability since it led to the infamous DAO attack. An attack of this type can take several forms (e.g, we can talk about a single function reentrancy attack or a cross-function reentrancy attack), but the main idea behind it is that a function can be interrupted in the middle of its execution and then be safely called again before its initial call completes. Once the second call completes, the initial one resumes correct execution. The simplest example is when a smart contract uses a variable to keep track of balances and offers a withdraw function. A vulnerable contract would make a transfer of funds prior to updating the corresponding balance which an attacker can take advantage of by recursively