Efficient Hardware Information-Flow Tracking for
Pre-Silicon Security Testing

Counterexample-guided abstraction refinement (CEGAR) [24] was originally proposed as a formal verification paradigm for scaling model checking. It reasons about an abstraction of the concrete system and refines it when the abstraction admits spurious counterexamples (cex). In CEGAR-based optimization for taint logic [23], the abstraction is the current taint logic. It starts with imprecise taint logic, checks if a reported cex to the target information-flow property is spurious, and refines the logic to eliminate the spurious one. The main challenge is refinement: eliminating a spurious cex while keeping taint logic lightweight requires deciding where and how to refine.

The where question is intrinsically an optimization problem. The objective is to eliminate the spurious cex with as few refinement sites, i.e., which hardware blocks to refine, as possible. However, refinement decisions are globally coupled: changing the taint logic of one block can alter which taints propagate to downstream blocks and, in sequential designs, across time-frames (i.e., clock-cycles) through state elements. As a result, identifying a minimal set of refinement sites requires reasoning globally about taint propagation and its interaction with candidate refinements.

The how question is equally nontrivial. Even after a refinement site is selected, one must decide how much precision to add to remove the spurious cex without unnecessarily resorting to the most precise and expensive taint logic.

In recent work that has used a CEGAR-based taint-logic optimization [23], these two challenges are handled through heuristic search for where to refine and manual inspection for how to refine. While practical when guided by sufficient design knowledge and understanding of the target property, such refinement relies heavily on human effort, is less systematic, and harder to transfer across new designs and target properties.

The proposed framework, CEGAR-T, tackles the how challenge by first formalizing the well-established notion of precision using NI semantics. This serves as the foundation for defining a partial order over the space of taint logic with different precisions. Such semantic characterization enables systematic strengthening of imprecise taint logic toward a more precise one. Based on this notion, CEGAR-T derives a refinement lattice structure for each block, capturing the space of taint logics between the initial imprecise logic and the fully precise one. As a result, how to refine becomes a problem of navigating this refinement lattice, enabling sound, incremental, and minimal changes to local taint logic over manually chosen updates or full replacement by the most precise and expensive one.

For the where challenge, CEGAR-T formulates the refinement-site selection as a constraint optimization problem using Max-SAT [25]. It encodes how candidate refinements alter taint propagation, capturing the removal of the spurious counterexample (cex) as constraints while minimizing the number of selected refinement sites. This enables global reasoning about interactions among refinement choices, including cases where refining one block can suppress false taints reaching downstream blocks and reduce the need for further updates.

The introduced Max-SAT formulation captures how refinement choices affect taint propagation of the combinational logic within a clock cycle. However, realistic RTL designs are sequential. A cex can be a multi-cycle execution trace, where false taint may propagate across clock cycles through state elements. To handle this temporal behaviour in practice, CEGAR-T provides two refinement algorithms that offer different optimality–scalability tradeoffs. The first Unroll Approach constructs the Max-SAT instance over the whole cex trace by unrolling, which duplicates the combinational logic of the design for the number of cycles in the cex, allowing the solver to reason about the propagation across all cycles. As a result, it computes a minimum-cost refinement for a given cex, but may incur high refinement time overhead due to unrolling as the cex gets longer. The second Single-Frame Approach, in contrast, avoids full unrolling by solving a sequence of simpler refinement problems within a single cycle. This sacrifices exact optimality for a given cex (with little empirical loss in terms of solution quality), but yields a significantly more scalable refinement procedure.

We use $\bar{x}$ for the negation of a variable $x$, $\neg\phi$ for negation of an expression $\phi$, symbols “$\cdot$”, “$+$”, “$\Rightarrow$”, and “$\forall$”, for logical AND, logical OR, implication, and universal quantification (forall), respectively.

