10 篇博文 含有标签「blockchain security」

2026 年初，当一个自主 AI 交易代理从 DeFi 协议中抽走 4500 万美元时，这次攻击并未利用任何一行智能合约代码。相反，攻击者污染了 AI 代理盲目信任的预言机数据源，将代理自身的速度和自主性转化为对抗其本应保护的协议的武器。欢迎来到这个加密领域最危险的漏洞不再存在于代码中，而是在于 AI 的时代。

Google Quantum AI 刚刚投下了一枚重磅炸弹：未来的量子计算机可以在大约 9 分钟内破解比特币私钥 —— 恰好在 10 分钟的区块确认窗口内。这份长达 57 页的论文由 Google 与以太坊基金会以及斯坦福大学的研究人员共同撰写，在加密市场引发了剧烈震荡。短短几天内，抗量子代币的涨幅高达 51%，而比特币和以太坊的投资者则面临着一个令人不安的问题：保护数万亿美元数字资产的加密技术是否已经时日无多？

GitHub 历史上增长最快的仓库刚刚暴露了分布在 82 个国家的超过 135,000 个脆弱的 AI 智能体——而加密货币用户是主要目标。欢迎来到 OpenClaw 安全危机。在这里，争相部署 AI 网关的中国科技巨头与一场大规模的供应链攻击正面碰撞，这场攻击正在改写区块链安全的规则。

成为安全噩梦的病毒式现象​

在 2026 年 1 月下旬，OpenClaw 实现了前所未有的成就：它在 单日内获得了超过 20,000 个 GitHub 星标，成为该平台历史上增长最快的开源项目。到 2026 年 3 月，这款 AI 助手已经积累了超过 250,000 个星标，全球科技爱好者纷纷争相安装这款看似代表个人 AI 未来的工具。

与基于云的 AI 助手不同，OpenClaw 完全在你的计算机上运行，拥有访问你的文件、电子邮件和应用程序的完整权限。你可以通过 WhatsApp、Telegram 或 Discord 向它发送消息，它会 24/7 全天候运行——执行 Shell 命令、浏览网页、发送电子邮件、管理日历，并跨越你的数字生活采取行动——所有这些都只需通过手机发送一条简单的消息即可触发。

这个卖点令人无法抗拒：你自己的个人 AI 智能体，在本地运行，随时待命，功能无限。但事实证明，现实要危险得多。

135,000 个暴露实例：安全灾难的规模​

到 2026 年 2 月，安全研究人员发现了一个令人心惊的事实：全球 82 个国家有超过 135,000 个 OpenClaw 实例暴露在公网上，其中超过 50,000 个容易受到远程代码执行攻击。原因何在？OpenClaw 默认配置中存在一个根本性的安全漏洞。

OpenClaw 默认绑定到 0.0.0.0:18789，这意味着它监听 包括公网在内的所有网络接口，而不是按照安全最佳实践要求仅监听 127.0.0.1（仅限本地主机）。从背景来看，这相当于敞开大门并挂上“请随意进入”的牌子——只不过这扇门通向的是你的整个数字生活。

“ClawJacked”漏洞使情况变得更糟。攻击者只需诱导你访问一个恶意网站，就能劫持你的 AI 助手。一旦被攻破，攻击者将获得与 AI 智能体本身同等级别的访问权限：你的文件、凭据、浏览器数据，以及没错——你的加密货币钱包。

安全公司竞相了解其影响范围。卡巴斯基（Kaspersky）、Bitsight 和 Oasis Security 都发布了紧急警告。共识非常明确：OpenClaw 代表了一场“安全噩梦”，涉及关键的远程代码执行漏洞、架构缺陷，以及——最令人震惊的——其插件市场中大规模的供应链投毒活动。

ClawHavoc：针对加密货币用户的供应链攻击​

在研究人员关注 OpenClaw 核心漏洞的同时，一个更隐蔽的威胁正在 ClawHub 中展开——这是一个旨在让用户轻松查找并安装 AI 智能体第三方“技能”（插件）的市场。

2026 年 2 月，代号为 ClawHavoc 的安全研究发现，在 ClawHub 审计的 2,857 个技能中，有 341 个是恶意的。到 2 月中旬，随着市场规模增长到 10,700 多个技能，恶意技能的数量增加了一倍多，达到 824 个——根据某些报告，恶意技能的数量甚至高达 1,184 个。

攻击机制极其巧妙：

1. 虚假前提条件：335 个技能利用虚假的安装要求欺骗用户下载 Atomic macOS Stealer (AMOS) 木马。
2. 针对特定平台的有效载荷：在 Windows 上，用户从被攻破的 GitHub 仓库下载 “openclaw-agent.zip”；在 macOS 上，托管在 glot.io 的安装脚本被直接复制到终端（Terminal）中。
3. 复杂的社会工程学：文档说服用户在合法设置步骤的掩护下执行恶意命令。
4. 统一的基础设施：所有恶意技能共享相同的指令与控制（C2）基础设施，表明这是一场协同作战。

主要目标是谁？加密货币用户。

该恶意软件旨在窃取：

• 交易所 API 密钥
• 钱包私钥
• SSH 凭据
• 浏览器密码
• 来自 Solana 钱包和钱包追踪器的加密货币特定数据

在这些恶意技能中，有 111 个是明确针对加密货币的工具，包括 Solana 钱包集成和加密货币追踪器。攻击者明白，习惯于安装浏览器扩展和钱包工具的加密货币用户，将是 AI 智能体供应链攻击中最具价值的目标。

中国科技巨头的部署竞赛​

就在安全研究人员发布警告时，中国科技巨头们看到了机遇。2026 年 3 月初，腾讯、阿里巴巴、字节跳动、京东和百度 都推出了竞争性的 免费 OpenClaw 安装活动，将通常需要数月的竞争博弈压缩到了短短几天内。

策略很明确：利用免费部署作为获客手段，在商业 AI 项目规模化之前锁定用户。每家巨头都在争夺成为“下一代 AI 开发者的首个基础设施触点”：

• 腾讯 推出了 QClaw，将 OpenClaw 与微信集成，以便用户可以通过手机发送指令远程控制笔记本电脑。
• 阿里云 在其平台上推出了对 OpenClaw 的支持，并连接到其通义千问（Qwen）AI 模型系列。
• 字节跳动的火山引擎（Volcano Engine） 发布了 ArkClaw，这是 OpenClaw 的一个“开箱即用”版本。

讽刺意味十分浓厚：正当安全研究人员警告 135,000 个暴露实例和大规模供应链攻击时，中国最大的科技公司却在积极向数百万用户推广大规模安装。技术热忱与安全现实之间的碰撞从未如此显眼。

Web3 的 AI 代理问题：当 MCP 遇上加密钱包​

OpenClaw 危机暴露了一个 Web3 构建者再也无法忽视的深层问题：AI 代理正越来越多地管理链上资产，而其安全模型却极其不成熟。

模型上下文协议（MCP）——连接 AI 代理与外部系统的新兴标准——正在成为 AI 与区块链交互的门户。MCP 服务器充当整个 Web3 栈的统一 API 网关，使 AI 代理能够读取区块链数据、准备交易并执行链上操作。

目前，大多数加密货币 MCP 服务器需要配置 私钥，这造成了单点故障。如果 AI 代理受到损害——正如成千上万个 OpenClaw 实例那样——攻击者就能直接获取资金。

两种竞争性的安全模型正在浮现：

1. 委托签名（用户控制）​

AI 代理准备交易，但用户保留对签名的唯一控制权。私钥 从未离开用户的设备。这是最安全的方法，但限制了代理的自主性。

2. 代理控制的额度​

代理拥有自己的密钥，并获得代表用户消费的额度。私钥由代理主机安全管理，且支出设有上限。这实现了自主运行，但需要信任主机的安全性。

这两种模型目前都尚未被广泛采用。大多数加密 MCP 实现仍在使用危险的“给代理私钥”的方法——这正是 ClawHavoc 攻击者所期待的场景。

根据 2026 年的预测，60% 的加密钱包将使用代理式 AI 来管理投资组合、跟踪交易并提高安全性。业界正在实施多方计算（MPC）、账户抽象、生物识别身份验证和加密本地存储来保护这些交互。诸如 ERC-8004（由以太坊基金会、MetaMask 和 Google 共同主导）等标准正试图为链上 AI 代理创建可验证的身份和信用历史。

但 OpenClaw 证明了这些保护措施尚未到位——而攻击者已经开始利用这一空白。

NVIDIA 的企业级方案：GTC 2026 上的 NemoClaw​

随着 OpenClaw 安全危机的发酵，NVIDIA 看到了一次契机。在 3 月中旬的 GTC 2026 上，该公司宣布了 NemoClaw，这是一个专为 企业自动化 设计的开源 AI 代理平台，从底层构建了安全和隐私机制。

与 OpenClaw 优先考虑消费者、随处安装的方法不同，NemoClaw 针对企业的特点包括：

• 内置安全与隐私工具，解决了困扰 OpenClaw 的漏洞
• 企业级身份验证与访问控制，防止了“默认对互联网开放”的配置灾难
• 多平台支持，不仅能在 NVIDIA 芯片上运行，还利用了该公司的 NeMo、Nemotron 和 Cosmos AI 框架
• 合作伙伴生态系统，包括与 Salesforce、Google、Cisco、Adobe 和 CrowdStrike 的洽谈

