一句话：Compass 用统一术语与 CEGAR 精化，为 RTL 设计各组件自动选择尽量轻量且满足安全验证目标的污点分析方案。
该论文研究硬件信息流跟踪中污点分析的精度与复杂度权衡问题：不同污点方案在验证能力与开销之间存在广泛取舍空间，而将不同方案应用于硬件设计的不同组件可提升整体效率。为此，作者提出 Compass 框架，首先建立统一术语以全面刻画已有污点方案，然后引入反例引导的抽象精化（CEGAR）迭代改进污点方案，从而在满足安全验证目标的前提下尽可能降低方案开销。评估在多个开源 RISC-V 处理器上进行，用于验证推测执行漏洞相关的信息流性质，结果表明 Compass 同时显著提升了污点分析的仿真速度与形式验证可扩展性。
Hardware information flow tracking (IFT) using taint analysis provides a methodology to check whether a hardware design satisfies certain security properties. Previous work has shown a broad trade-off space between precision and complexity when using different taint analysis schemes. A careful investigation of this space has led to the insight that applying different taint schemes to different components of a hardware design can improve overall efficiency. We present Compass, a systematic framework to guide users in designing appropriate taint schemes that are as lightweight as possible while still sufficient to accomplish their security verification goals. We first establish a unified terminology to comprehensively capture existing taint schemes. We then apply counterexample-guided abstraction refinement (CEGAR) for taint refinement to iteratively improve the taint scheme. We evaluated Compass on a set of open-source RISCV processors to verify the information flow properties for speculative execution vulnerabilities, and demonstrate that Compass significantly improves both simulation speed and formal-verification scalability of taint analysis.
@inproceedings{YangTBM026,
title = {Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification},
author = {Yuheng Yang and Qinhan Tan and Thomas Bourgeat and Sharad Malik and Mengjia Yan},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790144}
}