An information flow property specifies that sources (secret inputs) must not affect the sink (attacker-observable output) in a design. Intuitively, the sink should never change if we vary sources while holding other non-source inputs (public inputs) unchanged. This is formalized by the non-interference (NI) property [19]. Consider a combinational logic design $y=f(X_{p},X_{s})$ where $y$ is the sink, $X_{s}$ the secret inputs, and $X_{p}$ the public ones. The absence of information flow from $X_{s}$ to $y$ is captured by the NI condition below:

where $X_{s}^{\prime}$ corresponds to a change to the secret inputs. For a sequential design, we reason in terms of input traces and corresponding simulated executions. An input trace $\tau_{K}$ is a time-indexed sequence of input valuations over $k\in[0..K]$. We write $X_{p}(k)$ and $X_{s}(k)$ for the public and secret parts of the input valuation at time $k$ in $\tau$. Evaluating the design on $\tau_{K}$ induces a unique execution, which determines the valuations of all signals over time. We refer to this induced sequence of valuations as the full trace of the design under $\tau_{K}$. We denote the valuation of the sink in the full trace at time $k$ by $y_{\text{sink}}(k)$. NI requires that for all $K$ and for any two input traces $(\tau_{K},\tau^{\prime}_{K})$ whose public inputs agree at every time step, the sinks are identical at the last time step:

where $y_{\text{sink}}(k)$ (resp., $y_{\text{sink}}^{\prime}(k)$) is obtained by evaluating the design on $\tau_{K}$ (resp., $\tau^{\prime}_{K}$). If Eq. (2) is violated, then there is a $K$ and two input traces $\tau_{K},\tau^{\prime}_{K}$ such that $X_{p}(k)=X_{p}^{\prime}(k)$ for all $k\leq K$, but $y_{\text{sink}}(K)\neq y_{\text{sink}}^{\prime}(K)$. The input traces serve as the cex to the property.

A standard way to check NI is via self-composition [30] following Eq. (1) and Eq. (2). This approach builds a self-composed design consisting of two copies of the original design, constrain their public inputs to be equal while leaving their secret inputs unconstrained, and assert equality of sinks across the two copies. For combinational logic, self-composition corresponds to Eq. (1), whose violation can be checked via a SAT query over $(X_{p},X_{s},X_{s}^{\prime})$. For sequential logic, self-composition yields a safety property [30] in Eq. (2), whose violation can be checked by a model checker.

Taint analysis is an alternative way to check the NI property that avoids the two-copy self-composition. Instead, it instruments a single copy of the design with additional taint bits and taint logic, and then checks whether taint from the sources can reach the taint at the sink along an execution.

Taint analysis associates each signal $x$ with a taint bit $x^{t}$ indicating if there may be a flow from sources to $x$. For a combinational block $y=f(X)$, a taint logic $f^{t}$ computes the output taint $y^{t}$ from the input values and input taints:

For a sequential design, sequential state elements such as D-flip flops (DFFs) propagate taint across cycles (e.g., $q^{t}(k{+}1)=d^{t}(k)$, where $q$ and $d$ are the DFF output and input, respectively), and taint is propagated through combinational logic in each cycle with Eq. (3). NI of both combinational and sequential cases is soundly approximated by checking if the sink could ever be tainted assuming sources are tainted ($X_{s}^{t}=\mathbf{1}$) and non-source inputs are untainted ($X_{p}^{t}=\mathbf{0}$).

Design-level taint logic is constructed compositionally: each primitive block $f$ is assigned a taint logic $f^{t}$ (e.g., gates [12], RTL operators [13], or cells [6]), and composed according to the design connectivity. As a result, the sink taint is determined by the interaction of many local taint logics along the fanin cone of the sink and across cycles.

Taint analysis is designed to be a sound overapproximation with respect to the NI semantics in Eq. (1) and Eq. (2). In particular, if there exists an information-flow witness in the sense of NI, i.e., two executions that agree on all public inputs but differ at the sink—then, when we label only the sources as tainted, executing the design under any one of the two input traces must taint the sink in the taint logic. However, the converse need not hold: the sink can become tainted even when no such paired execution exists, leading to spurious information flows.