这个时机极具战略意义。当 OpenClaw 的“龙虾热”（Lobster Fever）暴露了以消费者为中心的 AI 代理的危险时，NVIDIA 将 NemoClaw 定位为安全的、企业级的替代方案——这可能会在企业 AI 代理市场挑战 OpenAI。

对于构建 AI 集成基础设施的 Web3 公司而言，NemoClaw 代表了解决 OpenClaw 所暴露安全问题的一个潜在方案：专业管理、经过审计且安全的 AI 代理部署，可以安全地与高价值区块链资产进行交互。

Web3 迫切需要的警钟​

OpenClaw 危机不仅是一个 AI 安全故事，它还是一个 区块链基础设施故事。

考虑以下影响：

• 135,000+ 个暴露的 AI 代理 可能访问加密钱包
• 1,184 个恶意插件 专门针对加密货币用户
• 五家中国科技巨头 在没有足够安全审查的情况下推动了数百万次安装
• 预计到年底 60% 的加密钱包 将使用 AI 代理
• 尚未有广泛采用的安全标准 用于 AI 与区块链的交互

这是 Web3 的“供应链安全时刻”——堪比传统金融中的 2020 年 SolarWinds 攻击或加密领域 2016 年的 DAO 黑客事件。它揭示了一个基本事实：随着区块链基础设施变得更加强大和自动化，攻击面也随之呈指数级扩大。

行业的反应将决定 AI 代理是成为 Web3 功能的安全门户，还是该领域见过的最大漏洞。在委托签名模型、代理额度、MPC 方案和账户抽象之间的选择不仅是技术性的——更是关乎生存的。

Web3 构建者现在应该做什么​

如果你正在 Web3 中构建并集成 AI 代理（或计划这样做），这里有一份清单：

1. 审计你的 MCP 服务器安全性：如果你要求私钥来访问 AI 代理，你就在制造类似 ClawHavoc 的攻击向量
2. 实施委托签名：即使用户使用 AI 准备交易，用户也应始终保留对交易签名的唯一控制权
3. 对自主代理使用基于额度的模型：如果代理需要独立行动，请为它们分配具有严格支出限制的专用密钥
4. 切勿使用默认网络配置安装 AI 代理：除非你有企业级身份验证，否则始终绑定到本地主机（127.0.0.1）
5. 像对待应用商店一样对待 AI 代理市场：在信任第三方技能之前，要求代码签名、安全审计和声誉系统
6. 教育用户了解 AI 代理风险：大多数加密用户并不明白，使用 AI 代理在功能上等同于给某人提供了其计算机的 root 访问权限

OpenClaw 危机教给我们：默认安全比功能更重要。部署 AI 代理的竞赛不能超过保护其安全的竞赛。

正在构建连接到 AI 代理的区块链基础设施？BlockEden.xyz 为 40 多个区块链提供企业级 API 基础设施，其安全优先的架构专为高风险集成而设计。探索我们的服务，在经得起考验的基础上进行构建。

数据来源：

• Meet OpenClaw: The AI assistant that broke every record – and started a security panic
• OpenClaw: GitHub's Fastest-Ever Rising Star Becomes 2026's First Major AI Security Disaster
• New OpenClaw AI agent found unsafe for use | Kaspersky official blog
• OpenClaw Security: Risks of Exposed AI Agents Explained | Bitsight
• ClawJacked: OpenClaw Vulnerability Enables Full Agent Takeover
• Researchers Find 341 Malicious ClawHub Skills Stealing Data from OpenClaw Users
• Malicious OpenClaw Skills Used to Distribute Atomic MacOS Stealer | Trend Micro
• ClawHavoc Poisons OpenClaw's ClawHub With 1,184 Malicious Skills
• Using MCP with Web3: How to secure blockchain-interacting agents | Google Cloud Blog
• How to Build AI-Powered Web3 Crypto Wallets in 2026
• Model Context Protocol (MCP): Bridging AI and Blockchain for Smarter Crypto Projects
• Chinese Tech Giants Race to Adopt OpenClaw AI Gateway
• China's AI Red Packet War: ByteDance, Tencent, Alibaba and Baidu Battle to Become the Default Gateway
• Nvidia targets enterprise AI agents with new open-source NemoClaw platform
• Nvidia Prepares NemoClaw to Power Enterprise AI Agents
• NVIDIA to Launch Open-Source AI Agent "NemoClaw" at GTC 2026: What We Know So Far

仅需 1.22 美元——比一杯咖啡的价格还低——AI 代理现在就可以扫描智能合约，识别其漏洞并生成可用的漏洞利用程序（exploit）。这并非安全白皮书中虚构的理论情景。这是 SCONE-bench 的实测结果，它是首个评估 AI 代理利用真实智能合约能力的基准测试，由 Anthropic 和 MATS Fellows 研究人员于 2025 年底发布。在 2020 年至 2025 年间实际遭到攻击的 405 个合约中，10 个前沿 AI 模型共同为其中的 207 个生成了交钥匙式（turnkey）的漏洞利用，产生的模拟被盗资金总额达 5.501 亿美元。

其影响远远超出了研究实验室。DeFi 协议的总锁仓量（TVL）合计超过 1000 亿美元。如果漏洞利用能力每 1.3 个月翻一番——正如 Anthropic 的数据显示的那样——支撑链上金融的安全假设正在接近拐点。

只需每个合约 1.22 美元，AI 代理现在就可以扫描智能合约中的可利用漏洞——且攻击性的漏洞利用能力每 1.3 个月就会翻倍。欢迎来到去中心化金融中最具影响力的军备竞赛。

2026 年 2 月，OpenAI 和 Paradigm 联合推出了 EVMbench，这是一个开源基准测试，用于评估 AI 代理在检测、修复和利用智能合约漏洞方面的有效性。结果令人警醒。GPT-5.3-Codex 成功利用了 72.2% 的已知漏洞合约，而六个月前这一比例仅为 31.9%。同时，一个专用的 AI 安全代理在 90 个被利用的 DeFi 合约（总价值 9680 万美元）中检测到了 92% 的漏洞——几乎是基准 GPT-5.1 编码代理 34% 检测率的三倍。

其中的含义显而易见：DeFi 安全的战斗已演变为一场 AI 对阵 AI 的竞赛，而且就目前而言，经济效益压倒性地倾向于攻击者。

攻击者存入 8 USDC 作为抵押品，然后带走了 187 ETH —— 价值大约 $390,000。智能合约完全按照设计运行。预言机也履行了职责。但有人将 BTC / USD Chainlink 价格馈送插入了本应属于 USDC 的插槽中。这一行配置将一个运行良好的借贷协议变成了“提款机”。

欢迎来到 DeFi 安全的新前线，在这里，最致命的漏洞并非隐藏在 Solidity 字节码中 —— 而是存在于管理员仪表板、部署脚本和参数文件中。

2025 年，尽管大多数受攻击的协议都经过了审计，甚至有些还审计了多次，DeFi 仍因智能合约漏洞损失了 33 亿美元。2 月份发生的 15 亿美元 Bybit 攻击、4200 万美元的 GMX 漏洞以及无数次重入攻击，证明了一个令人不安的事实：传统的安全审计是必要的，但并不充分。当数学精度至关重要时，仅仅测试极端情况是不够的。你需要证明它们。

这就是 Sui Prover 开源的意义，它远比仅仅在 GitHub 上发布一个项目更重要。Sui Prover 由 Asymptotic 开发，现在免费提供给 Sui 开发者社区。它将形式化验证（Formal Verification）引入到日常的智能合约开发中。这种数学技术同样被用于确保飞行控制系统和处理器设计不会失效。在这样一个哪怕一个被忽视的边缘情况都可能导致数亿美元损失的背景下，通过数学方式证明代码行为正确已不再是一种奢侈，而正成为一种必需。

2025 年 2 月 21 日，朝鲜黑客在大约 30 分钟内从总部位于迪拜的交易所 Bybit 窃取了 15 亿美元的加密货币。这不仅是历史上最大的加密货币劫案——如果 Bybit 是一家银行，它将被吉尼斯世界纪录列为有史以来最大的银行抢劫案。

此次攻击并非利用了智能合约漏洞或暴力破解私钥。相反，黑客入侵了一家第三方钱包供应商的一名开发人员的笔记本电脑，耐心等待了数周，并在 Bybit 员工批准看起来像是常规内部转账的操作时果断出击。当人们意识到出现问题时，500,000 ETH 已经消失在由朝鲜 Lazarus Group 控制的迷宫般的钱包中。

这是关于它是如何发生、为什么重要，以及它揭示了 2025 年加密货币安全状况的故事。

攻击过程：一场耐心与精准的杰作​

Bybit 黑客攻击并不是一次简单的抢劫，而是一场持续数周的精密手术式行动。

第一阶段：入侵开发人员​

2025 年 2 月 4 日，Safe{Wallet}（Bybit 用来保护大额转账的广泛使用的多签名钱包平台）的一名开发人员下载了一个看似合法的名为 “MC-Based-Stock-Invest-Simulator-main” 的 Docker 项目。该文件很可能是通过社交工程攻击发送的，可能伪装成工作机会或投资工具。

