3 min to read

Pathfinder

Constructing Cycle-accurate Taint Graphs for Analyzing Information Flow Traces

Pathfinder is a new framework for simplifying the analysis of information flow violations in hardware.
When security properties such as confidentiality or integrity are violated, hardware verification tools produce traces containing thousands of signals. Manually backtracking these traces to pinpoint the root cause of the violation is time-consuming and error-prone. Pathfinder introduces taint graphs, a novel abstraction that provides spatio-temporal context for where, when, and why information propagates.

To support diverse verification workflows, Pathfinder first establishes a unified theoretical foundation showing the equivalence of two widely used information flow tracking (IFT) approaches: taint tracking and self-composition. Building on this abstraction, Pathfinder automatically generates taint graphs from Hardware Description Language (HDL) designs and violation traces produced by simulation or formal tools.

Applied across a range of case studies including constant-time violations, temporal fencing, hardware Trojans, and Spectre, Pathfinder reduces the number of signals engineers must manually inspect by factors between 1.6× and 769.9×.

What is Information Flow Tracking?

Information Flow Tracking (IFT) verifies that sensitive information (sources) never improperly influences observable outputs (sinks). A violation indicates either a confidentiality breach (a secret leaks) or an integrity breach (an attacker-controlled input corrupts state).

IFT can be implemented via two complementary methods:

1. Taint Tracking (TT): Instruments the design with shadow logic that propagates taint bits, dynamically tracking where information flows during execution.
2. Self-Composition (SC): Creates two identical design instances with differing inputs; divergences in outputs reveal information flows.

Both methods detect the same violations but produce cluttered traces. Engineers must currently sift through thousands of signals and cycles to reconstruct the actual flow path, a costly process that consumes nearly half of verification engineers’ time.

Pathfinder and Taint Graphs

Pathfinder tackles this challenge by introducing Temporal Information Flow Graphs (TIFGs) and **Taint Graphs (TGs):

• TIFG: Derived from the RTL design, it encodes all potential information flows, annotated with timing (clock-cycle delays) and control dependencies.
• TG: Constructed by projecting a specific violation trace onto the TIFG, yielding a concrete cycle-accurate flow graph.

This approach isolates only the relevant source-to-sink paths, while also highlighting flow control signals, those capable of blocking the propagation. These control signals point directly to the conditions and logic changes required to eliminate vulnerabilities.

Pathfinder provides both compact views (summarizing multiple cycles) and expanded views (cycle-by-cycle progression), helping engineers understand both iterative loops and intra-cycle combinational flows.

Evaluation

The authors implemented Pathfinder as a Yosys pass for TIFG construction and a Python backend for TG generation.

• Performance: TIFG construction takes under two minutes for large open-source designs; TG generation completes in minutes per trace.
• Search Space Reduction: In case studies, Pathfinder slashed manual inspection effort, e.g., reducing 82,920 tainted signals in CVA6 down to just 1,187 relevant ones (a 769.9× reduction).
• Case Studies:
  • Hardware Trojan (AES): Quickly pinpointed the flow of a secret key into a malicious shift register, revealing the trigger condition.
  • µCFI Violations (Kronos CPU): Identified unintended operand-to-PC flows across multiple cycles, exposing integrity flaws.
  • Temporal Isolation (CVA6): Simplified the analysis of covert-channel violations across fence instructions.
  • Spectre (Boom CPU): Made visible the speculative leakage path through microarchitectural buffers.

Why Pathfinder Matters

Pathfinder represents a significant step toward automated, unified, and scalable analysis of hardware information flow violations. Its contributions include:

• A formal unification of taint tracking and self-composition.
• Taint graphs that explain not only where and when, but also why information propagates.
• A practical tool that reduces debugging effort by up to three orders of magnitude.

By automating root-cause analysis, Pathfinder accelerates the identification and mitigation of hardware vulnerabilities, supporting more secure CPU and SoC designs.

Access and Availability

You can access the Pathfinder publication here.
The tool itself is fully open-source and available here.

This work was supported by the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).