TasmScan：基于保存列表抽象的TVM字节码延续感知污点分析

中文摘要 AI 辅助

开放网络（TON）的峰值市值超过200亿美元，链上激活地址超过1.75亿，其智能合约的执行依赖于TVM（TON虚拟机）。TVM使用带有保存列表（savelist）的一等延续（first-class continuations）来管理控制流以及跨延续调用时的寄存器状态。由于保存列表捕获的寄存器允许数据在不经过操作数栈的情况下跨越延续边界流动，因此字节码级分析若不显式建模保存列表语义，则无法构建完整的数据流跟踪。我们提出了TasmScan，这是首个针对TVM的字节码级静态分析框架，无需源代码即可实现跨延续的数据流推理。TasmScan通过前向寄存器分析对保存列表语义进行建模，该分析对精确解析的保存点和局部跟踪的寄存器定义具有形式化的过近似保证，随后将字节码提升为TASIR（一种类型化中间表示），并执行具有上下文感知源（context-aware sources）的路径敏感污点分析以检测缺陷。我们在TON验证者注册表中的2,921个合约以及一个包含208个合约、具有人工确认真值标签的基准上评估了TasmScan。在完整语料库上，TasmScan以100%的精确率解析了294,546个动态延续目标；消融实验证实，保存列表传播对于解析依赖跨延续寄存器传递的间接寄存器调用至关重要。在基准上，TasmScan在五类缺陷上检测出95.3%的缺陷，精确率为96.8%。从完整语料库中抽取的366对分层样本估计总体精确率为85.8%。TasmScan相比最先进的符号执行基线实现了17倍的中位加速，在路径分析比较中，100%的分析完成且零崩溃或超时。

英文摘要

The Open Network (TON), with a peak market capitalization exceeding $20 billion and over 175 million activated on-chain addresses, relies on the TVM (TON Virtual Machine) to execute smart contracts. TVM uses first-class continuations with savelists to manage control flow and register state across continuation invocations. Since savelist-captured registers allow data to flow across continuation boundaries without passing through the operand stack, bytecode-level analyses cannot construct complete data flow tracking without explicitly modeling savelist semantics. We present TasmScan, the first bytecode-level static analysis framework for TVM that enables cross-continuation data flow reasoning without requiring source code. TasmScan models savelist semantics via forward register analysis with a formal over-approximation guarantee for exact-resolved save sites and locally tracked register definitions, then lifts bytecode into TASIR, a typed intermediate representation, and performs path-sensitive taint analysis with context-aware sources to detect defects. We evaluate TasmScan on 2,921 contracts from the TON verifier registry and a labeled benchmark of 208 contracts with human-confirmed ground truth. On the full corpus, TasmScan resolves 294,546 dynamic continuation targets with 100% precision; ablation confirms that savelist propagation is essential for resolving indirect register calls that depend on cross-continuation register passing. On the benchmark, TasmScan detects 95.3% of defects across five classes with 96.8% precision. A 366-pair stratified sample from the full corpus estimates 85.8% overall precision. TasmScan offers a 17x median speedup over the state-of-the-art symbolic-execution baseline, and in the path-analysis comparison completes 100% of analyses with zero crashes or timeouts.

发表机构

• Nanyang Technological University（南洋理工大学）
• Xi’an Jiaotong University（西安交通大学）

机构由 AI 辅助整理，请以论文原文为准。