From Formal SYMBOLEO Specifications to Secure and Interactive Smart Contract Code

Abstract

Context: Legal contracts have served as the bedrock of business transactions for millennia. They are core to modern supply chains, and their execution can now be automated through the use of i) smart contracts, supported by blockchain technology that safeguards data integrity, and ii) Internet-of-Things technologies to support their monitoring functions. Symboleo is a specification language used to formalize legal contracts, enable property analysis, and generate smart contracts for a permissioned blockchain platform (Hyperledger Fabric). However, automation around resulting smart contracts poses security challenges, particularly regarding who should have access to operate on contract elements. Additionally, how such smart contract should interact with their Cyber-Physical System (CPS) environment, including IoT devices, remains challenging. Purpose: The thesis proposes an architecture to integrate smart contracts, Complex Event Processing (CEP), message brokers, and a blockchain platform (namely Hyperledger Fabric) to support end-to-end Cyber-Physical Smart Contracts (CPSCs). This architecture makes it possible to connect IoT devices with smart contracts (generated using Symboleo) through a CEP engine and a message broker. Additionally, this thesis proposes an access control model, treating all contract elements as resources and ensuring regulated access by designated parties. This model extends the Symboleo ontology and language for legal contracts with new modeling concepts inspired by Role-Based Access Control (RBAC), tailored for the legal contract domain, resulting in SymboleoAC (Symboleo Access Control). SymboleoAC also extends the Symboleo language to handle dynamic contract execution scenario. Methodology: This research follows a Design Science Research methodology, which guides the development and evaluation of the research artifacts. This research is conducted in several iterative steps that are divided into two main phases, one that focuses on theoretical aspects and the other on the design, demonstration, and evaluation of the research artifacts. Contributions: The contributions of this thesis are: • An architectural framework for CPSCs that leverages complementary aspects of CPS and smart contracts; • SymboleoAC, an access control ontology for Symboleo; • An extension of the current Symboleo specification language (syntax and semantics) that supports smart contract requirements, including automation and control actions, access control, and CPS components; • An implementation of the SymboleoAC ontology and semantics into a reusable JavaScript library (SymboleoACJS), together with a tool, SymboleoAC2SC, that generates JavaScript smart contract code with security aspects for a designated platform (Hyperledger Fabric); and • A secure and event-driven SymboleoAC Application Programming Interface (API) that orchestrates the runtime ecosystem connecting IoT sensors, the message broker, the CEP engine, and the blockchain platform. Through extensive and the evaluation of multiple variations of two contract case studies, SymboleoAC (architecture, ontology, and language), along with its associated tools, is shown to be an effective environment for CPSCs, simplifying the design of secure smart contracts and their connections to message brokers, CEP engines, and IoT devices.