(Weighted) maximum satisfiability [32] (Max-SAT) extends SAT with an optimization objective. We use the following Max-SAT formulation (one of several equivalent ones [32]) as it aligns with our subsequent discussion and is supported by the solvers [33, 34, 35, 36, 37, 38]. Given a set of Boolean constraints $\Phi$ over variables $V$, Max-SAT searches for an assignment that satisfies $\Phi$ while minimizing (or maximizing) a user-specified cost. The cost is expressed as an objective over a subset of variables as a weighted sum. We use the following notation for a Max-SAT query with constraint set $\Phi$ and objective $\min\sum_{i}w_{i}\cdot v_{i}$ with $v_{i}\in V$ a Boolean variable and $w_{i}\geq 0$ its weight (the unweighted case sets $w_{i}=1$):

There exists efficient Max-SAT solvers that scale to large instances [33, 34, 35, 36, 37]. More generally, optimization modulo theories (OMT) solvers such as Z3’s optimizing engine also support Max-SAT-style objectives with logical constraints over non-Boolean variables [38].

We assume DFFs are the only sequential blocks in designs. Since they simply propagate taint across clock cycles and cannot be refined, we focus on combinational blocks.

Let $X=(x_{1},\ldots,x_{n})$ be the inputs, $y=f(X)$ the output, and $y^{t}=f^{t}(X,X^{t})$ the taint logic of a block $f$.

A taint assignment $\tau^{t}\in\{0,1\}^{n}$ to $X^{t}$ partitions the inputs into the public inputs $X_{p}$ and the secret inputs $X_{s}$:

As a reminder, this partition may change because it depends on how the hardware block is embedded within the larger design. For the same block, we may see different partitions in different cex or time frames. We write the taint logic $f^{t}$ under the taint assignment $\tau^{t}$ as

When fixing a taint assignment $\tau^{t}$, following the NI semantics in Section III, a taint logic $y^{t}=f^{t}_{\tau^{t}}(X_{p},X_{s})$ is precise iff $y^{t}=1$ exactly when there is a flow from $X_{s}$ to $y$. That is, there exists $X_{s}^{\prime}$ such that $f(X_{p},X_{s})\neq f(X_{p},X_{s}^{\prime})$ with $X_{p}$ fixed, as captured by the predicate $\hat{f}^{t}_{\tau^{t}}$:

Given a taint logic $f^{t}$, we can now reason about its precision for a specific taint-assignment $\tau^{t}$. We say $f^{t}$ is precise under $\tau^{t}$ if $f^{t}_{\tau^{t}}$ is equivalent to $\hat{f}^{t}_{\tau^{t}}$.

The above concept of per-assignment precision guides us to make assignment-specific refinement in Section V-B and to further derive our refinement lattice in Section V-C. Additionally, we give the definition of precise taint logic that is agnostic to taint assignments.

We next explain how to refine a taint logic $f^{t}$ to remove a spurious cex in which $f^{t}$ over-taints.

Let’s consider a motivating example of a 3-input AND cell $y=a\cdot b\cdot c$ with the most imprecise taint logic

Suppose we observe a cex assignment with $\tau^{t}=(1,0,0)$ and $\tau=(1,0,1)$, under which taint should not propagate to the output, but the current taint logic nevertheless sets $y^{t}=1$. We describe three versions of refinement to demonstrate the benefit of making assignment-specific refinements.

First, a naive refinement would block exactly this single valuation by conjoining a constraint that excludes it:

However, this refinement is overly specific: it eliminates only the particular cex and may still admit many other assignments that share the same taint assignment $\tau^{t}=(1,0,0)$ and are equally spurious. For example, under the same $\tau^{t}=(1,0,0)$, $(a,b,c)=(0,0,1)$ and $(1,0,0)$ should also yield $y^{t}=0$ because $b=0$ or $c=0$ blocks the secret $a$, yet $f^{t}_{0}$ over-taints these cases as well.

