Smart contracts are software programs that enable diverse business activities on the blockchain. Recent research has identified new classes of "machine un-auditable" bugs that arise from both transactional contexts and source code. Existing detection methods require human understanding of underlying transaction logic and manual reasoning across different sources of context (i.e. modalities), such as code, dynamic transaction executions, and natural language specifying the expected transaction behavior. To automate the detection of ``machine un-auditable'' bugs, we present SmartInv, an accurate and fast smart contract invariant inference framework. Our key insight is that the expected behavior of smart contracts, as specified by invariants, relies on understanding and reasoning across multimodal information, such as source code and natural language. We propose a new prompting strategy to foundation models, Tier of Thought (ToT), to reason across multiple modalities of smart contracts and ultimately to generate invariants. By checking the violation of these generated invariants, SmartInv can identify potential vulnerabilities. We evaluate SmartInv on real-world contracts and re-discover bugs that resulted in multi-million dollar losses over the past 2.5 years (from January 1, 2021 to May 31, 2023). Our extensive evaluation shows that SmartInv generates (3.5X) more bug-critical invariants and detects (4$\times$) more critical bugs compared to the state-of-the-art tools in significantly (150X) less time. \sys uncovers 119 zero-day vulnerabilities from the 89,621 real-world contracts. Among them, five are critical zero-day bugs confirmed by developers as ``high severity.''

翻译：智能合约是支持区块链上多样化业务活动的软件程序。近期研究发现了由交易上下文和源代码共同引发的新型“机器不可审计”漏洞类别。现有检测方法需要人工理解底层交易逻辑，并跨不同上下文来源（即模态，如代码、动态交易执行过程以及描述预期交易行为的自然语言）进行手动推理。为实现“机器不可审计”漏洞的自动化检测，本文提出SmartInv——一种精准高效的智能合约不变式推断框架。我们的核心洞见在于：由不变式定义的智能合约预期行为，依赖于对源代码与自然语言等多模态信息的理解与跨模态推理。为此，我们提出面向基础模型的新型提示策略——思维分层（Tier of Thought, ToT），以支持跨智能合约多模态信息的推理并最终生成不变式。通过检查这些生成不变式的违反情况，SmartInv能够识别潜在漏洞。我们在真实合约上评估SmartInv，成功复现了过去2.5年（2021年1月1日至2023年5月31日）导致数百万美元损失的安全事件。大量实验表明，相较于最先进工具，SmartInv在显著（150倍）更短的时间内生成多（3.5倍）关键漏洞相关不变式，并检测出多（4倍）关键漏洞。本系统从89,621份真实合约中发现了119个零日漏洞，其中5个被开发者确认为“高危”级别的关键零日漏洞。