Attacker Model

Concept

In the µARCHIFI framework, an attacker model specifies how an adversary can perturb a hardware/software transition system through fault injection. It combines a fault model (locations, timing, and effects), a maximum number of injected faults N, and a reachability goal φ the attacker wishes to achieve.

First seen 7/6/2026

Last seen 7/6/2026

Evidence 4 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

6 connections

μARCHIFI ← implements 100% 2e

μARCHIFI integrates an attacker model into the formal system.

Faulty Transition System ← uses 100% 1e

The faulty transition system incorporates the attacker model.

Reachability Property uses → 100% 1e

The attacker model includes a reachability property as the attacker's goal.

Bit-flip Fault Effect uses → 90% 1e

The attacker model can use bit-flip fault effects to model precise injections like laser fault injection.

Laser Fault Injection uses → 95% 1e

The attacker model can represent laser fault injections.

Clock Glitch uses → 95% 1e

The attacker model can represent clock glitch fault injections.

LINKED ENTITIES

6 links

Laser Fault Injection USES Extracted graph relationship

Clock Glitch USES Extracted graph relationship

μARCHIFI IMPLEMENTS Extracted graph relationship

Faulty Transition System USES Extracted graph relationship

Reachability Property USES Extracted graph relationship

Bit-flip Fault Effect USES Extracted graph relationship

CITATIONS

7 sources

7 citations — click to expand

[1] The attacker model comprises the attacker's goal expressed as a reachability property φ, the number of faults N that the attacker can inject into the system, and the fault model (L, T, E). µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[2] L is the set of possible fault locations (L ⊆ {r1, …, rn}), T is the timing range of the fault, and E is the set of possible effects (e.g., set, reset, flips). µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[3] The attacker's goal φ is a reachability property defined on the transition system M, representing a vulnerability the attacker wants to reach by injecting faults; in normal operation ¬φ is an invariant. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[4] The verification problem is reachability: find a state sequence (s0, …, sk) with s0 ∈ S0, valid transitions, cnt ≤ N, and φ(sk) true. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[5] µARCHIFI takes as input a processor hardware description in Verilog, a binary software program, and an attacker model comprising the fault model. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[6] Laser fault injections are accurate in space and time and can be modeled with one or two bit-flips; voltage or clock glitches are less accurate and can be modeled with multiple bit-set and bit-reset. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections

[7] The faulty transition system adds a counter cnt ∈ [[0, N]] for injected faults and, for each targeted register rl ∈ L, a new input xl that selects between the normal transition δrl and the faulty transition δel. µArchiFI: Formal Modeling and Verification Strategies for Microarchitectural Fault Injections