[Paper] SseRex：实用的 Solana 智能合约符号执行

发布: 3天前 (2026年3月17日 GMT+8 18:33)

8 分钟阅读

原文: arXiv

Source: arXiv - 2603.16349v1

概述

Solana 的高吞吐量区块链正吸引大量智能合约开发者，但其独特的账户模型也导致了一系列安全漏洞。SseRex 是首个专为 Solana 程序构建的符号执行引擎，能够自动发现传统分析工具遗漏的平台特定陷阱。

SseRex 将 Solana 程序视为一个符号状态机：

字节码提升 – 将链上 BPF 字节码提升为中间表示（IR），在保留低层控制流的同时，暴露 Solana 特有的 API 调用（例如 invoke、invoke_signed）。
账户模型建模 – 将每条指令所需的账户表示为携带 owner、signer、writable 等属性的符号对象。执行器会跟踪这些属性在程序执行过程中的验证情况（或缺失情况）。
路径探索 – 使用经典的深度优先符号执行引擎，SseRex 探索可行的执行路径，为分支条件以及账户字段的取值生成约束。
漏洞检查 – 在每条路径探索完毕后，引擎会应用一组基于规则的检查：
- 缺失所有者检查 – 程序是否在未确认 account.owner == expected_program_id 的情况下读取或写入账户？
- 缺失签名者检查 – 在执行特权操作前是否验证了所需的签名？
- 缺失密钥检查 – 在使用公钥之前是否将其与预期值进行比较？
- 不安全的 CPI – 程序是否在未约束被调用程序账户的情况下调用了其他程序？
约束求解 – 当检测到潜在漏洞时，SMT 求解器会尝试找到具体输入（账户数据、签名），以触发不安全行为，从而生成可复现的概念验证（PoC）。

整个流水线仅基于字节码运行，因此可用于尚未在 Rust 层开源的合约。

覆盖率: SseRex 成功分析了 8,714 个已编译的 Solana 合约，平均每个耗时 3.2 秒。
漏洞检测: 标记了 467 个合约（≈5.4 %）存在至少一种目标漏洞。
对比: 与两款针对 Solana 调整的最先进静态分析器相比，SseRex 实现了 +27 % 更高的真实阳性率和 ‑15 % 更低的误报率。
案例研究: 对四个流行开源项目的深入检查发现了细微漏洞，例如：
- 缺少签名者检查，导致攻击者能够重放代币铸造指令。
- 未检查的 CPI，使恶意程序通过提供精心构造的账户劫持资金。
实际影响: 许多已识别的问题与近期 Solana 利用中的模式相匹配，证实 SseRex 能在漏洞被武器化前发现 预利用 条件。

开发者工具：将 SseRex 集成到 CI/CD 流程中，为 Solana 开发者提供自动化的“安全 lint”，提前捕获平台特有的错误，降低部署后修补的高昂成本。
审计员效率：审计公司可以使用 SseRex 对大型代码库进行初步筛选，将人工审查重点放在引擎标记的高风险路径上。
市场安全：托管用户提交的 Solana 程序的平台（如 DeFi 聚合器、NFT 市场）可以将 SseRex 作为守门人，阻止存在漏洞的合约上架。
教育：工具生成的具体概念验证输入可作为教学材料，帮助开发者学习 Solana 账户模型的细微差别。
跨链工具：该方法展示了符号执行如何适配具有非以太坊账户语义的其他区块链，鼓励在 Web3 生态系统中更广泛地采用形式化分析。

可扩展性到超大程序 – 虽然 SseRex 能高效处理典型合约，但极大的程序以及深层循环可能导致路径爆炸；未来工作将探索启发式方法和有界模型检查以缓解此问题。
动态数据源 – 当前模型假设账户数据是静态的；处理运行时加载的数据（例如通过链上反序列化自定义结构体）可能会遗漏某些漏洞。
漏洞集合有限 – 该工具聚焦于四种 Solana 特定模式；计划扩展规则集以覆盖重入、算术溢出以及 gas 相关问题。
与源代码层工具的集成 – 将字节码分析与 Rust 源代码层注解相结合，可提升开发者的使用体验并降低误报。

底线：SseRex 表明，当符号执行针对区块链独特的运行时模型进行调优时，能够成为针对 Solana 下一波智能合约攻击的实用、开发者友好的防御手段。