基于形式化方法构建智能合约的可执行安全设计模型

智能合约颇具吸引力，因为它们是各方之间具有预定义且不可变义务与权利的自我执行商业协议。然而，与所有软件一样，智能合约可能因设计缺陷而存在漏洞，从而被某一方利用以欺诈他人。本文展示一种利用形式化方法构建智能合约安全设计模型的系统化方法。为构建安全模型，我们首先将参与方的行为建模为状态机，然后建模合约的预定义义务与权利，其规定了为实现商业目标而在状态机之间的交互。此后，我们在 TLA+（Temporal Logic of Actions，动作时序逻辑）中给出可执行安全模型设计模式，以在设计层面针对已知智能合约漏洞（涉及状态机及义务与权利）进行防护。这些漏洞发现于以太坊合约中，包括调用未知（Call to the unknown）、无 gas 发送（Gasless send）、重入（Reentrancy）、转账丢失（Lost in the transfer）与不可预测状态（Unpredictable state）。所得 TLA+ 规约称为安全模型。我们以房地产合约为例，说明在设计层面检测这些漏洞的方法。