恶意的 Docker 容器立即建立了与攻击者控制的服务器的连接。随后，黑客从开发人员的工作站中提取了 AWS 会话令牌——这些是授予 Safe{Wallet} 云基础设施访问权限的临时凭据。

凭借这些令牌，攻击者完全绕过了多因素身份验证。他们现在掌握了通往 Safe{Wallet} 王国的钥匙。

第二阶段：潜伏的代码​

攻击者并未立即采取行动，而是在 Safe{Wallet} 的 Web 界面中注入了隐蔽的 JavaScript 代码。这段代码是专门为 Bybit 设计的——它会一直处于潜伏状态，直到检测到 Bybit 员工打开了他们的 Safe 账户并准备授权一笔交易。

这种复杂程度令人惊叹。对于其他所有用户，整个 Safe{Wallet} 应用程序运行正常。只有 Bybit 成了目标。

第三阶段：大劫案​

2025 年 2 月 21 日，Bybit 员工发起了一项本应是常规的从冷钱包（安全、离线存储）到温钱包（用于活跃交易）的转账。这需要授权人员的多重签名——这是一种标准的安全实践，称为多签（multisig）。

当签名者打开 Safe{Wallet} 批准交易时，界面显示了看似正确的接收地址。但恶意代码已经替换了不同的指令。员工在不知情的情况下批准了一项清空 Bybit 整个冷钱包的交易。

几分钟内，500,000 ETH（价值约 15 亿美元）流向了攻击者控制的地址。

技术漏洞：Delegatecall​

关键漏洞在于以太坊的 delegatecall 函数，该函数允许智能合约在自己的存储上下文中执行另一个合约的代码。攻击者诱使 Bybit 的签名者将他们的钱包合约逻辑更改为恶意版本，从而有效地授予了黑客完全控制权。

这不仅仅是以太坊或 Safe{Wallet} 核心协议中的漏洞。这是一场针对人为层面的攻击——即信任的员工验证和批准交易的时刻。

朝鲜 Lazarus Group：世界上获利最丰的黑客​

攻击发生后的 24 小时内，区块链调查员 ZachXBT 向 Arkham Intelligence 提交了证据，明确将此次攻击与朝鲜的 Lazarus Group 联系起来。联邦调查局（FBI）于 2025 年 2 月 26 日确认了这一归属。

Lazarus Group（也称为 TraderTraitor 和 APT38）在朝鲜侦察总局下属运作。它不是一个为了个人利益而谋利的犯罪团伙。这是一个由国家资助的行动，其所得用于资助朝鲜的核武器和弹道导弹计划。

数据令人震惊：

• 仅 2025 年：朝鲜黑客窃取了 20.2 亿美元的加密货币
• Bybit 的份额：15 亿美元（占朝鲜 2025 年从单一攻击中获利总额的 74%）
• 自 2017 年以来：朝鲜已窃取了超过 67.5 亿美元的加密资产
• 2025 年 vs 2024 年：被盗价值同比增长 51%

朝鲜占 2025 年全球所有被盗加密货币的 59%，以及所有交易所入侵事件的 76%。没有其他威胁行为者能与之相提并论。

加密货币窃取的产业化​

让朝鲜与众不同的不仅是规模，还有其行动的复杂程度。

社交工程胜过技术漏洞​

2025 年的大多数重大攻击都是通过社交工程而非技术漏洞实施的。这代表了一个根本性的转变。黑客不再主要寻找智能合约漏洞或加密弱点。他们瞄准的是人。

Lazarus Group 的特工已经以 IT 工作者的身份潜入加密货币公司。他们冒充高管。他们向开发人员发送包含恶意软件的工作邀请。Bybit 的攻击始于一名开发人员下载了一个虚假的股票交易模拟器——这是一个典型的社交工程媒介。

中国洗钱网络​

窃取加密货币仅仅是挑战的一半。在不被抓获的情况下将其转换为可用资金同样复杂。

朝鲜并没有直接变现，而是将洗钱业务外包给了调查人员所称的 “中国洗钱网络” (Chinese Laundromat) —— 一个由地下钱庄、OTC 经纪人和基于贸易的洗钱中介组成的庞大网络。这些角色跨链、跨司法管辖区和跨支付渠道清洗被盗资产。

到 2025 年 3 月 20 日 —— 即 Bybit 被黑事件发生不到一个月后 —— 首席执行官周本 (Ben Zhou) 报告称，黑客已经通过多个中介钱包、去中心化交易所和跨链桥，将 86.29% 的被盗 ETH 转换为比特币。重大盗窃案发生后为期 45 天的洗钱周期已成为一种可预测的模式。

尽管付出了这些努力，周本指出 88.87% 的被盗资产仍可追溯。但 “可追溯” 并不意味着 “可追回”。资金流经的司法管辖区与美国或国际执法部门没有合作关系。

Bybit 的应对：火线下的危机管理​

在发现漏洞后的 30 分钟内，首席执行官周本接管了指挥权，并开始在 X (前 Twitter) 上提供实时更新。他的信息非常直白：“即使这笔黑客损失无法追回，Bybit 仍具有偿付能力，所有客户资产均有 1:1 准备金支持，我们可以弥补损失。”

该交易所在 12 小时内处理了超过 350,000 份提币请求 —— 向用户发出信号，尽管损失惨重，业务仍将正常运行。

紧急融资​

在 72 小时内，Bybit 通过从 Galaxy Digital、FalconX 和 Wintermute 等合作伙伴处获得 447,000 ETH 的紧急融资，补充了其储备。Bitget 借出了 40,000 ETH 以确保提币不间断 —— Bybit 在三天内偿还了这笔借款。

网络安全公司 Hacken 进行了储备证明审计，确认 Bybit 的主要资产拥有超过 100% 的抵押支持。对于这种规模的危机，这种透明度是前所未有的。

赏金计划​

周本宣布 “向 Lazarus 宣战”，并启动了一项全球赏金计划，为导致资产冻结的信息提供高达 10% 的奖励。到年底，Bybit 已向帮助追踪或追回资金的贡献者支付了 218 万美元的 USDT。

市场的裁决​

到 2025 年底，Bybit 全球用户数突破 8000 万，日交易量达到 71 亿美元，在加密货币现货交易所中排名第 5。这次危机应对已成为如何从灾难性黑客攻击中幸存下来的案例研究。

2025 年：加密货币盗窃额达到 34 亿美元的一年​

Bybit 黑客攻击占据了头条新闻，但这只是更大模式的一部分。2025 年加密货币盗窃总额达到 34 亿美元 —— 创下新纪录，且为连续第三年增长。

关键统计数据：

• 2023 年：被盗 20 亿美元
• 2024 年：被盗 22 亿美元
• 2025 年：被盗 34 亿美元

朝鲜的份额从大约一半增长到所有加密货币盗窃案的近 60%。朝鲜民主主义人民共和国 (DPRK) 以更少的事件实现了更大规模的盗窃，展示了不断提高的效率和复杂性。

经验教训：安全防线在哪里失守​

Bybit 黑客攻击暴露了远远超出单一交易所的关键漏洞。

第三方风险关乎生存​

Bybit 本身并没有发生安全故障。Safe{Wallet} 出了问题。但 Bybit 承担了后果。

加密行业构建了复杂的依赖链，交易所依赖钱包提供商，钱包提供商依赖云基础设施，而云基础设施依赖于个人开发者的工作站。这条链条上任何一个环节的妥协都可能导致灾难性的连锁反应。

冷存储已不足够​

长期以来，行业一直将冷钱包视为安全的金标准。但 Bybit 的资金在被盗时正处于冷存储中。漏洞出现在移动资金的过程中 —— 即多重签名旨在保护的人工审批步骤。

当转账变得常规化时，签名者会产生一种虚假的安全感，将审批视为形式，而不是关键的安全决策。Bybit 的攻击正是利用了这种行为模式。

UI 是单点故障点​

多重签名安全假设签名者可以验证他们正在批准的内容。但如果显示交易详情的界面被篡改，验证就变得毫无意义。攻击者向签名者展示了一套内容，却执行了另一套操作。

预签名模拟 —— 允许员工在批准前预览交易的实际目的地 —— 本可以防止这种攻击。针对大额提币的延迟处理也是如此，这能为额外审查争取时间。

社会工程学击败技术安全​

你可以拥有世界上最复杂的密码学安全系统，但一个员工下载了错误的文件就可以绕过这一切。加密货币安全的薄弱环节日益趋向于人为因素，而非技术因素。

监管与行业影响​

Bybit 黑客攻击已经在重塑监管格局。

预计对以下方面的强制性要求：

• 用于密钥管理的硬件安全模块 (HSM)
• 实时交易监控和异常检测
• 定期的第三方安全审计
• 增强的 AML (反洗钱) 框架和大额转账的交易延迟

安全和合规正在成为市场准入的门槛。项目项目若无法证明其拥有强大的密钥管理、权限设计和可靠的安全框架，将发现自己与银行合作伙伴和机构用户隔绝。

对行业的意义​

Bybit 遭黑客攻击揭示了一个令人不安的事实：加密货币的安全模型仅与其最薄弱的运营环节一样强大。

