KindHML：基于Hennessy-Milner逻辑的智能合约形式化验证
密码学与安全
2026-04-16 v1 计算机科学中的逻辑
摘要
部署在以太坊等区块链上的智能合约通常管理着大量资产，因此其安全性至关重要。实证研究表明，现实世界中的攻击常常利用跨多个交易展开的合约业务逻辑中的缺陷，例如流动性攻击或抢先交易攻击。检测这些攻击需要对表达性的时序性质进行推理，这超出了现有分析工具的能力范围。在本文中，我们提出了一种智能合约形式化验证的自动化方法，能够对复杂的时序性质进行规约和验证。我们的方法提供了一种全自动的编码方式，将基于一阶Hennessy-Milner逻辑的Solidity合约的一个表达性子集及时序规约编码为Lustre——即Kind 2模型检查器支持的规约语言。这种编码使我们能够利用Kind 2来确定合约是否满足规约。我们在一个集成了翻译和验证步骤的工具链中实现了我们的方法，并在一个包含智能合约和捕获复杂攻击场景的时序性质的基准测试上评估了其有效性和性能。我们的结果表明，所提出的方法能够有效验证智能合约的非平凡时序性质，并检测出现有分析工具无法触及的违规行为。
引用
@article{arxiv.2604.14038,
title = {KindHML: formal verification of smart contracts based on Hennessy-Milner logic},
author = {Massimo Bartoletti and Angelo Ferrando and Enrico Lipparini and Vadim Malvone},
journal= {arXiv preprint arXiv:2604.14038},
year = {2026}
}