Attacker Model

In the µARCHIFI formal verification framework for microarchitectural fault injection, the attacker model is the formal abstraction used to characterize how an adversary can perturb a system under attack through fault injection. It is an input to µARCHIFI alongside a hardware description (Verilog) and a binary software program, and it drives the construction of a faulty transition system on which bounded model checking (BMC) is performed.

Definition

The attacker model consists of three components:

1. The attacker's goal, expressed as a reachability property φ defined on the system's transition system. The goal represents a vulnerability that the attacker wants to reach in order to create an exploit on the system by injecting faults. In normal (fault-free) operation, the exploit should not exist, i.e., ¬φ is a system invariant that the attacker aims to break.
2. The number of faults N that the attacker is allowed to inject into the system. This capacity is enforced during verification by a counter cnt ∈ [[0, N]] that is incremented on each faulty transition.
3. The fault model, a triplet (L, T, E) describing the possible modifications a fault may induce:
   • L — the set of possible locations of the fault, denoting the registers targeted by the fault injection, with L ⊆ {r1, …, rn}. Each targeted register rl ∈ L has an associated input xl controlling whether a fault is applied.
   • T — the timing range of the fault injection, a set of non-negative integers specifying when the fault may occur (a fault can be injected between states si and si+1 if i ∈ T).
   • E — the set of possible effects of the fault, i.e., functions that modify how a register is updated in the next state. For a register rj and effect e ∈ E, the normal transition function δrj is replaced by a faulty transition δej producing the same output data type. Non-exhaustive example effects include set, reset, and flips (e.g., bit-flip, bit-reset) on an 8-bit register.

Integration into the Faulty Transition System

The attacker model is incorporated into a faulty transition system MF = (S, S0, X, T) derived from the hardware transition system M = (S, S0, X, T). For each register rl ∈ L, an additional input xl is introduced so that the next-state value is:

• δrl(s) if xl = False (normal operation), or
• δel(s) if xl = True (faulty transition).

The verification problem is then a reachability property verification: find a sequence of states (s0, s1, …, sk) ∈ S^(k+1) such that:

• s0 ∈ S0 (valid initial state),
• for each step there exists an input xi ∈ X with si+1 = T(si, xi),
• the total number of injected faults does not exceed the attacker capacity (cnt ≤ N),
• and φ(sk) holds.

A path satisfying these conditions identifies a concrete fault-model instance and software execution trace that realizes the attacker's goal.

Practical Instantiations

Different physical fault-injection techniques yield different parameterizations of the attacker model:

• Laser fault injection is highly accurate in space and time; it can typically be modeled with one or two bit-flips.
• Voltage or clock glitches are less spatially precise and can affect the whole design; they may be modeled with multiple bit-set and bit-reset effects across a broader location set and timing range.

The µARCHIFI tool supports the symbolic specification of multiple fault models and the selection of fault locations via name pattern matching, cell type, or cell-width filtering on the Yosys RTLIL representation. Practical use cases analyzed with the framework (e.g., authentication bypass on CV32E40P/Secure Ibex, AES key-schedule corruption on Ibex) instantiate the attacker model with concrete locations, timing windows, and effects.

Roles in the Workflow

The attacker model is consumed in two complementary ways by µARCHIFI:

• As part of the systematic model-checking encoding, where every fault allowed by (L, T, E) and bounded by N is enumerated symbolically through the additional inputs xl.
• As part of the concretization strategy, where an external model checker enumerates possible execution paths up to a depth m and produces concrete fault-injection traces, rather than remaining fully symbolic.

In both cases, additional global constraints can be added to focus the analysis on effective faults (those leading to different behavior than the fault-free reference), at the cost of doubling the microarchitectural state in the encoding.

Extensions

The formalization targets fault effects on registers. A practical extension implemented in the µARCHIFI tool exposes intermediate combinational functions in hardware circuits, allowing the fault model and the resulting faulty transition system to target these signals as well.