Thesis Defense of Mouhamad Almakhour
Mouhamad Almakhour, a PhD candidate from the CIR team, defended his thesis on October 4, 2023, in the RT Amphitheater at the Vitry-sur-Seine campus of UPEC—120 rue Paul Armangot, 94400 Vitry-sur-Seine.
Title: Reliable Collaboration Platform Based on Distributed Ledgers
Thesis Supervisor(s): MELLOUK Abdelhamid
Abstract:
The emergence of new technologies such as 5G and IoT has led to the creation of new business models that primarily rely on what is known as open or dynamic collaboration as a key concept. In this context, a business process is defined as a group of activities carried out by different actors to achieve business objectives. Today, global market competition and changing conditions make collaboration in business processes between organizations always necessary. This collaboration often involves unknown partners who need to exchange a large amount of data, which presents serious challenges, such as security breaches and unauthorized access, among others.
As a result, companies have started seeking new decentralized, secure, and reliable environments that can implement, verify, and enforce agreements related to collaborative business processes in a transparent manner. Since 2015, a technology called blockchain has transformed the approach to collaboration. Blockchain has successfully addressed many traditional issues by providing a trustworthy, immutable, secure, and decentralized environment. Additionally, it offers self-executing codes known as "smart contracts," where the terms of an agreement between contractual partners are directly encoded.
Consequently, many businesses have begun integrating blockchain into their business processes, leading to the emergence of a new concept called "Collaborative Business Processes Based on Composite Smart Contracts." Composite smart contracts represent one or more smart contracts that must call other contracts belonging to the same or different business process owners to carry out specific tasks. However, new security risks have emerged with applications based on smart contracts. In blockchain, security breaches and vulnerabilities in any contract can result in significant financial loss. Thus, the formal verification of composite smart contracts is essential to ensure the security of collaboration.
To this end, we propose a new approach for verifying the security of Ethereum composite smart contracts in collaborative business process applications. In this work, we introduce a new framework based on formal verification techniques to verify both static and dynamic composite smart contracts, considering general security properties, context-dependent properties, and those relying on external contract calls. Our proposal utilizes finite state machine models, temporal logic formulas, and the model checking method.
To demonstrate the proposed approach, a proof of concept (PoC) with various use cases of composite smart contracts was implemented to test our proposal. First, we began with a standard motivating example, a "Travel Agency System" based on static composite smart contracts. Then, we provided a secure end-to-end platform based on dynamic composite smart contracts for Network Function Virtualization (NFV) to orchestrate and manage the lifecycle of virtual functions. The results obtained validated the effectiveness of our approach, avoiding many issues related to security, privacy, integrity, access control, non-repudiation, and more.