Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools.

翻译：部署在以太坊等区块链上的智能合约通常管理着大量资产，因此其安全性至关重要。实证研究表明，现实世界中的攻击往往利用合约业务逻辑中的缺陷，这些缺陷会跨多个交易展开，例如流动性攻击或抢先交易攻击。检测这些攻击需要对超越现有分析工具能力的、具有表达性的时序性质进行推理。在本文中，我们提出了一种自动化智能合约形式化验证方法，支持复杂时序性质的规约与验证。我们的方法提供了一种全自动编码方案，可将Solidity合约的一个具有表达力的子集以及基于一阶Hennessy-Milner逻辑的时序规约编码至Lustre语言——即Kind 2模型检查器所支持的规约语言。该编码使我们能够利用Kind 2判定合约是否满足规约。我们实现了一个集成翻译与验证步骤的工具链，并在涵盖复杂攻击场景的智能合约与时序性质基准上评估了其有效性与性能。结果表明，所提出的方法能够有效验证智能合约的非平凡时序性质，并检测出现有分析工具无法识别的违规行为。