Advancing Hardware Information Flow Tracking: Reconvergence-Aware Counterexample-Guided Automated Taint Refinement

Abstract

Hardware security is the foundation of computer security --- vulnerabilities discovered at this layer are known to bypass even cryptographically-secure software protections. As a result, there is a need for an efficient, comprehensive mechanism to detect when secret values leak to adversary-observable outputs. One key approach is taint propagation, which augments the original circuit with additional logic to reason about such information flows. However, existing taint propagation approaches suffer from two key limitations. First, they can be overly conservative, introducing unnecessarily complex taint logic that incurs significant performance and area overhead in cases where simpler logic would have sufficed. Second, there is currently no automated method capable of resolving all false positive types --- manual efforts are often infeasible given the scale and complexity of modern processor designs. These limitations motivate the goal of this work: to develop an automated taint refinement scheme that minimizes taint logic complexity while achieving sufficient precision to systematically eliminate all false positive types.