Smart contract life-cycle management: an engineering framework for the generation of robust and verifiable smart contracts

The concept of smart contracts (SCs) is becoming more prevalent, and their application is gaining traction across many diverse scenarios. However, producing poorly constructed contracts carries significant risks, including the potential for substantial financial loss, a lack of trust in the technology, and the risk of exposure to cyber-attacks. Several tools exist to assist in developing SCs, but their limited functionality increases development complexity. Expert knowledge is required to ensure contract reliability, resilience, and scalability. To overcome these risks and challenges, tools and services based on modeling and formal techniques are required that offer a robust methodology for SC verification and life-cycle management. This study proposes an engineering framework for the generation of a robust and verifiable smart contract (GRV-SC) framework that covers the entire SC life-cycle from design to deployment stages. It adopts SC modeling and automated formal verification methodologies to detect security vulnerabilities and improve resilience, extensibility, and code optimization to mitigate risks associated with SC development. Initially, the framework includes the implementation of a formal approach, using colored Petri nets (CPNs), to model cross-platform Digital Asset Modeling Language (DAML) SCs. It also incorporates a specialized type safety dynamic verifier, which is designed to detect and address new vulnerabilities that can arise in DAML contracts, such as access control and insecure direct object reference (Idor) vulnerabilities. The proposed GRV-SC framework provides a holistic approach to SC life-cycle management and aims to enhance the security, reliability, and adoption of SCs.