SecIC3: Customizing IC3 for Hardware Security Verification

TL;DR

SecIC3 tailors the IC3 model checking approach to non-interference verification by exploiting the symmetry inherent in self-composed hardware designs. It introduces two main innovations: symmetric state exploration and equivalence predicates, including word-level inequivalence predicates and a Predicate_replace mechanism with three heuristics, to accelerate lemma learning and state-space reduction. Implemented on ABC-PDR and rIC3, SecIC3 demonstrates substantial speedups over baselines (up to 49.3x) across a 10-design benchmark designed for hardware information-flow verification, with a representative average improvement around 16.5x. The work provides practical impact for scalable hardware security verification and contributes a benchmark suite and open-source tooling to the community.

Abstract

Recent years have seen significant advances in using formal verification to check hardware security properties. Of particular practical interest are checking confidentiality and integrity of secrets, by checking that there is no information flow between the secrets and observable outputs. A standard method for checking information flow is to translate the corresponding non-interference hyperproperty into a safety property on a self-composition of the design, which has two copies of the design composed together. Although prior efforts have aimed to reduce the size of the self-composed design, there are no state-of-the-art model checkers that exploit their special structure for hardware security verification. In this paper, we propose SecIC3, a hardware model checking algorithm based on IC3 that is customized to exploit this self-composition structure. SecIC3 utilizes this structure in two complementary techniques: symmetric state exploration and adding equivalence predicates. We implement SecIC3 on top of two open-source IC3 implementations and evaluate it on a non-interference checking benchmark consisting of 10 designs. The experiment results show that SecIC3 significantly reduces the time for finding security proofs, with up to 49.3x proof speedup compared to baseline implementations.

Figures (6)

• Figure 1: Non-Interference Checking via Self-Composition.
• Figure 2: The frames of an IC3 inductive trace when checking a property $P$. IC3 refines frames by blocking bad states: the state is shown to be part of an unreachable cube $c$, and is thereby excluded from the latest frame $F_n' = F_n \wedge \neg c$.
• Figure 3: IC3 Example on Checking Non-Interference
• Figure 4: Equivalence Predicate Construction
• Figure 5: A lattice (partial order) of possible predicate replacements given the cube at the bottom of the lattice.