Source-linked AI summary
Efficient Hardware Information-Flow Tracking for Pre-Silicon Security Testing
Yu-Wei Fan, Yuheng Yang, Christine Guo, SooHyuk Cho, Thomas Bourgeat, Mengjia Yan, Sharad Malik
TL;DR
Taint-based information-flow tracking can make pre-silicon security simulation costly, while less precise logic risks false positives. CEGAR-T automatically refines taint logic, reducing instrumentation and simulation overhead across evaluated cores while retaining the CellIFT precision benefit.
Problem
The paper asks how taint logic can be made lightweight for simulation without sacrificing the precision needed to avoid false positives.
Source: §1 · p. 2Method
CEGAR-T formalizes taint precision using non-interference semantics and uses a refinement lattice and Max-SAT to automate where and how taint logic is refined.
Source: §1 · p. 2Results
Across evaluated cores, instrumentation overhead falls from 5.64× to 1.42× and simulation-time overhead from 34.65× to 1.79×, without compromising CellIFT’s precision benefit.
Source: §1 · p. 2Takeaways & Limitations
On the evaluated safe instruction set problem, automated taint-logic refinement reduces both instrumentation and simulation overhead while retaining the CellIFT precision benefit.
Source: §1 · p. 2The word-level approach has irreducible granularity imprecision that can leave spurious counterexamples in patterns such as packed fields, masking, and bitslicing.
Source: §10 · p. 13
Abstract
from arXiv · showhide
Register-Transfer Level (RTL) simulation is widely used to test hardware before it is fabricated. To allow testing for security related information flow properties, such as confidentiality and integrity, taint logic can be automatically added to the design to track how information flows through it. However, taint logic instrumented by the state-of-the-art, such as CellIFT, makes simulation-based testing prohibitively expensive: On our evaluation of Mega-BOOM (136K cells), it increases the instrumented design to 5.81x the original cell count and causes a 143.72x simulation slowdown. The taint logic could be simplified to improve simulation speed, but it will inevitably trade off its precision. This lightweight, imprecise taint logic will introduce false positives and may eventually result in even more overhead to check these false positives. This paper explores the research question of where precision is actually needed in the design to overcome the overhead of false positives. It presents CEGAR-T, a framework that automatically synthesizes taint logic that minimizes the taint-logic instrumentation overhead while guaranteeing no false positives (relative to the precise CellIFT baseline). We have implemented CEGAR-T and evaluated it on the safe instruction set problem for timing side-channel security across open-source RISC-V cores. Over all evaluated cores, CEGAR-T reduces both instrumentation and simulation overhead, in geometric-mean, from 5.64x to 1.42x and from 34.65x to 1.79x, respectively, without compromising the precision benefit of the CellIFT baseline.
1. Introduction
Simulation-based taint tracking supports pre-silicon security testing, but precise logic can impose high overhead and imprecise logic can generate false positives. CEGAR-T automates refinement of where and how taint logic is made more precise.
1. Introduction
- Precise taint logic can make simulation prohibitively expensive, while imprecise logic tends to over-taint and generate false positives.On Mega-BOOM (136K cells), CellIFT increases design size to 5.81× and causes a 143.72× simulation slowdown.Source: §1 · p. 1
2.2. CEGAR-T: A Fully Automated Framework for Taint-Logic Optimization
- CEGAR-T formalizes taint precision using non-interference semantics and uses a refinement lattice and Max-SAT to automate how and where taint logic is refined.The framework selects local refinements sufficient to eliminate successive spurious counterexamples.Source: §1 · p. 2
1. Introduction
- Across evaluated cores, CEGAR-T reduces instrumentation-size overhead from 5.64× to 1.42× and simulation-time overhead from 34.65× to 1.79×, without compromising the precision benefit of the CellIFT baseline.These are geometric-mean comparisons for CEGAR-T evaluated on simulation-based IFT of SISP.Source: §1 · p. 2
2.1. Challenges in CEGAR-Based Optimization
- CEGAR-based taint optimization must resolve globally coupled choices about where to refine and how much precision to add, challenges prior work handled with heuristic search and manual inspection.Those choices can affect downstream taint propagation and propagation across sequential time frames.Source: §2.1 · p. 2
2.2. CEGAR-T: A Fully Automated Framework for Taint-Logic Optimization
- For sequential designs, Unroll finds a minimum-cost refinement for a counterexample trace but can be costly at longer bounds; Single-Frame scales better with little empirical loss in solution quality.Single-Frame sacrifices exact optimality for a given counterexample by solving simpler, single-cycle refinement problems.Source: §2.2 · p. 3
3. Background
The background defines information-flow security through non-interference and describes taint analysis as a sound, compositional approximation for checking it. It also distinguishes local from correlation-based imprecision and introduces Max-SAT as an optimization framework.
3.2. Information Flow Property
- Non-interference requires that changing secret inputs while holding public inputs equal cannot change the sink; sequential designs compare traces with matching public inputs at every time step.The property is checked by comparing sink values at the final time step of the traces.Source: §3.2 · p. 3
3.3. Hardware IFT with Taint Analysis
- Taint analysis instruments one design copy with taint bits and propagates taint through combinational logic and sequential state to approximate non-interference.The design-level taint logic is composed from local block logics along the sink’s fan-in and across cycles.Source: §3.3 · p. 4
Scope of Refinement
- Taint logic soundly over-approximates information flow, but can mark a sink tainted even when no non-interference witness exists; imprecision may be local or correlation-based.This work focuses on eliminating local imprecision and leaves correlation-based imprecision for future work.Source: §3.3 · p. 4, Scope of Refinement · p. 4
3.4. Maximum Satisfiability (Max-SAT)
- Max-SAT searches for a Boolean assignment satisfying constraints while minimizing or maximizing a weighted-sum objective over selected variables.The unweighted case assigns each objective variable a weight of 1.Source: §3.4 · p. 4
4. Spuriousness Check
A counterexample under imprecise taint logic may be spurious, so the framework checks whether it reflects a real non-interference violation. It combines a cheaper, incomplete taint simulation check with a more expensive, complete SAT check.
4. Spuriousness Check
- Precise taint simulation re-evaluates the counterexample with a precise reference logic; an untainted sink identifies a spurious counterexample.This check is sound and more efficient, but incomplete because it does not account for correlation-based imprecision.Source: §4 · p. 4
- The SAT check fixes one execution to the counterexample, constrains public inputs equal in the other, and asks whether another trace can change the sink.It checks the two-trace non-interference condition on an unrolled self-composed design; unsatisfiability means the counterexample is spurious.Source: §4 · p. 4
- The workflow runs precise taint simulation first and invokes SAT only if that check leaves the sink tainted.SAT is complete for spuriousness checking but generally more expensive.Source: §4 · p. 4
5. Precision and Refinement of Taint Logic
Section 5 defines taint-logic precision relative to non-interference semantics and develops assignment-specific refinements that move from an imprecise logic toward a precise one. Its refinement lattice supports targeted refinement instead of requiring precision under every input value.
5. Precision and Refinement of Taint Logic
- The refinement lattice enables minimum refinement for a given spurious counterexample, unlike constructions that force precision under all possible input values.Source: §5 · p. 5
5.1. Formalizing Per-assignment Precision
- Under a fixed taint assignment, taint logic is precise exactly when its output taint indicates whether secret inputs can influence the output.Source: §5.1 · p. 5
5.2. Counterexample-Guided Precision Refinement
- A blocking-condition refinement generalizes one spurious counterexample across its taint-assignment family, potentially reducing repeated CEGAR-T iterations.Source: §5.2 · p. 6
5.3. Refinement Lattice
- For a 3-input AND, the lattice contains 64 nodes versus 8 variants in prior work, and subsumes those variants.Source: §5.3 · p. 6
- Refinement steps commute, so multiple assignment-specific refinements can be applied in any order.Source: §5.3 · p. 6
6. Max-SAT for Optimum Refinement
Section 6 selects refinement sites by formulating counterexample elimination as a Max-SAT optimization. It identifies falsely tainted blocks, guards refinements against incoming taint assignments, and describes unrolled and single-frame procedures for sequential designs.
6. Max-SAT for Optimum Refinement
- Max-SAT selects the fewest combinational blocks to refine while making the sink untainted on the counterexample; block count serves as a proxy for instrumentation complexity.Source: §6 · p. 7
6.1. Identifying Refinement Candidate Set
- Candidates are blocks tainted by the current logic but untainted by the precise reference in at least one frame, excluding refinements that cannot remove observed over-tainting.Source: §6.1 · p. 7
6.2. Circuit Construction for Refinement Candidates
- The guarded construction suppresses a block’s output taint only when it is falsely tainted under the incoming input-taint assignment, which upstream refinements can change.Source: §6.2 · p. 8
6.3. Overall Algorithm
- The end-to-end sequential-design procedure combines candidate detection, guarded candidate constraints, and the refinement operator to eliminate a spurious counterexample.Source: §6.3 · p. 8
6.3.1. Unroll Approach.
- The unroll approach builds one Max-SAT instance across frames, enforces an untainted final sink, then batch-refines selected blocks at active input-taint assignments.Source: §6.3.1 · pp. 8–9
6.3.2. Single-Frame Approach.
- Single-frame refinement solves smaller per-timeframe Max-SAT instances and is typically more scalable, but may select a non-minimal refinement set.Source: §6.3.2 · pp. 9–10
7. Implementation
The implementation uses word-level CellIFT instrumentation and makes CEGAR-T refinement practical through small, precomputed lattices for supported cells. The section also points to the two-phase IFT workflow.
7. Implementation
- Word-level CellIFT assigns one taint bit to each multi-bit word, whereas bit-level CellIFT assigns one taint bit to each data bit.A word is tainted if at least one of its bits is tainted; this granularity reduces taint variables and instrumented logic size.Source: §7 · p. 10
- For supported cells, word-level taint bounds the largest refinement lattice to eight nodes, making explicit lattice construction and lightweight online refinement practical.The supported cell library has at most three input words per cell; a mux is given as an example.Source: §7 · p. 10
- CEGAR-T is implemented in C++ using Yosys for Verilog and RTLIL processing and Z3’s optimization engine to solve Max-SAT instances.Figure 4 depicts two-phase simulation-based IFT, which terminates upon detecting true leakage or exhausting the tests.Source: §7 · p. 10, Figure 4 · p. 10
8. CEGAR-T-based Simulation Worflow
The workflow first refines taint logic in response to spurious counterexamples, then fixes the refined logic for high-throughput simulation. It uses different simulators to suit the compilation and throughput needs of each phase.
8. CEGAR-T-based Simulation Worflow
- In the Refinement Phase, each detected spurious counterexample triggers taint-logic refinement to eliminate a class of similar false positives.Spurious counterexamples are expected to be frequent at this stage.Source: §8 · p. 10
- Once spurious counterexamples are relatively rare and their checking overhead negligible, the workflow switches to Fast-Simulation with the refined taint logic fixed.Remaining spurious counterexamples are checked and reported but do not trigger refinements that could slow simulation throughput.Source: §8 · pp. 10–11
- Icarus Verilog is used during refinement to limit compilation time, while Verilator is used for higher-throughput Fast-Simulation despite greater compilation overhead.A taint-logic change requires recompilation.Source: §8 · p. 11
9. Evaluation
The evaluation tests CEGAR-T on safe-instruction SISP across open-source RISC-V cores, comparing taint-logic size, simulation slowdown, precision, and refinement behavior. Frame scales across the evaluated cores, while the Small-BOOM case study shows how refinements target MUX selection logic and identifies a limitation of Frame.
9. Evaluation
- The evaluation models register-file data as the source and instruction commit as a timing proxy sink, assuming only safe instructions execute, and uses generated safe-instruction tests.It covers Ibex, Rocket, and four BOOM configurations; unsafe-instruction runs terminate upon detecting true leakage, so reported experiments focus on safe instructions.Source: §9 · p. 11
9.1. Runtime and Taint Logic Reduction Analysis
- 1.42x (Frame) and 1.31x (Unroll) are the geometric-mean cell-count overhead ratios, versus 5.64x (CellIFT-B) and 4.99x (CellIFT-W).Cell count is normalized to the original design without taint logic.Source: Figure 6 · p. 11, §9.1 · p. 12
- Frame scales across all evaluated cores, while Unroll times out on Medium, Large, and Mega BOOM as full-trace Max-SAT cost grows; Frame runtime is dominated by counterexample generation.The Unroll timeouts are omitted from Figure 5.Source: §9.1 · p. 11, Figure 5 · p. 11
- 1.04x (Frame) and 1.03x (Unroll) are the geometric-mean gate-count overhead ratios, versus 3.77x (CellIFT-B) and 1.80x (CellIFT-W).Gate count approximates taint-logic physical implementation cost, such as for hardware emulation.Source: Figure 7 · p. 12, §9.1 · p. 12
9.2. Downstream Simulation-based IFT
- 1.79x (Frame) and 1.60x (Unroll) are the geometric-mean simulation slowdown ratios, versus 34.65x (CellIFT-B), 6.16x (CellIFT-W), and 67.17x (No-Refine).Slowdown is normalized to the original design; Unroll results are reported only for cores where refinement completes.Source: Figure 8 · p. 12, §9.2 · p. 12
- Frame reports at most two tainted counterexamples and Unroll at most three, while both precise CellIFT baselines report zero; no true counterexamples occur in the evaluated tests.Thus all evaluated cores satisfy SISP for these tests.Source: §9.2 · p. 12
9.3. Refinement Analysis: A Case Study
- In Small-BOOM, most refinements target MUXes to stop taint from unselected paths, making taint propagation path-sensitive around register reads, control/datapath choices, and data-array reads.MUX trees can require many fixes because imprecise taint can spread through internal muxes at multiple levels.Source: §9.3 · pp. 12–13
- Frame can refine falsely tainted DFFs that do not functionally affect instruction commit; cone-of-influence reduction is suggested to focus refinements on sink-influencing DFFs.Small-BOOM debug-related states and memories are examples of such irrelevant states.Source: §9.3 · p. 13
10. Discussion
CEGAR-T’s refinements are optimal only within the scope of each approach, not globally across all counterexamples. Word-level taint tracking keeps taint-logic size and optimization time manageable but retains irreducible imprecision.
10. Discussion
- Neither Unroll nor Frame guarantees a globally minimal refinement across all counterexamples.A global optimum would require one Max-SAT instance encoding all observed counterexamples, which may be computationally prohibitive, especially for large K.Source: §10 · p. 13
- Word-level tracking can spuriously propagate taint through packed fields, masking, or bitslicing because taint on any bit taints the whole word.Some spurious counterexamples may arise only from this coarse granularity; the evaluation did not encounter them.Source: §10 · p. 13
11. Related Work
Prior hardware IFT work includes self-composition, taint analysis at different abstraction levels, and hybrid approaches. The paper targets SISP through simulation-based IFT, unlike self-composition-based formal verification, and uses Max-SAT for taint refinement rather than bug localization.
11. Related Work
- Prior hardware IFT work has explored self-composition, taint analysis at different abstraction levels, and hybrid approaches combining both; taint-analysis optimization work is cited as,,, and.Source: §11 · p. 13
Secure Processor Verification Frameworks
- For secure speculation, contract-based properties are outside this evaluation because they cannot be expressed as a single source-to-sink information-flow property.Prior constant-time SISP work uses self-composition and invariant synthesis, whereas this work evaluates simulation-based IFT.Source: Secure Processor Verification Frameworks · p. 13
- Max-SAT selects minimum-cost taint-logic refinements that eliminate spurious information-flow counterexamples, rather than localizing functional bugs.Prior VLSI debugging and diagnosis use it to select suspect fault sites,,.Source: Secure Processor Verification Frameworks · p. 13
12. Conclusion
CEGAR-T automates property-driven taint-logic optimization by formalizing precision with non-interference semantics and structuring refinements. Its evaluation reports reduced taint-logic overhead and faster simulation-based IFT.
12. Conclusion
- CEGAR-T formalizes taint-logic precision with non-interference semantics and characterizes refinements through a lattice-like structure.Its automated procedure optimizes how to refine via the refinement lattice and where to refine via Max-SAT.Source: §12 · pp. 13–14
- CEGAR-T introduces Unroll and Single-Frame refinement algorithms with different optimality–scalability tradeoffs.Unroll and Frame reduce taint-logic overhead by 91.32%/89.88% compared to bit-level CellIFT and its word-level variant, and achieve up to 19.35×/3.44× corresponding speedups in simulation-based IFT.Source: §12 · p. 14
- The authors conclude that reducing simulation overhead advances the scalability of taint-based security verification and opens the door for full industrial adoption.Source: §12 · p. 14
Appendix A. Additional Figures and Tables for Evaluation
Validation tests report few spurious counterexamples for both refinement approaches. Refinements are concentrated early in the test sequence, with occasional later updates across representative BOOM configurations.
Appendix A. Additional Figures and Tables for Evaluation
- Frame reports at most two tainted counterexamples and Unroll at most three out of 200K validation tests on the evaluated cores.The authors interpret this as evidence of high empirical precision for the synthesized lightweight taint logic.Source: Table 1 · p. 16, Appendix A · p. 16
- Across Medium, Large, and Mega BOOM, most refinements occur in the first 3000-test bucket, followed by a sharp drop and a sparse long tail.The bucket ID follows the sequence of sequentially simulated tests; similar behavior was observed on other evaluated cores.Source: Appendix A · p. 16, Figure 9 · p. 16