论文标题
声明性智能合约的安全验证
Safety Verification of Declarative Smart Contracts
论文作者
论文摘要
如今，智能合约管理大量数字资产。这些合同中的错误导致了重大财务损失。因此，验证智能合约的正确性是一项重要任务。本文提出了一种自动化的安全验证工具DCV，该工具针对以DeCon编写的声明性智能合约为目标，DeCon是一种基于逻辑的域名语言，用于智能合约实施和规范。 DCV通过数学诱导证明了安全性能，并且可以使用启发式模式自动推断归纳不变，而无需开发人员注释。我们对20个基准合同的评估表明，DCV有效验证根据公共存储库改编的智能合约，并且可以验证其他工具不支持的合同。此外，在验证时间内，DCV明显优于基线工具。
Smart contracts manage a large number of digital assets nowadays. Bugs in these contracts have led to significant financial loss. Verifying the correctness of smart contracts is, therefore, an important task. This paper presents an automated safety verification tool, DCV, that targets declarative smart contracts written in DeCon, a logic-based domain-specific language for smart contract implementation and specification. DCV proves safety properties by mathematical induction and can automatically infer inductive invariants using heuristic patterns, without annotations from the developer. Our evaluation on 20 benchmark contracts shows that DCV is effective in verifying smart contracts adapted from public repositories, and can verify contracts not supported by other tools. Furthermore, DCV significantly outperforms baseline tools in verification time.