Second, at the other extreme, we could replace $f^{t}_{0}$ with $\tilde{f}^{t}$, thereby eliminating all spurious over-tainting for this cell. While effective, this can be unnecessarily expensive when $\tilde{f}^{t}$ contains terms that are irrelevant under the design’s reachable behaviors, e.g., the don’t-care values in the design.

Lastly, we seek a refinement that generalizes from the cex to capture the blocking condition over the public inputs, which characterizes the public input values that block the taints for $f^{t}$ and the given $\tau^{t}$.

Under $\tau^{t}=(1,0,0)$, the secret is $X_{s}=\{a\}$ and the public inputs are $X_{p}=\{b,c\}$. For $y=a\cdot b\cdot c$, the secret can influence $y$ iff $b\cdot c=1$; equivalently, $(\bar{b}+\bar{c})$ blocks taint propagation. Thus, a just-enough refinement, that lies in between the two ends above, strengthens $f^{t}_{0}$ by ruling out taint propagation whenever $(\bar{b}^{t}\cdot\bar{c}^{t}\cdot(\bar{b}+\bar{c}))$ holds:

As a result, this refinement eliminates a set of generalized cex, the original cex and a family of cex that share the same taint assignment $\tau^{t}=(1,0,0)$, using a simpler taint logic compared with $\tilde{f}^{t}$. This potentially avoids generating cex from the same family, thus reducing the number of iterations in the CEGAR-T loop.

We now formalize the space of candidate taint logics by viewing each application of Eq (9) as a refinement step to a more precise taint logic.

Not every taint observed in the current taint logic can (or should) be eliminated by refinement. In fact, any taint seen by the precise reference model must be preserved. Refinement should only address blocks whose output is tainted in the current model but untainted in the reference model, i.e., the output is falsely tainted. Therefore, before formulating the Max-SAT instance, we identify combinational blocks with false taints under the current taint logic. We refer to this set of blocks as a refinement candidate set.

Given the cex trace, we perform two taint simulations on the unrolled design: (i) the current taint simulation using the current block taint logic $f^{t}$, and (ii) the reference taint simulation using the precise reference model. For each combinational block $f$ and timeframe $k$, let $Y^{t}(f,k)$ and $\tilde{Y}^{t}(f,k)$ denote the taint value of $f$’s output under the two simulations, respectively. We add $f$ to the refinement candidate set $\mathcal{C}$ if it is falsely tainted in at least one timeframe:

Only blocks in $\mathcal{C}$ are eligible to be refined for this cex. Conceptually, $\mathcal{C}$ excludes blocks whose taint outputs already agree with the reference model, so refining them would not help eliminate any over-tainting observed on this cex.

For each refinement candidate block $f\in\mathcal{C}$, we use the variable $r_{f}$ indicating whether we apply refinement to $f^{t}$ for the current cex. A first attempt is to gate away the false taint by a mux: if $r_{f}=1$ we force the block’s output taint to $0$, otherwise we keep the original output taint computed by the current taint logic $f^{t}$. However, this construction is not sound: it may suppress output taint even when the current taint logic already matches the precise reference model.

The key subtlety is that the input-taint assignment seen by $f^{t}$ depends on the taints of its upstream fanin logic. Since some fanin taints may be falsely tainted and eliminated by refining upstream blocks, the input taints $X^{t}$ arriving at $f^{t}$ can change depending on upstream refinements. Thus, whether the false taint at $f^{t}$ can be eliminated by refinement must be based on the input-taint $\tau^{t}$ assignment reaching $f^{t}$, referred to as the incoming input-taint assignment, together with the input assignment $\tau$ from the cex.

To capture this dependency, we construct an enabling condition $S_{f}(X^{t})$ over the input taint bits $X^{t}$. Let $\tau$ be the assignment to $X$ given by the cex. We define $S_{f}$ to describe when $f^{t}$ is falsely tainted on the cex under the incoming input-taint assignment:

Intuitively, $S_{f}(X^{t})=1$ means that, under $\tau$ and the seen $X^{t}$, the output taint produced by $f^{t}$ disagrees with the precise reference model, and hence is imprecise and eligible to be fixed by refinement. When $S_{f}(X^{t})=0$, the current taint logic already matches the reference model, and we should not allow refinement to change the output taint.

We then guard refinement by $S_{f}$ so that the refinement is enabled only when (i) the solver chooses $r_{f}=1$ and (ii) the incoming input-taint assignment makes $f^{t}$ falsely tainted. Concretely, letting $y^{t}$ be the output taint of $f$, we enforce

This ensures that a block’s output taint can be suppressed only in cases where it is falsely tainted on the cex under the incoming input-taint assignment reaching the block.

With (i) the refinement candidate set, (ii) the guarded mux construction for candidates, and (iii) the refinement operator, we now present the end-to-end procedures for eliminating a spurious cex on a general sequential design.

We evaluate CEGAR-T using the random safe-instruction testbench with $(N,B)=(20,60K)$. The parameters are chosen empirically to provide sufficient opportunities to expose spurious cex and drive refinement. We set a 12-hour timeout for each run.

Figure 5 shows the runtime breakdown of the refinement process into cex generation (Cex-Gen), Max-SAT solving (Max-SAT), and other tasks (Others). The Unroll results of Medium, Large, and Mega BOOM time out and are omitted. Bar labels (# iters, # fixes) denote the number of iterations and refined cells; e.g., (19, 751) for Mega-BOOM Frame.

Frame scales across all evaluated cores, whereas Unroll handles the in-order cores and Small-BOOM but fails to scale to the larger BOOM variants. This gap is due to the higher Max-SAT cost for the fully unrolled design. For Unroll, Max-SAT grows substantially with core complexity and becomes a major runtime bottleneck. For Frame, runtime is dominated by Cex-Gen and Max-SAT remains a small fraction of the total, showing its effectiveness. The (# iters, # fixes) labels further illustrate the tradeoff between the two refinement algorithms. Unroll consistently requires fewer refined cells than Frame, consistent with its global optimization over the full unrolled trace. In contrast, Frame often needs fewer refinement iterations, likely because refining falsely tainted DFFs early in the trace can suppress false taint propagation in later cycles and eliminate additional spurious counterexamples at once. Together, these results suggest that Frame is the practical scalable choice for refinement, while Unroll can provide stronger per-cex optimization for cases where it does not time out.

We compare the optimized taint logic against both the original bit-level (CellIFT-B) and word-level (CellIFT-W) precise CellIFT baseline. We implemented CellIFT-W as the corresponding precise word-level taint logic without CEGAR-T optimization to enable a fair-comparison with CEGAR-T which introduces taint logic at the word level. To quantify the taint logic reduction achieved, we measure both cell count and gate count after lowering the taint-instrumented design to gate level. Cell count reflects design complexity and correlates with RTL simulation overhead, whereas gate count approximates the cost of physical implementation of the taint logic (e.g., in hardware emulation). Figure 6 reports the cell-count overhead normalized to the original design without taint logic. The gate-count results are similar and are shown in Figure 7. Across both metrics, Unroll and Frame yield substantially smaller taint-logic overhead than both CellIFT-B and CellIFT-W.

We next evaluate the end-to-end simulation runtime of the taint logic produced by the Refinement Phase. In the Fast-Simulation Phase, we use the same workload with $(N,B)=(50,200K)$ to stress the taint logic under substantially larger validation runs. In addition to CellIFT-B and CellIFT-W, we include a baseline (No-Refine) that directly uses the initial imprecise taint logic without refinement. The CellIFT-W baseline isolates the effect of optimized taint logic on raw simulation runtime, whereas No-Refine isolates the cost of low precision in end-to-end validation, where tainted traces incur spuriousness-check overhead.