Towards Secure and Interactive Smart Contract Code from Formal Symboleo Specifications

SYMBOLEO is a specification language used formalize legal contracts, analyze properties, and generate smart contracts for Hyperledger Fabric. However, this ecosystem presents challenges, particularly in securing access to contract elements and enabling interactions with Cyber-Physical Systems (CPS), including IoT devices. This thesis aims to develop and validate a tool for converting extended SYMBOLEO specifications into smart contracts, with a focus on security and privacy. The thesis proposes an architecture to integrate smart contracts, Complex Event Processing (CEP), a message broker, and blockchain (Hyperledger Fabric), facilitating CPS interaction. Additionally, a Role-Based Access Control (RBAC) model is proposed, extending SYMBOLEO with RBAC-inspired concepts, forming SYMBOLEOAC, to regulate access and support dynamic contract execution. Existing code generation tools are also extended to exploit SYMBOLEOAC and this new architecture.