The logic of distributed ledger technology : a formal study

<p dir="ltr">Once considered a technology primarily confined to the fintech realm, Distributed Ledger Technology (DLT) has broadened its applicability, permeating across information technology and engineering disciplines, such as cybersecurity, gaming, and energy management. This uptake is primarily attributed to the continuous exploration of new concepts, resulting in the emergence of distinct classes of DLTs that significantly differ from their initial exemplars, such as Bitcoin. These classes have prompted a substantial shift in the design principles of conventional DLT, leading to an increase in the intricacy of underlying architectures and further complicating the process associated with their analysis and development. Therefore, a meticulous and formal study of DLT becomes imperative, both for leveraging its advancements to their full potential and for adeptly addressing the multifaceted and intricate concerns of various stakeholders. Nevertheless, despite the swift proliferation of DLT literature, the current body of research often maintains a limited purview, leaving a considerable gap in holistic analysis and inadvertently limiting the exploration of interdependencies associated with the inherent challenges within the DLT ecosystem. This gap becomes notably pronounced in pivotal domains, including addressing the pervasive uncertainties surrounding DLT’s applicability, rigorous analysis of DLT architecture and its fundamental components like smart contracts, and ensuring seamless interoperability across heterogeneous DLT systems.<br>Accordingly, the core objective of this thesis is to undertake a comprehensive exploration of the challenges presented within the DLT ecosystem through a systematic study of three key dimensions: (i) applicability, (ii) formal analysis, and (iii) interoperability. First, we conduct an in-depth performance analysis of DLT by implementing an enterprise application on Hyperledger Fabric (HF), a widely adopted DLT software. This investigation entails thorough testing of various operational parameters to assess their impact on the effectiveness and efficiency of HF-based architecture. The primary objective of this study is to gain insights into the scalability and pragmatic aspects, thereby showcasing the applicability of DLT.<br>Second, we incorporate formal methods into the engineering practices of DLT. This study begins by presenting an approach to mitigate potential architectural flaws arising from unreliable component specifications. Specifically, leveraging principles of declarative modeling, widely employed in program verification and refactoring, this thesis introduces Alloy4CMD, a component-based approach for formal modeling and analysis of DLT. The primary objective of this approach is to facilitate the development of verified and reusable modules during the early stages of DLT architectural modeling. Thus, by embracing a correct-by-construction methodology, it aims to enhance the reliability and efficiency of DLT systems. The second part of this formal analysis study presents a multi-formalism approach tailored for DLT components, with a specific focus on smart contracts. This approach aims to address the limitations commonly associated with using a single semi-formal or formal method during various stages of smart contract development, spanning from early architectural sketches to the final implementable code. The main objective of this approach is to provide a systematic and comprehensive analysis using tool-assisted methods, thereby facilitating a holistic assessment of smart contracts.<br>Third, this thesis delves into the critical aspects of interoperability among heterogeneous DLTs. It begins with a formal study of fundamental concepts, including asset swapping and transferring. Additionally, it explores a diverse range of methodologies, strategies, and approaches to obtain a comprehensive understanding of the pivotal role played by interoperability in the broader DLT landscape. Furthermore, this study brings attention to two potential paradoxes associated with the current approach taken by DLT interoperability solutions, shedding light on challenges, such as increased complexity and costs, and a decrease in efficiency. The overarching objective of this multifaceted exploration of DLT interoperability is to address concerns pertaining to the design and development of more decentralized interoperability solutions. We then present an approach to effectively address the interoperability challenges faced by multiple HF networks. This approach aims to extend the conventional role of clients by equipping them with pertinent information regarding the HF network topology. The efficacy of the approach is evaluated using a methodology that considers key factors, such as the number of HF networks, application channels, and clients. Furthermore, the resilience of the approach is assessed against diverse execution failure scenarios associated with chaincode. The primary objective of this study is to leverage existing HF components, thereby avoiding the need for proprietary solutions and minimizing potential complexities, such as integration difficulties, scalability issues, and operational inefficiencies.</p>