整个行业在密码学安全方面投入了巨资——零知识证明、阈值签名、安全飞地（Secure Enclaves）。但如果攻击者能够诱骗人类批准恶意交易，那么最复杂的密码学也无济于事。

对于交易所来说，这一信息很明确：安全创新必须超越技术本身，涵盖运营流程、第三方风险管理和持续的员工培训。定期审计、协作式威胁情报共享和应急响应计划不再是可选项。

对于用户来说，教训同样深刻：即使是拥有最先进安全措施的大型交易所也可能被攻破。自托管、硬件钱包和分布式资产存储仍然是长期来看最安全的策略——即使它们不太方便。

结论​

朝鲜的 Lazarus Group 已经将加密货币盗窃工业化。自 2017 年以来，他们已窃取了超过 67.5 亿美元，而 2025 年是他们迄今为止最成功的一年。仅 Bybit 遭黑客攻击这一项——单次行动就获利 15 亿美元——就展示了足以让任何情报机构垂涎的能力。

加密行业正处于一场与国家支持的黑客的军备竞赛中，这些黑客拥有无限的耐心、尖端的技术能力，且无惧后果。Bybit 攻击之所以成功，并非因为任何新颖的漏洞利用，而是因为攻击者明白人，而非代码，才是最薄弱的环节。

在该行业以对待密码学安全同样的严谨态度对待运营安全之前，此类攻击仍将继续。问题不在于是否会再次发生十亿美元级别的黑客攻击，而在于何时发生，以及目标是否能像 Bybit 那样有效地做出反应。

本文仅用于教育目的，不应被视为财务建议。在与加密货币交易所和钱包互动时，请务必自行开展研究并优先考虑安全性。

智能合约审计中的形式化验证​

形式化验证是指使用基于数学和逻辑的技术来证明智能合约的正确性和安全性。在实践中，这涵盖了一系列方法：从基于属性的模糊测试和符号执行，到严格的定理证明和模型检查。其目标是确保合约满足其规范，并且在所有可能的输入和状态下不包含可利用的漏洞。鉴于 DeFi 协议中锁定了数十亿美元的巨额资金，形式化方法对于以太坊和其他区块链平台变得越来越重要。

传统方法： 以太坊早期的形式化方法包括像 Oyente 和 Mythril 这样的符号执行工具，以及像 Slither 和 Securify 这样的静态分析器。符号执行通过符号输入探索程序路径以检测问题（例如重入、整数溢出），而静态分析则使用基于规则的模式匹配。这些工具取得了一定的成功，但也存在局限性：例如，Oyente 即使在简单的合约上也会产生许多误报，而 Slither 基于模式的检测器也可能产生一些假阳性。此外，2023 年的一项研究发现，超过 80% 的可利用合约漏洞（尤其是复杂的“业务逻辑”漏洞）被现有工具所忽略，这凸显了对更强大验证技术的需求。

全面验证的前景与挑战： 理论上，形式化验证可以通过对所有状态进行详尽的不变量检查来证明漏洞不存在。像 Certora Prover 或以太坊基金会的 KEVM 框架等工具旨在根据形式化规范对智能合约进行数学验证。例如，Certora 的“自动化数学审计器”使用一种规范语言 (CVL) 来证明或反驳用户定义的规则。然而，在实践中，完全证明真实世界合约的属性通常是无法实现或非常耗费人力的。代码可能需要重写为简化的形式以便验证，必须编写自定义规范，循环和复杂算术可能需要手动设置边界或进行抽象，而 SMT 求解器在处理复杂逻辑时经常超时。正如 Trail of Bits 的工程师所指出的，在非平凡的代码库上*“证明漏洞不存在通常是无法实现的”*，并且实现这一目标通常需要大量的用户干预和专业知识。因此，形式化验证工具传统上仅用于代码的关键部分（例如，验证代币的不变量或共识算法），而不是端到端地验证整个合约。

Foundry 的模糊测试和不变量测试​

近年来，基于属性的测试已成为完全形式化证明的一种实用替代方案。Foundry 是一个流行的以太坊开发框架，它内置了对模糊测试和不变量测试的支持——这些技术极大地增强了测试覆盖率，可以被视为轻量级的形式化验证。Foundry 的模糊测试会自动生成大量输入，试图违反指定的属性，而不变量测试则将此扩展到一系列改变状态的操作：

• 模糊测试： 开发者不再为特定输入编写单元测试，而是指定应在任何输入下都成立的属性或不变量。然后，Foundry 生成成百上千个随机输入来测试该函数，并检查该属性是否始终成立。这有助于捕捉开发者可能不会手动想到去测试的边缘情况。例如，模糊测试可能会断言函数的返回值始终为非负数，或者某个后置条件在任何输入下都为真。Foundry 的引擎使用智能启发式方法——它分析函数签名并引入边缘情况值（0, max uint 等）——以触及可能破坏属性的角落案例。如果断言失败，Foundry 会报告一个违反该属性的反例输入。

• 不变量测试： Foundry 的不变量测试（也称为状态模糊测试）更进一步，它会按顺序执行多个函数调用和状态转换。开发者编写在合约生命周期内应始终为真的不变量函数（例如，总资产 = 用户余额之和）。然后，Foundry 随机生成调用序列（带有随机输入）来模拟多种可能的使用场景，并定期检查不变量条件是否仍然为真。这可以发现只有在特定操作序列后才会显现的复杂漏洞。本质上，不变量测试更彻底地探索了合约的状态空间，确保任何有效的交易序列都不能违反所声明的属性。

Foundry 的重要性： Foundry 使这些先进的测试技术变得易于使用。模糊测试和不变量功能原生于开发者工作流——不需要特殊的测试工具或外部工具，测试与单元测试一起用 Solidity 编写。得益于基于 Rust 的引擎，Foundry 可以快速执行数千个测试（并行化它们），并为任何不变量违规提供详细的失败跟踪。开发者报告说，Foundry 的模糊测试器易于使用且性能高，只需要少量配置（例如，设置迭代次数或添加假设来约束输入）。Foundry 文档中的一个简单例子是 divide(a,b) 函数的模糊测试，它使用 vm.assume(b != 0) 来避免无意义的无效输入，然后断言数学后置条件，如 result * b <= a。通过用数千个随机的 (a,b) 对运行这样的测试，Foundry 可能会迅速发现难以通过手动推理找到的边缘情况（如溢出边界）。

比较： Foundry 的方法建立在社区先前工作的基础上。Trail of Bits 的 Echidna 模糊测试器是早期用于以太坊的基于属性的测试工具。Echidna 同样生成随机交易来寻找违反不变量的情况，这些不变量表示为返回布尔值的 Solidity 函数。它以“智能”输入生成（结合了覆盖率引导的模糊测试）而闻名，并已用于发现许多漏洞。事实上，安全研究人员指出，Echidna 的引擎非常有效——“Trail of Bits 的 Echidna 是目前最好的模糊测试器，因为它有智能的随机数选择”——尽管 Foundry 的集成工作流使开发者编写测试更简单。在实践中，Foundry 的模糊测试通常被视为安全 Solidity 开发的新的**“最低标准”**，补充了传统的单元测试。它不能证明漏洞不存在（因为它是随机的而不是详尽的），但通过覆盖大量的输入和状态组合，它极大地增加了信心。

超越模糊测试：形式化证明和高级工具​

虽然模糊测试和不变量测试能捕捉到许多问题，但在某些情况下会使用更强的形式化方法。模型检查和定理证明涉及用形式化逻辑指定期望的属性，并使用自动证明器来对照合约代码进行检查。Certora Prover（最近已开源）是这一类别中的一个著名工具。它允许开发者用一种领域特定语言 (CVL) 编写规则，然后自动检查合约是否违反这些规则。Certora 已被用于验证 MakerDAO 和 Compound 等协议中的关键不变量；例如，它识别出了 MakerDAO 中被忽视了四年的“DAI 债务不变量”漏洞（一个微妙的记账不一致问题）。值得注意的是，Certora 的引擎现在支持多个平台（EVM、Solana 的 VM 和 eWASM），并且通过在 2025 年开源，它使得工业级的形式化验证在以太坊、Solana 和 Stellar 上免费可用。此举承认了形式化证明不应只是资金雄厚的团队的奢侈品。

其他形式化工具包括运行时验证方法（例如，以太坊的 KEVM 语义，或用于 Move-based 链的 Move Prover）。特别是 Move Prover 内置于 Move 语言中（被 Aptos 和 Sui 区块链使用）。它允许在代码旁边编写形式化规范，并能以类似于 linter 或类型检查器的用户体验自动证明某些属性。这种紧密的集成降低了这些平台上的开发者在开发过程中使用形式化验证的门槛。

总结： 如今的智能合约审计融合了这些方法。模糊测试和不变量测试（以 Foundry 和 Echidna 为代表）因其易用性和在捕捉常见漏洞方面的有效性而被广泛采用。符号执行和静态分析器仍然用于快速扫描已知的漏洞模式（像 Slither 这样的工具通常被集成到 CI 管道中）。与此同时，形式化验证工具正在成熟并扩展到多个链，但由于其复杂性，它们通常被保留用于特定的关键属性或由专业的审计公司使用。在实践中，许多审计结合了这些方法：例如，使用模糊测试器查找运行时错误，使用静态工具标记明显的错误，并对关键不变量（如“代币余额不超过总供应量”）进行形式化规范检查。

