声明式智能合约的安全性验证
软件工程
2023-08-03 v3
摘要
如今智能合约管理着大量数字资产。这些合约中的漏洞已导致重大的财务损失。因此，验证智能合约的正确性是一项重要任务。本文提出一款自动化安全验证工具 DCV，其面向以 DeCon 编写的声明式智能合约，DeCon 是一种基于逻辑、用于智能合约实现与规约的领域特定语言。DCV 通过数学归纳法证明安全性质，并能够利用启发式模式自动推断归纳不变量，无需开发者标注。我们在 20 个基准合约上的评估表明，DCV 能有效验证改编自公共仓库的智能合约，并可验证其他工具不支持的合约。此外，DCV 在验证时间上显著优于基线工具。
引用
@article{arxiv.2211.14585,
title = {Safety Verification of Declarative Smart Contracts},
author = {Haoxian Chen and Lan Lu and Brendan Massey and Yuepeng Wang and Boon Thau Loo},
journal= {arXiv preprint arXiv:2211.14585},
year = {2023}
}