Blockchain-Based Business Processes:A Solidity-to-CPN Formal Verification Approach

摘要

With its span of applications widening by the day, the technology of Blockchain has been gaining more interest in different domains. It has intrigued many investors, but also numerous malicious users who have put different Blockchain platforms under attack. It is therefore an inescapable necessity to guarantee the correctness of smart contracts as they are the core of Blockchain applications. Existing verification approaches, however, focus on targeting particular vulnerabilities, seldom supporting the verification of domain-specific properties. In this paper, we propose a translation of Solidity smart contracts into CPNs (Coloured Petri nets) and investigate the capability of CPN Tools to verify CTL (Computation Tree Logic) properties.