使用大语言模型的 AI 辅助审计​

像 OpenAI 的 GPT-3/4 (ChatGPT) 和 Codex 这样的大语言模型 (LLMs) 的出现，为智能合约分析引入了一种新的范式。这些模型在大量代码和自然语言上进行训练，能够推理程序行为、解释代码，甚至通过模式识别和“常识”知识检测某些漏洞。问题是：AI 能否增强甚至自动化智能合约审计？

基于 LLM 的漏洞分析工具​

已经出现了几项将 LLM 应用于智能合约审计的研究工作和原型工具：

• OpenAI Codex / ChatGPT (通用模型)： 早期的实验只是简单地向 GPT-3 或 Codex 提供合约代码并询问潜在的漏洞。开发者发现 ChatGPT 可以识别一些众所周知的漏洞模式，甚至建议修复方案。然而，响应时好时坏，并不可靠地全面。最近的一项学术评估指出，在基准数据集上，天真地提示 ChatGPT 进行漏洞检测*“与随机预测相比，并未产生显著更好的结果”*——基本上，如果模型没有得到适当的引导，它可能会捏造不存在的问题或错过真正的漏洞。这凸显了需要精心设计的提示词或微调才能获得有用结果。

• AuditGPT (2024)： 这是一个学术工具，专门利用 ChatGPT (GPT-3.5/4) 来检查以太坊合约中的 ERC 标准合规性。研究人员观察到，许多 ERC20/ERC721 代币合约违反了标准的微妙规则（这可能导致安全或兼容性问题）。AuditGPT 的工作方式是将审计分解为小任务，并为每种规则类型设计专门的提示词。结果令人印象深刻：在对真实合约的测试中，AuditGPT “成功地指出了 418 个 ERC 规则违规，并且只报告了 18 个误报”，展示了高准确性。事实上，该论文声称 AuditGPT 在发现 ERC 合规性漏洞方面优于专业的审计服务，且成本更低。这表明，对于定义明确、范围狭窄的领域（如执行一系列标准规则），一个带有良好提示词的 LLM 可以非常有效和精确。

• LLM-SmartAudit (2024)： 另一个研究项目 LLM-SmartAudit 采用更广泛的方法，使用多代理对话系统来审计 Solidity 代码。它设置了多个专门的 GPT-3.5/GPT-4 代理（例如，一个“审计员”专注于正确性，一个“攻击者”思考如何利用），它们相互交谈来分析一个合约。在他们的评估中，LLM-SmartAudit 能够检测到广泛的漏洞。值得注意的是，在与传统工具的对比测试中，基于 GPT-3.5 的系统实现了最高的整体召回率 (74%)，超过了他们测试的所有传统静态和符号分析器（次好的是 Mythril，召回率为 54%）。它还能够找到他们测试套件中所有 10 种类型的漏洞（而每个传统工具都在某些类别上表现不佳）。此外，通过切换到 GPT-4 并集中分析（他们称之为目标分析模式），该系统可以检测到像 Slither 和 Mythril 完全错过的复杂逻辑缺陷。例如，在一组真实世界的 DeFi 合约上，基于 LLM 的方法发现了数百个逻辑漏洞，而静态工具*“在检测这些问题上没有表现出任何效果”*。这些结果展示了 LLM 在捕捉超出传统分析器模式匹配范围的微妙漏洞方面的潜力。

• Prometheus (PromFuzz) (2023)： 一种混合方法是使用 LLM 来指导其他技术。一个例子是 PromFuzz，它使用一个基于 GPT 的“审计员代理”来识别代码中的可疑区域，然后自动生成不变量检查器并将其输入到模糊测试引擎中。本质上，LLM 进行第一遍分析（从善意和攻击者的角度），以将模糊测试集中在可能的漏洞上。在评估中，这种方法实现了非常高的漏洞发现率——例如，在某些基准测试集中召回率超过 86%，且零误报——显著优于独立的模糊测试器或以前的工具。这是一个有前途的方向：使用 AI 来协调和增强像模糊测试这样的经典技术，结合两者的优势。

• 其他 AI 工具： 社区已经看到了各种其他 AI 辅助审计的概念。例如，Trail of Bits 的“Toucan”项目将 OpenAI Codex 集成到他们的审计工作流中（下文将详细介绍其发现）。一些安全初创公司也在宣传 AI 审计器（例如，“ChainGPT Audit”服务），通常是用自定义提示词包装 GPT-4 来审查合约。开源爱好者在论坛上创建了基于 ChatGPT 的审计机器人，可以接收 Solidity 代码片段并输出潜在问题。虽然其中许多是实验性的，但总体趋势是明确的：AI 正在安全审查过程的各个层面被探索，从自动代码解释和文档生成到漏洞检测，甚至建议修复方案。

LLM 审计器的能力与局限性​

LLM 在智能合约审计中展示了显著的能力：

• 广泛的知识： 像 GPT-4 这样的 LLM 已经在无数的代码和漏洞上进行了训练。它“知道”常见的安全陷阱（重入、整数溢出等），甚至一些历史上的漏洞利用。这使得它能够识别可能表明存在漏洞的模式，并从文档中回忆起最佳实践。例如，它可能记得 ERC-20 的 transferFrom 应该检查授权（并将缺少此类检查标记为违规）。与只标记已知模式的静态工具不同，LLM 可以对新颖的代码应用推理，并推断出工具开发者没有明确编码进去的问题。

• 自然的解释： AI 审计器可以提供人类可读的潜在问题解释。这对开发者体验非常有价值。传统工具通常输出需要专业知识才能解释的神秘警告，而基于 GPT 的工具可以生成一段用通俗英语解释漏洞的段落，甚至建议修复方案。例如，AuditGPT 不仅标记了 ERC 规则违规，还描述了代码为何违反规则以及其影响。这有助于引导经验较少的开发者了解安全概念。

• 灵活性： 通过提示词工程，可以引导 LLM 关注不同的方面或遵循自定义的安全策略。它们不受固定规则集的限制——如果你能用语言描述一个属性或模式，LLM 就可以尝试检查它。这使得它们在审计可能具有独特不变量或逻辑的新协议时很有吸引力（在这种情况下，从头开始编写自定义静态分析是不可行的）。

然而，也观察到了重大的挑战和可靠性问题：

• 推理限制： 当前的 LLM 有时难以进行安全分析所需的复杂逻辑推理。Trail of Bits 报告说，“这些模型无法很好地推理某些更高级别的概念，例如合约的所有权、重入和函数间关系”。例如，GPT-3.5/4 可能在理论上理解什么是重入（甚至可以解释它），但如果需要理解跨函数的调用序列和状态变化，它可能无法识别出重入漏洞。模型也可能错过涉及多合约交互或时间依赖逻辑的漏洞，因为这些超出了单个代码片段分析的范围。

• 误报和幻觉： 一个主要问题是 LLM 可能会产生听起来自信但实际上不正确的结论。在审计中，“幻觉”可能是标记一个实际上不存在的漏洞，或误解代码。Trail of Bits 使用 Codex (GPT) 的实验发现，当他们扩展到更大的真实世界合约时，“误报和幻觉率变得过高”，以至于会因为太多虚假的报告而减慢审计员的速度。这种不可预测性是有问题的——一个经常“狼来了”的工具不会被开发者信任。AuditGPT 在保持低误报率（数百个发现中只有 18 个）方面的成功令人鼓舞，但那是在一个受限的领域。在通用用途中，需要仔细的提示词设计和可能的人工审查循环来过滤 AI 的发现。

• 上下文限制： LLM 有上下文窗口限制，这意味着它们一次只能“看到”一定数量的代码。复杂的合约通常跨越多个文件和数千行代码。如果 AI 无法消化整个代码库，它可能会错过重要的联系。像代码切片（分块提供合约）这样的技术被使用，但它们有失去全局视野的风险。LLM-SmartAudit 团队指出，使用 GPT-3.5 的 4k token 限制，他们无法分析一些大型的真实世界合约，直到他们切换到具有更大上下文的 GPT-4。即便如此，将分析分成部分也可能导致它忽略只有在考虑整个系统时才会显现的漏洞。这使得 AI 对整个协议（具有多个交互合约）的分析目前仍然是一个真正的挑战。

• 集成和工具： 围绕 AI 审计器的强大开发者工具仍然缺乏。运行 LLM 分析不像运行 linter 那样直接。它涉及对模型的 API 调用、处理提示词工程、速率限制以及解析 AI 的响应。正如一个审计团队所说，“围绕将 LLM 与传统软件集成的软件生态系统过于粗糙，一切都很麻烦”。几乎没有现成的框架可以在 CI 管道中持续部署 AI 审计器，同时管理其不确定性。这种情况正在慢慢改善（一些项目正在探索使用 GPT-4 进行代码审查的 CI 机器人），但这还处于早期阶段。此外，调试 AI 给出某个结果的原因很困难——与确定性工具不同，你无法轻易地追踪导致模型标记或错过某事的逻辑。

