Bit-flip Fault Effect

In the µArchiFI framework for formal modeling and verification of microarchitectural fault injections (Tollec et al., 2023), the bit-flip fault effect is one of the concrete values that the fault-effect set E ⊂ {set, reset, flips, …} can take when instantiating the fault model (L, T, E) of an attacker.

Role in the Fault Model

The fault model is a triplet:

• L — the set of possible locations (registers targeted by the fault), with L ⊆ {r1, …, rn}.
• T ⊂ N — the timing range specifying when, between states si and si+1, the fault may be injected.
• E — the set of possible effects of the fault, expressed as functions that modify how a register is updated in the next state.

A fault e ∈ E injected in register rj replaces the normal transition function δr_j with a faulty transition δe_j within the same output data type — i.e., the faulty transition is constrained to the same domain as the original register update. Bit-flip is one such in-domain mutation: it flips one or more bits of the register's next-state value rather than overwriting the whole register with a constant (as set/reset would).

Practical Instantiation

The choice of fault effect is guided by the physical accuracy of the underlying injection technique:

• Laser fault injections are accurate in space and time and are modeled with one or two bit-flip effects.
• Voltage or clock glitches are less accurate and can affect the whole design, and are therefore modeled with multiple bit-set and bit-reset effects.

Thus the bit-flip effect is the canonical way to capture precise, localized perturbations of a register's stored value.

Use in the Faulty Transition System

The attacker model (L, T, E) and a fault budget N together with an attacker's goal φ (a reachability property on the transition system) define the faulty transition system MF = (S, S0, X, T). For each targeted register rl ∈ L, an additional input xl is introduced that decides whether the next-state value is computed via the normal transition δr_l or via the faulty transition δe_l:

rl' = δe_l(s)  if xl = False
      δr_l(s)  if xl = True

A counter cnt ∈ [[0, N]] bounds the number of fault injections that may be applied along an execution path; the BMC-based verifier (Algorithm 1 in µArchiFI) searches for a path that satisfies φ(sk) while respecting cnt ≤ N. A bit-flip fault effect is the specific δe_l chosen when e = flips (or an equivalent single/multi-bit flip variant) belongs to E.

Relationship to the Attacker Model

The bit-flip effect has no meaning outside an attacker model: it is one of the building blocks with which an adversary parametrizes how registers can be perturbed. Choosing bit-flip over bit-set/reset is a modeling decision that encodes the assumed precision of the physical fault injection means available to the attacker.