Technical Summary: Augmented Symbolic Execution for Information Flow in Hardware Designs

Problem Statement

Verifying the security of hardware designs requires analyzing how information flows from source signals (inputs) to sink signals (outputs). Unwanted flows can lead to access authorization violations, memory leakage, or privilege escalation. While symbolic execution (SE) is a precise tool for tracking these flows without instrumentation, it suffers from the "path explosion" problem, where the number of execution paths grows exponentially with branch points. Furthermore, hardware designs introduce complexity through multi-clock-cycle reasoning, making it difficult to realize complete flows from input to output. Existing solutions often restrict the design space or analyze only small, critical components.

The core challenge addressed is how to efficiently distinguish between realizable information flows (true paths where data actually moves) and unrealizable paths (static analysis artifacts that cannot occur in execution) within a bounded time frame, while providing concrete input sequences to drive these flows.

Methodology: SEIF

The authors present SEIF (pronounced "safe"), a methodology that augments symbolic execution with static analysis to verify and explicate information flow paths. SEIF operates on a statically built Information Flow (IF) graph, which over-approximates signal connectivity in the Verilog RTL design.

The methodology proceeds in three main phases:

1. Pruning Globally Unrealizable Paths

Before invoking symbolic execution, SEIF analyzes the IF graph to eliminate paths that are logically impossible.

• Segmentation: The IF path is divided into segments based on non-blocking assignments, which denote clock cycle boundaries.
• Constraint Checking: For each segment, the conditions required for the flow to occur are collected. An SMT solver checks for co-satisfiability. If constraints within a single clock cycle segment are mutually contradictory (e.g., a signal must be high and low simultaneously), the path is discarded as globally unrealizable.

2. Guided Symbolic Execution

For the remaining paths, SEIF uses symbolic execution guided by the IF graph to find realizable execution paths through the design state.

• Guided Search: The execution engine is restricted to follow only those design paths that include the specific lines of code required to realize the current IF graph segment. This significantly reduces the search space.
• Clock Cycle Boundary Pruning: At each clock cycle, the engine checks if the current symbolic state satisfies the conditions for the next IF segment. If not, paths leading to that branch are pruned.
• Stalling Strategy: A critical innovation is the ability to "stall" the IF path progression. If the current state cannot satisfy the next segment's conditions, SEIF symbolically executes the design for a clock cycle to advance the machine state without advancing the IF path pointer. Crucially, during stalling, SEIF prevents the symbolic engine from exploring paths that would overwrite information accumulated in prior segments (e.g., preventing a register from being cleared).
• Search Heuristics: The paper evaluates four search strategies:
  1. Baseline 1: Continue or Stall only (exhaustive search of combinations).
  2. Baseline 2: Backtracking only (no stalling).
  3. Stalling with Backtracking: A hybrid approach.
  4. Stalling with UNSAT Core Heuristic: Uses the UNSAT core from the SMT solver to prioritize stall paths that reduce constraint conflicts, effectively guiding the search toward valid next states.

3. Semantic Analysis and Post-Processing

• True Flow Verification: SEIF performs semantic checks to eliminate "false positives" where a textual flow exists but no actual information transfer occurs (e.g., y = x XOR x).
• Reset State Verification: The tool checks if the found execution path is reachable from the design's reset state. If not, it identifies the path as starting from an intermediate state.

Key Contributions

1. Definition of SEIF: A novel methodology combining static analysis (IF graphs) with guided symbolic execution to analyze information flow in hardware.
2. Implementation: A tool implementation built on top of the Sylvia symbolic execution engine and the Hyperflow graph toolchain, utilizing the Z3 solver.
3. Search Heuristics: The development and evaluation of specific search strategies, particularly the use of UNSAT cores to guide stalling, to manage the complexity of multi-clock-cycle path exploration.
4. Evaluation: Comprehensive testing on four open-source designs (OR1200, openMSP430, AKER Access Control, and an AES core).

Results

The evaluation was conducted on a dual-socket server with 12 cores and 62GB RAM.

• Path Accounting: SEIF successfully accounted for 86–90% of the paths in the statically built IF graph. This was achieved by either finding a corresponding realizable design path or proving the path was infeasible.
• True Flows: Of the accounted paths, 58–77% were identified as true information flows, indicating the static IF graph is a strong approximation.
• Performance: SEIF can exhaustively explore paths 10–12 clock cycles deep in an average of 4–6 seconds.
• Search Strategy Efficacy: The UNSAT Core Heuristic outperformed other strategies, finding corresponding design paths 26% more often than baselines and reducing the average search time to 3–6 seconds per path. It also significantly reduced the frequency of backtracking compared to non-heuristic approaches.
• Scalability: In a case study on the MSP430 program counter, SEIF found design paths for 89.93% of 19,060 IF paths within a 16-clock-cycle search horizon.

Significance and Claims

The paper claims that SEIF provides a new angle for security verification by automating the process of distinguishing between static analysis artifacts and actual security violations.

• Precision: It eliminates the need for engineers to manually trace complex multi-cycle flows or guess input sequences.
• Actionability: When a violation is found, SEIF provides a concrete sequence of input values to drive the design along the violating path, starting from either a reset or intermediate state.
• Efficiency: By using the static IF graph to guide symbolic execution, the tool avoids the path explosion problem inherent in pure symbolic execution, allowing for the analysis of deeper clock cycles and larger designs than previously feasible with pure SE.
• Limitations: The authors acknowledge that SEIF targets flaws arising from benign human error in specification and design. It cannot detect flaws introduced by malicious synthesis tools, manufacturing, or supply chain attacks (e.g., analog Trojans) inserted after validation. Additionally, for reconvergent fan-out scenarios, the tool may report incorrect results if it cannot exhaustively explore all design paths.