• 成本和性能： 使用像 GPT-4 这样的大型模型是昂贵的，而且可能很慢。如果你想将 AI 审计集成到 CI/CD 管道中，它可能会为每个合约增加几分钟的时间，并为大型代码产生显著的 API 成本。微调模型或开源 LLM 可以降低成本，但它们的能力往往不如 GPT-4。目前正在进行关于用于代码安全的更小、更专业模型的研究，但目前最好的结果来自大型专有模型。

总而言之，LLM 辅助审计前景广阔，但并非万能药。 我们看到的是混合方法，其中 AI 帮助生成测试或分析特定方面，而不是端到端地完成整个审计。例如，AI 可能会建议潜在的不变量或风险区域，然后由人工或其他工具进行调查。正如一位安全工程师所说，鉴于推理差距和集成障碍，该技术尚未准备好取代人类审计员来完成关键任务。然而，它已经可以成为一个有用的助手——在传统工具不足的情况下，“不完美的东西可能比什么都没有要好得多”。

不同工具链的准确性和可靠性​

比较所讨论的各种审计方法的准确性、覆盖率和可靠性是很有启发性的。以下是来自研究和行业评估的发现摘要：

• 静态分析工具： 像 Slither 这样的静态分析器因其快速反馈和易用性而受到重视。它们通常具有高精确率但中等召回率——这意味着它们报告的大多数问题都是真实问题（设计上误报很少），但它们只检测某些类别的漏洞。一项 2024 年的基准研究 (LLM-SmartAudit 的 RQ1) 发现，Slither 在一个测试套件中捕获了约 46% 的已知漏洞。Mythril（符号执行）表现稍好，召回率为 54%。每种工具在特定漏洞类型上都有优势（例如，Slither 非常擅长发现算术问题或 tx.origin 的使用，而符号工具则擅长发现简单的重入场景），但没有一个具有全面的覆盖率。像 Slither 这样的成熟工具的误报率相对较低——其开发者宣传*“误报最少，执行速度快（每个合约不到 1 秒）”*，使其适合在 CI 中使用。尽管如此，如果代码使用复杂的模式，静态工具可能会出错；它们可能会标记实际上已处理的边缘情况，或错过不匹配任何已知反模式的深层逻辑漏洞。

• 模糊测试和属性测试： 像 Foundry 的模糊/不变量测试或 Trail of Bits 的 Echidna 这样的模糊测试器在发现运行时错误和不变量违规方面非常有效。这些工具的误报率几乎为零，因为如果报告了一个漏洞（断言失败），它就是一个真实的反例执行。权衡在于漏报——如果一个漏洞在测试的输入空间或运行次数内没有显现，它就可能被漏掉。覆盖率取决于模糊测试器探索状态空间的好坏。只要有足够的时间和好的启发式方法，模糊测试器已经发现了许多静态分析错过的严重漏洞。例如，Echidna 能够快速重现 MakerDAO 和 Compound 的漏洞，而这些漏洞需要形式化验证才能找到。然而，模糊测试并不能保证找到每一个逻辑错误。随着合约变得越来越复杂，模糊测试器可能需要编写额外的不变量或使用更智能的搜索策略来触及更深的状态。在指标方面，模糊测试没有一个单一的“召回率”数字，但轶事证据表明，如果重要的不变量是可破坏的，通常可以被模糊测试器破坏。它所发现的东西可靠性很高（不需要手动筛选误报），但必须记住，通过模糊测试并不等于正确性的证明——只是信心的增加。

• 形式化验证工具： 在适用时，形式化验证提供最高的保证——一个成功的证明意味着100% 的状态都满足该属性。在准确性方面，对于它能证明的属性，它实际上是完美的（健全且完备的）。这里最大的问题不是结果的准确性，而是使用的难度和范围的狭窄。形式化工具在实践中也可能有漏报：它们可能因为复杂性而无法证明一个真实的属性（产生无结果或超时，这不是误报，但意味着我们未能验证实际上安全的东西）。它们也可能有规范错误，即工具“证明”了不是你意图的属性（用户错误）。在实际审计中，形式化方法已经捕获了一些关键漏洞（Certora 的成功案例包括在部署前捕获了一个微妙的 SushiSwap 漏洞和一个 PRBMath 库问题）。但它们的记录受限于它们被全面应用的频率——正如 Trail of Bits 指出的，“很难找到仅通过形式化验证发现的公开问题，相比之下，通过模糊测试发现的漏洞很多”。因此，虽然形式化验证在成功时非常可靠，但其对整体工具链覆盖率的影响受限于所需的精力和专业知识。

• 基于 LLM 的分析： AI 审计器的准确性目前是一个移动的目标，因为新技术（和更新的模型）正在迅速推动其发展。我们可以收集到一些数据点：

  • AuditGPT 系统专注于 ERC 规则，实现了非常高的精确率（按误报数计算约 96%），并发现了数百个静态工具或人类忽略的问题。但这是在一个具有结构化提示词的狭窄领域。我们不应将此推广为 ChatGPT 在任意漏洞搜寻中将有 96% 的准确性——在受控设置之外，其性能较低。
  • 在更广泛的漏洞检测中，LLM-SmartAudit (GPT-3.5) 在一个基准测试中显示出约 74% 的召回率和中等的误报率，这比任何单一的传统工具都要好。当升级到带有专门提示词的 GPT-4 (TA 模式) 时，它显著改善——例如，在一组 1400 个真实世界漏洞上，GPT-4 代理找到了约 48% 的特定问题和约 47% 的复杂逻辑问题，而 Slither/Mythril/Conkas 各自找到了约 0%（无）的那些特定复杂问题。这表明 LLM 可以极大地扩展覆盖范围，涵盖静态分析完全错过的漏洞类型。另一方面，LLM 没有找到超过一半的问题（所以它也有大量的漏报），并且不清楚它报告的问题中有多少是误报——该研究更关注召回率而不是精确率。
  • Trail of Bits 的 Codex/GPT-4 “Toucan” 实验说明了可靠性问题。最初，在小例子上，Codex 可以通过仔细的提示词识别已知的漏洞（所有权问题、重入）。但一旦他们尝试扩大规模，就遇到了不一致和不正确的结果。他们报告说*“即使在平均大小的代码中，失败的次数也很高”并且难以预测。最终，他们得出结论，GPT-4（截至 2023 年初）只是一个增量改进*，并且仍然*“缺少关键功能”*，如推理跨函数流程。结果是，AI 并未显著减少他们静态工具的误报，也未能可靠地加快他们的审计工作流程。换句话说，在该试验中，专业审计员认为通用 LLM 作为审计器的当前可靠性不足。

总结一下，每个工具链都有不同的优势：

• 静态工具： 可靠地快速检测已知问题；噪音低，但漏洞类型有限（在基准测试中召回率中等，约 40-50%）。
• 模糊/不变量测试： 精确率非常高（几乎没有误报），并且在发现功能性和状态依赖性漏洞方面表现出色；覆盖范围可以很广，但不能保证（没有简单的度量标准，取决于时间和不变量的质量）。如果给予足够的指导，通常能找到与形式化证明相同的漏洞。
• 形式化验证： 特定属性绝对正确性的黄金标准；如果成功应用，对于这些属性的召回率/精确率基本上是 100%。但实际上仅限于狭窄的问题，并需要大量精力（还不是一个用于全面审计的一键式解决方案）。
• AI (LLM) 分析： 潜在的高覆盖率——可以发现跨类别的漏洞，包括其他工具错过的漏洞——但精确率可变。通过专门的设置，它可以既精确又广泛（如 AuditGPT 对 ERC 检查所示）。没有仔细的限制，它可能会撒一张大网，需要人工审查结果。ChatGPT 在漏洞检测上的“平均”准确性并不出色（在一项研究中接近猜测），但使用 LLM 的最佳工程系统正在推动性能超越传统工具。目前有积极的研究旨在使 AI 输出更值得信赖（例如，通过让多个代理交叉验证，或将 LLM 与静态推理相结合以复核 AI 的结论）。

值得注意的是，结合各种方法可以产生最佳结果。例如，可以先运行 Slither（以无噪音的方式捕获低垂的果实），然后使用 Foundry/Echidna 来模糊测试更深层次的行为，或许再使用基于 LLM 的工具来扫描任何未考虑到的模式或不变量。每种方法都会覆盖其他方法的不同盲点。

实际采用中的挑战与局限性​

在实践中，在开发工作流中采用形式化验证或 AI 工具会带来实际的挑战。一些关键问题包括：

• 开发者体验和专业知识： 传统的形式化验证有陡峭的学习曲线。编写形式化规范（用 CVL、Coq、Move 的规范语言等）更像是编写数学证明而不是编写代码。许多开发者缺乏这方面的背景，而形式化方法专家供不应求。相比之下，使用 Foundry 进行模糊测试或用 Solidity 编写不变量要容易得多——感觉就像编写额外的测试。这是模糊测试在以太坊社区比形式化证明更快普及的一个重要原因。Trail of Bits 团队明确指出，在许多情况下，模糊测试**“产生类似的结果，但所需的技能和时间要少得多”**。因此，即使形式化验证可以捕获不同的漏洞，许多团队还是选择更简单的方法，以较低的精力获得足够好的结果。

