paperbot · PL 论文追踪

全部论文 待读 收藏

P2 TasmScan: Continuation-Aware Taint Analysis for TVM Bytecode with Savelist Abstraction

TasmScan:面向 TVM 字节码的续延感知污点分析与 Savelist 抽象
ASE Proceedings of the 41st IEEE/ACM International Conference on Automated Software Engineering2026匹配度 4/10 · 这是一篇方法论扎实的静态分析论文(抽象解释、IR 提升、路径敏感污点分析、形式化过近似保证、含人工标注 benchmark 与工业级语料评估),在研究品味上与用户偏好(理论+工程、问题驱动、工业落地、benchmark 建设)高度契合;但其应用域是 TON 区块链 TVM 字节码与智能合约缺陷检测,与用户画像的四条主线(PL↔AI/Agentic 程序、浮点程序分析、贝叶斯程序分析)均无交集,尤其完全不涉及 LLM。引用 0 inbox
Yixuan Liu, Yin Wu, Yi Li
crossref: 2026-10-09

AI 速览

一句话:提出首个 TVM 字节码级静态分析框架,通过建模 savelist 语义实现跨续延污点分析并检测合约缺陷。

TON 智能合约运行于 TVM,TVM 使用一等续延与 savelist 跨续延管理寄存器和控制流;被 savelist 捕获的寄存器可绕过操作数栈传递数据,导致字节码级分析无法完整跟踪数据流。TasmScan 是首个无需源码的 TVM 字节码静态分析框架:以前向寄存器分析建模 savelist 语义,对精确解析的保存点与局部寄存器定义给出过近似保证;再将字节码提升为类型化 IR TASIR,进行路径敏感、上下文感知的污点分析以检测缺陷。在 2,921 个 TON 合约与 208 个标注基准上,TasmScan 以 100% 精度解析 294,546 个动态续延目标;五类缺陷召回 95.3%、精度 96.8%,抽样估计整体精度 85.8%,较符号执行基线中位加速 17×,路径分析无崩溃或超时。

问题
TVM 的一等续延和 savelist 允许寄存器状态跨续延边界隐式传递,使字节码级静态分析难以构建完整数据流,且现有方法依赖源码或符号执行。
方法
提出 TasmScan,用前向寄存器分析建模 savelist 语义并提升到类型化中间表示 TASIR,进而执行路径敏感、上下文感知的污点分析。
评估
在 2,921 个真实 TON 合约和 208 个带人工标注真值的基准上评估,报告续延目标解析精度、五类缺陷检测召回/精度、消融实验以及与符号执行基线的性能对比。
原文摘要(Abstract)

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 17× 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.

链接与引用

DOI 原文 · arXiv ·

BibTeX
@inproceedings{paperbot12395,
  title = {TasmScan: Continuation-Aware Taint Analysis for TVM Bytecode with Savelist Abstraction},
  author = {Yixuan Liu and Yin Wu and Yi Li},
  booktitle = {ASE},
  year = {2026},
  doi = {10.1145/3832783.3834346}
}