Compass: Navigating the Design Space of Taint Schemes for RTL Security Verification

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.