Overview
Bounded model checking (BMC) is a hardware and software verification technique that limits its analysis to a fixed number of execution steps. Rather than exploring the full reachable state space, BMC checks whether any counterexample to a property exists within a finite bound [arxiv:0710.4629]. In the µArchiFI fault-injection workflow, the BMC bound k is fixed according to the length of the longest program execution trace plus a small safety margin (e.g., a 10-percent increment) to capture possible modifications in the control flow induced by faults [1].
The result of a BMC run can be one of three outcomes: Proven (the assertion is fully proved), Failure (the model checker produces a counterexample), or Undetermined / Bounded Proven (the tool cannot prove or disprove the assertion within the bounded trace or time) [2]. When a counterexample is produced by µArchiFI's external model checker, a VCD file reports precisely where the fault is injected and when the attacker's goal is reached, although understanding the propagation of the fault and its consequences still requires further analysis [3].
How BMC Works
In the hardware setting, BMC works by unrolling a bounded number of circuit steps into one large SMT query. The unrolled query is then passed to an SMT solver, and satisfiability of the query corresponds to the existence of a counterexample within the chosen bound [4]. µArchiFI formalizes this as Algorithm 1 (BMC_Concretizing), which initializes a formula φ with the initial state s₀, then iteratively appends the transition relation φ ← φ ∧ (sᵢ = T(sᵢ₋₁, xᵢ₋₁)) until either the property φ is reached at some step i (in which case a counterexample path is returned) or the bound is reached [8abdfb7e-3ae4-427d-911b-53facf60f5a1, 5560e7ac-6509-44b5-8719-f58282d30fd7].
Because BMC reduces model checking to a sequence of satisfiability problems, the formulation of those problems is typically expressed in SMT-LIB, the standard interchange format for SMT solvers. This makes BMC tightly coupled with advances in SMT solver technology [007d4713-fff9-457f-963a-ee09c3491124, 91532559-482e-4d7c-96dd-390c79237ffc]. For example, the EPEX processor-verification pipeline uses CBMC to translate a C description of an ISA into an SMT-LIB v2.0 instance, which is then handed to Z3 [5]. µArchiFI likewise emits the faulty transition system in SMT-LIB or BTOR2 format for consumption by external model checkers [3].
SAT- and QBF-Based Variants
Classical BMC algorithms encode the unrolled transition relation as a propositional formula and check it with a SAT solver. While effective, this encoding can suffer from a potential memory explosion because the transition relation must be repeatedly unrolled [arxiv:0710.4629]. The µArchiFI paper notes that solving the unrolled formula φ "suffers from the increasing number of variables and clauses" as more transitions are added [6979538c-2d3f-4855-b269-cadc59c83269, 5560e7ac-6509-44b5-8719-f58282d30fd7].
An alternative formulation uses Quantified Boolean Formulae (QBF), which can represent BMC instances more succinctly because it avoids the explicit unrolling of the transition relation. QBF-based BMC has not been as widely adopted, historically because of the lack of efficient general-purpose QBF decision procedures, and specialized decision procedures have been developed to evaluate it on industrial benchmarks [arxiv:0710.4629].
BMC and State-Space Explosion
State-space explosion is an inherent problem of model checking: analyzing an entire system exhaustively is computationally expensive and may be impractical for large systems. BMC is used as an alternative precisely because it can reduce the state space effectively [2]. It is considered an acceptable and popular technique for two main reasons:
- Efficiency: it reduces the state space by examining only a finite prefix of execution traces, rather than exploring the full reachable state space [2].
- Scalability: scaling model checking to large designs remains a challenge, and BMC has been found promising in finding deep vulnerabilities in industrial designs and scales well with size [2].
It might be argued that since BMC cannot cover the whole state space, it cannot guarantee completeness; however, researchers have shown that completeness can be guaranteed with an appropriate threshold, so that an Undetermined result is acceptable in many cases [2]. The µArchiFI paper similarly justifies bounded over unbounded verification for fault-injection analysis because, while unbounded techniques prove the property in the general case, the data dependencies and transient nature of faults make them ill-suited to the fault-injection problem [6].
Tool Support
SymbiYosys is a popular open-source hardware verification front-end that supports several solver backends. Several of its backends, including the built-in Yosys-SMTBMC engine, verify properties using BMC, passing the resulting SMT queries to a backend solver [4]. SymbiYosys also relies on the Yosys synthesis suite, which it shares with other push-button verification systems [7]. µArchiFI's modeling and fault-injection passes are likewise integrated into the Yosys toolchain, and µArchiFI uses the SystemVerilog Assertion subset supported by Yosys to encode the attacker's goal into the hardware design [e850c76e-c937-4c9a-984a-5eb76918c9dc, 6979538c-2d3f-4855-b269-cadc59c83269].
A foundational reference for the technique is Biere's chapter "Bounded Model Checking" in the Handbook of Satisfiability (volume 185 of Frontiers in Artificial Intelligence and Applications, 2009) [7].
CBMC is a model checker for C programs that compiles bounded unwinding of a C program into an SMT-LIB instance suitable for backend solvers such as Z3 [5].
PONO is an SMT-based model checker that µArchiFI invokes as one of several external verification backends on the emitted transition system. In µArchiFI's fault-injection experiments on RISC-V use cases, PONO was reported to be faster than the alternatives on the fault-free model-checking problem of Use Case I and was able to solve fault-injected variants of all three use cases where some other tools timed out [ddff11c6-9d5d-4713-89d7-10cc01ecce93, 6979538c-2d3f-4855-b269-cadc59c83269].
µArchiFI is an open-source tool dedicated to the formal modeling and verification of microarchitecture-level fault injections and their effects on hardware/software systems. µArchiFI models the system under attack as a transition system M_F = (S, S₀, X, T), with S₀ describing possible software execution paths and X controlling the attacker's fault-injection choices, and reduces fault-injection security to a BMC reachability problem with bound k [e850c76e-c937-4c9a-984a-5eb76918c9dc, 8abdfb7e-3ae4-427d-911b-53facf60f5a1]. A path (s₀, …, s_k) in this transition system allows an attacker to identify both the fault-injection instance and the software execution trace that satisfies the attacker goal φ [8].
BMC for SEU Reliability Evaluation
BMC has been applied to evaluate the reliability of hardware against Single Event Upsets (SEUs). In the SEU-evaluation workflow applied to the RISC-V Ibex core, the formal method exhaustively searches the state space and the full fault list for faults that may cause Silent Data Corruptions (SDCs), crashes, or hangs. Compared to fault injection, the advantages of this approach are exhaustive search and backward tracing of faults, while the inherent limitation is state-space explosion, which cannot be avoided in complex designs [9]. The workflow classifies faults according to their effects: faults whose corresponding assertion is Proven are deemed safe SEUs, while faults whose assertion is Failure yield a counterexample and are deemed crucial SEUs (vulnerable bits) [2].
Because BMC only explores a bounded prefix of execution, there is a trade-off between the permitted model-checking time and the number of Undetermined results: with a longer bounded model-checking time, the number of Undetermined results can be minimized, but reducing that number to zero requires an indeterminate amount of time, which is unlikely to be worthwhile [9]. Future work in this line includes extending the method from SEUs to Double Event Upsets and investigating approaches to mitigate state-space explosion [9].
Use Inside Symbolic Quick Error Detection (SQED)
Symbolic Quick Error Detection (SQED), the symbolic pre-silicon form of Quick Error Detection (QED), uses BMC as its underlying engine when checking that two executions of an instruction sequence, fed matching inputs, produce matching outputs [10]. In practice this means performing a single-instruction BMC check for every instruction on the core. SQED imposes practical restrictions on this check, such as splitting the register file in half so that one half holds the original instructions and the other holds the duplicated sequence, which prevents tests from using the full register range [10].
Optimizations and Counterexample Discovery
Because BMC scales with the unrolling bound, a number of techniques have been proposed to reduce the cost of finding counterexamples. One approach adapts ideas from software testing by running BMC in parallel over versions of the system in which features have been randomly disabled. Adding such constraints to the BMC problem can shrink the verification instance and dramatically decrease the time required to find a counterexample; if no counterexample is found, the partial verification results are still useful in practice [arxiv:1610.08020].
The µArchiFI paper introduces two complementary state-space reduction techniques that both add terms and clauses to the unrolled BMC formula:
- Sandboxing restricts the Program Counter (PC) to a range of values that a static analysis (e.g., an
objdump-like tool) can derive from the binary, eliminating software execution paths that cannot occur under fault injection. In µArchiFI, sandboxing is implemented by constraining the PC of the decode stage of in-order processors. Adding such a global constraint, however, may lose the k-completeness of the bounded verification procedure; sandboxing is therefore recommended for vulnerability exploration rather than for proving robustness [8abdfb7e-3ae4-427d-911b-53facf60f5a1, 5560e7ac-6509-44b5-8719-f58282d30fd7, 6979538c-2d3f-4855-b269-cadc59c83269]. - Concretization splits the unrolled formula φ into sub-formulas encoding different software execution paths. µArchiFI's
BMC_Concretizingprocedure (Algorithm 1) first runs BMC up to a concretization depth m, then enumerates possible PC values returned by the SMT solver up to a limit L, running a separate bounded verification for each concretized PC up to bound k. If the PC enumeration is incomplete, the remaining paths are encoded in a single follow-up BMC call [8abdfb7e-3ae4-427d-911b-53facf60f5a1, 5560e7ac-6509-44b5-8719-f58282d30fd7, 6979538c-2d3f-4855-b269-cadc59c83269].
Limitations Inherited From the Encoding
BMC, as implemented in tools such as SymbiYosys, encodes execution directly into the solver query. This makes such implementations less effective than symbolic-execution-based approaches for reasoning across many cycles of execution [4]. Additionally, because BMC only checks a finite bound, it cannot on its own establish unbounded correctness; complementary techniques such as property-directed reachability and k-induction are typically required to extend its guarantees [7]. SQED inherits these scalability considerations, and the EPEX authors observe that formal approaches in general—while able to provide correctness guarantees—are significantly harder to use than simulation-based methods and should be complemented by simulation-based verification [10].
In the fault-injection setting, µArchiFI explicitly justifies choosing bounded over unbounded verification: unbounded techniques prove the property in the general case, but the data dependencies and transient nature of faults make them ill-suited to the fault-injection problem [6]. µArchiFI's experimental evaluation reports that, on the same RISC-V use cases, PONO was generally faster than Yosys-BMC and BTORMC on fault-free verification and was the only solver able to solve fault-injected variants of all three use cases within the time budget, while BTORMC timed out on the fault-injected Use Case II [1]. In the SEU-evaluation setting, state-space explosion is acknowledged as an inherent problem of formal verification and a key limitation when applying BMC to complex designs [9].