SmartInv：用于智能合约不变式推断的多模态学习
软件工程
2024-11-15 v1 密码学与安全
编程语言
摘要
智能合约是在区块链上实现各种业务活动的软件程序。最近的研究发现了由交易上下文和源代码共同引起的新一类“机器不可审计”漏洞。现有的检测方法需要人工理解底层交易逻辑，并跨不同上下文来源（即模态）进行手动推理，例如代码、动态交易执行以及指定预期交易行为的自然语言。为了自动化检测“机器不可审计”漏洞，我们提出了 SmartInv，一个准确且快速的智能合约不变式推断框架。我们的核心见解是，由不变式指定的智能合约预期行为依赖于对多模态信息（如源代码和自然语言）的理解和推理。我们提出了一种面向基础模型的新提示策略——思维分层（Tier of Thought, ToT），以跨智能合约的多种模态进行推理，并最终生成不变式。通过检查这些生成的不变式是否被违背，SmartInv 可以识别潜在的漏洞。我们在真实世界的合约上评估了 SmartInv，并重新发现了过去 2.5 年内（从 2021 年 1 月 1 日至 2023 年 5 月 31 日）导致数百万美元损失的漏洞。我们的广泛评估表明，与最先进的工具相比，SmartInv 生成了多 3.5 倍的漏洞关键不变式，检测出多 4 倍的关键漏洞，且耗时显著减少 150 倍。该系统从 89,621 个真实世界合约中发现了 119 个零日漏洞。其中，五个被开发者确认为“高严重性”的关键零日漏洞。
引用
@article{arxiv.2411.09217,
title = {SmartInv: Multimodal Learning for Smart Contract Invariant Inference},
author = {Sally Junsong Wang and Kexin Pei and Junfeng Yang},
journal= {arXiv preprint arXiv:2411.09217},
year = {2024}
}