Formal Requirement Enforcement on Smart Contracts Based on Linear Dynamic Logic

Recently, despite the growing popularity of smart contracts, one serious concern is arising among both industry and academia, that is, whether they work autonomously without human intervention really as intended and, when we are not sure, how we can ensure that contracts meet particular requirements. To resolve this, we propose a new formal approach to smart contract development: Instead of defining contracts just as programs in conventional languages, they should be defined using formal logic so that we can verify whether they meet particular requirements and enforce them if necessary. The primary challenge is that expressive formal logic often turns out to be undecidable and consequently executable programs cannot be generated. As a solution, each contract definition is divided into two layers, namely specification layer in a decidable logic called Linear Dynamic Logic for verification and enforcement of requirements and rule layer for defining implementation details, while the consistency between the two layers is systematically guaranteed. Based on this, it also becomes possible to automatically generate executable contract programs from their formal specification, which leads to improving the trustworthiness of contracts. Evaluation on Hyperledger Fabric shows the feasibility and high effectiveness of our approach.