• 集成到开发工作流中： 一个工具要被广泛采用，它需要适应 CI/CD 管道和日常编码。像 Slither 这样的工具在这方面表现出色——它*“可以轻松集成到 CI/CD 设置中，简化自动化并帮助开发者。”* 开发者可以将 Slither 或 Mythril 添加到 GitHub Action 中，并在发现问题时使构建失败。Foundry 的模糊测试可以作为每次 forge test 的一部分运行。不变量测试甚至可以使用像 CloudExec 这样的工具在云中持续运行，任何失败都可以使用 fuzz-utils 自动转换成单元测试。这些集成意味着开发者可以获得快速反馈并进行迭代。相比之下，像 Certora Prover 这样的工具在历史上是作为单独的进程运行（或由外部审计团队运行），可能需要数小时才能产生结果——这不是你会在每次提交时都运行的东西。基于 AI 的工具也面临集成障碍：调用 API 并在 CI 中确定性地处理其输出并非易事。还有一个安全和隐私的问题——许多组织对于将专有合约代码发送到第三方 AI 服务进行分析感到不安。自托管的 LLM 解决方案目前还不如大型云 API 强大，因此这是 AI 审计器在 CI 中采用的一个症结。

• 误报和噪音： 一个报告许多误报或低严重性发现的工具会降低开发者的信任。静态分析器过去一直受此困扰——例如，一些工具的早期版本会用警告淹没用户，其中许多是无关紧要的。信号与噪音之间的平衡至关重要。Slither 因其最少的误报而受到称赞，而像 Securify（在其研究形式中）这样的工具通常会产生许多需要手动过滤的警告。如前所述，如果不进行适当的目标定位，LLM 可能会产生噪音。这就是为什么目前 AI 的建议通常被视为建议性的，而不是绝对的。如果一个嘈杂的工具由单独的安全团队或在审计环境中使用，团队更有可能采用它，但对于日常使用，开发者更喜欢提供清晰、可操作、低噪音结果的工具。理想情况是仅在确定存在漏洞时**“使构建失败”**，而不是基于假设。实现这种可靠性是一个持续的挑战，特别是对于 AI 工具。

• 可扩展性和性能： 形式化验证可能是计算密集型的。如前所述，求解器可能会在复杂的合约上超时。这使得它难以扩展到大型系统。如果验证一个属性需要数小时，你不会在每次代码更改时都检查几十个属性。模糊测试也面临可扩展性限制——探索巨大的状态空间或具有许多方法的合约在组合上可能会很慢（尽管在实践中，模糊测试器可以在后台或通宵运行以加深其搜索）。AI 模型有固定的上下文大小，增加模型容量是昂贵的。虽然 GPT-4 的 128k-token 上下文是一个福音，但向其提供数百 KB 的合约代码成本高昂，并且对于非常大的项目仍然不够（想象一个包含许多合约的复杂协议——你可能会超过这个限制）。还有一个多链扩展的问题：如果你的项目涉及不同链上合约之间的交互（以太坊 ↔ 另一条链），验证或分析这种跨链逻辑更加复杂，并且可能超出了当前工具的能力。

• 人工监督和验证： 归根结底，大多数团队仍然依赖专家级的人类审计员进行最终签核。自动化工具是辅助工具，而不是替代品。所有这些工具的一个局限性是它们在已知属性或模式的范围内操作。它们可能会错过一种全新的漏洞类型或 DeFi 协议设计中微妙的经济缺陷。人类审计员利用直觉和经验来思考攻击者可能如何接近系统，有时是以任何工具都没有明确编程的方式。有些情况下，合约通过了所有自动化检查，但后来有人在业务逻辑或创造性的攻击向量中发现了漏洞。因此，一个挑战是避免产生虚假的安全感——开发者必须正确解释形式化工具和 AI 的输出，而不是假设“未发现问题”就意味着代码 100% 安全。

• 维护规范和测试： 特别是对于形式化验证，一个实际问题是规范漂移。随着代码的演变，规范（不变量、规则等）可能会过时。确保代码及其形式化规范保持同步是一项不小的管理任务。如果开发者不警惕，证明可能会“通过”，仅仅因为它们证明的东西与代码的实际需求不再相关。同样，随着系统预期行为的变化，不变量测试也必须更新。这需要一种并非所有团队都具备的、以不变量驱动的开发文化（尽管正在推动鼓励这种文化）。

总而言之，主要的限制是人和流程，而不是技术的原始能力。形式化和 AI 辅助方法可以极大地提高安全性，但它们必须以适合开发者工作流程和技能集的方式部署。令人鼓舞的是，像不变量驱动开发（从第一天起就写下关键不变量）这样的趋势正在获得关注，并且工具正在慢慢改进，使高级分析更加即插即用。主要工具的开源（例如 Certora Prover）和模糊测试集成到流行框架（Foundry）正在降低门槛。随着时间的推移，我们期望在使用这些强大的验证技术方面，“普通开发者”能做的和“博士研究员”能做的之间的差距将会缩小。

开源与商业审计工具​

智能合约安全工具的领域包括开源项目和商业服务。两者各有其角色，并且常常互为补充：

• 开源工具： 以太坊生态系统中大多数广泛使用的审计工具都是开源的。这包括 Slither（静态分析器）、Mythril（符号执行）、Echidna（模糊测试器）、Manticore（符号/混合执行）、Securify（来自苏黎世联邦理工学院的分析器）、Solhint/Ethlint（linter），当然还有 Foundry 本身。开源工具受到青睐有几个原因：（1）透明度——开发者可以看到工具如何工作，并相信没有恶意或隐藏的东西发生（这在一个开放的生态系统中很重要）。（2）社区贡献——规则和功能由广泛的社区添加（例如，Slither 有许多社区贡献的检测器）。（3）成本——它们是免费使用的，这对于 Web3 中许多小型项目/初创公司很重要。（4）集成——开源工具通常可以在本地或 CI 中运行，没有法律障碍，并且通常可以为项目特定需求进行定制或编写脚本。

  开源工具发展迅速。例如，Slither 对新 Solidity 版本和模式的支持由 Trail of Bits 持续更新。由 ConsenSys 开发的 Mythril 不仅可以分析以太坊，还可以通过处理字节码来分析任何 EVM 兼容链——这展示了开源工具如何轻松地跨链重用。开源工具的缺点是它们通常带有*“使用风险自负”*的声明——没有官方支持或保证。它们可能无法扩展或没有商业产品 UI 的精美。但在区块链领域，即使是许多公司也在内部使用开源作为其核心工具（有时会进行轻微的自定义修改）。

• 商业服务和工具： 一些公司将安全分析作为产品提供。例子包括 MythX（ConsenSys Diligence 的基于云的扫描 API）、Certora（在开源之前将其证明器作为服务提供）、CertiK 和 SlowMist（这些公司拥有内部扫描器和 AI，用于审计或通过仪表板提供），以及一些新进入者，如来自 ChainSecurity 的 Securify（该公司被收购，其工具在内部使用）或 SolidityScan（一个输出审计报告的云扫描器）。商业工具通常旨在提供更用户友好的体验或集成服务。例如，MythX 与 IDE 扩展和 CI 插件集成，以便开发者可以将他们的合约发送到 MythX 并获得详细的报告，包括漏洞评分和修复细节。这些服务通常在后台运行多种分析技术的组合（模式匹配、符号执行等），并经过调整以最小化误报。

  商业工具的价值主张通常是便利性和支持。它们可能会维护一个持续更新的漏洞知识库，并提供客户支持来解释结果。它们也可能在云中处理繁重的计算（这样你就不需要在本地运行求解器）。然而，成本是一个因素——鉴于有免费的替代品，许多项目选择不为这些服务付费。此外，本着去中心化的精神，一些开发者对依赖闭源服务来保障安全持保留态度（“验证，而不是信任”的理念）。Certora Prover 在 2025 年的开源是一个值得注意的事件：它将一个高端商业工具变成了社区资源。此举预计将加速其采用，因为现在任何人都可以尝试在没有付费许可的情况下形式化验证他们的合约，并且代码的开放性将允许研究人员改进该工具或将其应用于其他链。

• 人工审计服务： 值得一提的是，除了软件工具，许多审计是由专业公司（Trail of Bits、OpenZeppelin、Certik、PeckShield 等）完成的。这些公司使用上述工具（主要是开源的）和专有脚本的混合。这些工作的产出通常是保密的，或仅在审计报告中进行总结。这里并不完全是“开源与商业”的二分法，因为即使是商业审计公司也严重依赖开源工具。区别更多在于专业知识和手动工作。话虽如此，一些公司正在开发专有的 AI 辅助审计平台，以给自己带来优势（例如，有报道称*“ChainGPT”被用于内部审计，或 CertiK 开发了一个名为Skynet*的 AI 用于链上监控）。这些本身不是公共工具，因此它们的准确性和方法没有被广泛记录。

在实践中，一种常见的模式是开源优先，商业可选。团队在开发和测试期间会使用开源工具（因为它们可以轻松集成并根据需要频繁运行）。然后，他们可能会在部署前使用一两个商业服务作为额外的检查——例如，运行一次 MythX 扫描以获得“第二意见”，或聘请一家使用像 Certora 这样的高级工具来形式化验证关键组件的公司。随着界限变得模糊（Certora 开源，MythX 的结果经常与开源工具重叠），区别更多地在于支持和便利性，而不是能力。

