@inproceedings{741e02b2510b45f4b540eecb6bb16e56,
title = "Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification",
abstract = "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.",
keywords = "counterexample-guided abstraction refinement, hardware information flow tracking, speculative execution attacks, taint analysis",
author = "Yuheng Yang and Qinhan Tan and Thomas Bourgeat and Sharad Malik and Mengjia Yan",
note = "Publisher Copyright: {\textcopyright} 2026 Owner/Author.; 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, ASPLOS 2026 ; Conference date: 22-03-2026 Through 26-03-2026",
year = "2026",
month = mar,
day = "22",
doi = "10.1145/3779212.3790144",
language = "English (US)",
series = "International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS",
publisher = "Association for Computing Machinery",
pages = "442--458",
booktitle = "ASPLOS 2026 - Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2",
}