一个值得注意的交叉点是 Certora 的多链支持——通过正式支持 Solana 和 Stellar，他们解决了在这些平台上开源替代品较少的问题（例如，以太坊有许多开源工具，而 Solana 直到最近几乎没有）。随着安全工具扩展到新的生态系统，我们可能会看到更多的商业产品填补空白，至少在开源赶上之前是这样。

最后，值得注意的是，开源与商业在这里并非对立关系；它们常常相互学习。例如，在学术/商业工具中开创的技术（如 Securify 中使用的抽象解释）最终会进入开源工具，反之，来自开源工具使用的数据可以指导商业工具的改进。双方追求的最终结果是为整个生态系统提供更好的安全性。

跨链适用性​

虽然以太坊一直是大多数这些工具的焦点（鉴于其在智能合约活动中的主导地位），但形式化验证和 AI 辅助审计的概念也适用于其他区块链平台。以下是它们如何应用的：

• EVM 兼容链： 像 BSC、Polygon、Avalanche C-Chain 等使用以太坊虚拟机 (EVM) 的区块链，可以直接使用所有相同的工具。模糊测试或静态分析不关心你的合约是部署在以太坊主网上还是 Polygon 上——字节码和源语言（Solidity/Vyper）是相同的。实际上，Mythril 和 Slither 可以通过从地址拉取字节码来分析任何 EVM 链的合约（Mythril 只需要一个 RPC 端点）。这些链上的许多 DeFi 项目运行 Slither 和 Echidna 的方式与以太坊项目完全相同。对 BSC 或 Avalanche 上协议的审计通常使用与以太坊审计相同的工具包。因此，在 EVM 环境中，跨链主要意味着重用以太坊的工具链。

• Solana： Solana 的智能合约是用 Rust 编写的（通常通过 Anchor 框架），并在 BPF 虚拟机上运行。这与以太坊的环境非常不同，所以以太坊特定的工具无法直接使用。然而，同样的原则适用。例如，可以使用 Rust 的原生模糊测试库或像 cargo-fuzz 这样的工具对 Solana 程序进行模糊测试。直到最近，Solana 上的形式化验证几乎不存在。Certora 和 Solana 工程师之间的合作为 Solana 程序产生了一个内部验证工具，可以根据规范证明 Rust/Anchor 合约。如前所述，Certora 将其证明器扩展到了 Solana 的 VM，这意味着开发者可以像为 Solidity 那样编写关于 Solana 程序行为的规则并进行检查。这很重要，因为 Solana 的快速发展方式意味着许多合约在没有经过以太坊那种严格测试的情况下就启动了；形式化工具可以改善这一点。对 Solana 的 AI 审计也是可行的——一个理解 Rust 的 LLM 可以被提示检查 Solana 程序的漏洞（如缺少所有权检查或算术错误）。它可能需要针对 Solana 特定的模式进行微调，但鉴于 Rust 的流行度，GPT-4 在阅读 Rust 代码方面相当熟练。我们可能很快就会看到类似“ChatGPT for Anchor”的工具出现。

• Polkadot 和基于 Substrate 的链： Polkadot 的智能合约可以用 Rust 编写（编译成 WebAssembly），使用 ink! 框架，或者你可以运行一个 EVM pallet（就像 Moonbeam 那样），这再次允许使用 Solidity。在 ink!/Wasm 的情况下，验证工具仍处于起步阶段。可以尝试使用通用的 Wasm 验证框架来形式化验证 Wasm 合约的属性（例如，微软的 Project Verona 或其他项目已经研究了 Wasm 的安全性）。Certora 的开源证明器也提到了对 Stellar 的 WASM 智能合约的支持，这在概念上与任何基于 Wasm 的链相似。因此，它很可能也适用于 Polkadot 的 Wasm 合约。对 ink! 合约进行模糊测试可以通过编写 Rust 测试来完成（Rust 中的属性测试可以起到类似的作用）。对 ink! 合约的 AI 审计也需要分析 Rust 代码，这同样是 LLM 在有正确上下文的情况下可以做到的（尽管它可能在没有一些提示的情况下不知道特定的 ink! 宏或 trait）。

  此外，Polkadot 正在探索使用 Move 语言进行并行智能合约开发（正如一些社区论坛所暗示的）。如果 Move 在 Polkadot 平行链上被使用，Move Prover 就会随之而来，从设计上就带来了形式化验证能力。Move 对安全性的强调（面向资源的编程）和内置的证明器展示了形式化方法从一开始就在跨链传播。

• 其他区块链： 像 Tezos（Michelson 智能合约）和 Algorand（TEAL 程序）这样的平台各自都有形式化验证的努力。例如，Tezos 有一个名为 Mi-Cho-Coq 的工具，它提供了 Michelson 的形式化语义并允许证明属性。这些更多是学术性的，但表明任何具有明确定义的合约语义的区块链都可以进行形式化验证。原则上，AI 审计可以应用于任何编程语言——这只是一个适当地训练或提示 LLM 的问题。对于不太常见的语言，LLM 可能需要一些微调才能有效，因为它可能没有在足够多的例子上进行预训练。

• 跨链交互： 一个新的挑战是验证跨链的交互（如桥接或链间消息传递）。这里的形式化验证可能涉及对多个链的状态和通信协议进行建模。这非常复杂，目前超出了大多数工具的能力，尽管特定的桥接协议已经过手动安全分析。AI 可能有助于审查跨链代码（例如，审查一个与 Cosmos 上的 IBC 协议交互的 Solidity 合约），但目前还没有现成的解决方案。

本质上，以太坊的工具为其他链铺平了道路。许多开源工具正在被改造：例如，有努力创建一个类似 Slither 的 Solana (Rust) 静态分析器，而不变量测试的概念是语言无关的（基于属性的测试存在于许多语言中）。强大引擎的开源（如 Certora 的多 VM 引擎）对于跨链安全尤其有前途——同一个平台可以用来验证 Solidity 合约、Solana 程序和 Move 合约，只要每个都有适当的规范编写。这鼓励了整个行业更统一的安全态势。

还值得注意的是，AI 辅助审计将使所有链受益，因为模型可以被教导关于任何上下文中的漏洞。只要向 AI 提供正确的信息（语言规范、该生态系统中的已知漏洞模式），它就可以应用类似的推理。例如，可以要求 ChatGPT 用适当的提示词审计一个 Solidity 合约或一个 Move 模块，它两者都能做到——如果它有这个概念，它甚至可能捕获到类似*“这个 Move 模块可能违反了资源守恒”*的问题。限制在于 AI 是否接触到了足够多的该链的训练数据。以太坊作为最受欢迎的链，很可能使模型偏向于最擅长 Solidity。随着其他链的增长，未来的 LLM 或微调的衍生品也可以覆盖这些。

结论​

智能合约形式化验证与 AI 辅助审计是一个快速发展的领域。我们现在拥有一个丰富的工具包：从提高代码可靠性的确定性静态分析器和模糊测试框架，到能够以类似人类的方式推理代码的前沿 AI。形式化验证，曾是一个小众的学术追求，正通过更好的工具和集成变得更加实用。AI，尽管目前存在局限性，但在自动化安全分析方面已经展现出改变游戏规则的能力的曙光。

目前还没有一刀切的解决方案——现实世界的审计结合了多种技术以实现纵深防御。Foundry 的模糊测试和不变量测试已经提高了部署前的期望标准（捕获了许多会绕过基本测试的错误）。AI 辅助审计，如果谨慎使用，可以作为审计员的力量倍增器，以手动审查无法比拟的规模和速度突出问题并验证合规性。然而，人类的专业知识对于驱动这些工具、解释它们的发现以及定义要检查的正确属性仍然至关重要。

展望未来，我们可以期待这些方法的更大程度的融合。例如，AI 可能帮助编写形式化规范或建议不变量（“AI，这个 DeFi 合约应该遵守哪些安全属性？”）。模糊测试工具可能会结合 AI 来更智能地引导输入生成（正如 PromFuzz 所做的那样）。形式化验证引擎可能会使用机器学习来决定应用哪些引理或启发式方法。所有这些都将有助于在不仅是以太坊，而且是所有区块链平台上构建更安全的智能合约。最终的愿景是，未来关键的智能合约可以在对其正确性有高度信心的情况下部署——这个目标很可能通过形式化方法和 AI 辅助的协同使用来实现，而不是单独依赖任何一种。

来源：

• Foundry 模糊测试和不变量测试概述
• Trail of Bits 关于模糊测试与形式化验证的论述
• Trail of Bits 关于形式化验证局限性的论述
• Patrick Collins 关于模糊/不变量测试与形式化方法的比较
• Trail of Bits 关于审计中不变量的论述
• Medium (BuildBear) 关于 Slither 和 Mythril 的使用
• AuditGPT 结果（ERC 合规性）
• Trail of Bits 关于 LLM (Codex/GPT-4) 局限性的论述
• LLM-SmartAudit 与传统工具的性能比较
• “Detection Made Easy” 关于 ChatGPT 准确性的研究
• PromFuzz (LLM+模糊测试) 性能
• Certora 开源公告（多链）
• Move Prover 描述 (Aptos)
• 静态分析背景（智能合约安全文献）