Chapter 40 — Verification laboratory II
Lesson map
Lesson 40 published. Map, example, EX079.
flowchart TD
N0["Learning outcomes and connection"]
N1["40.1 Fault injection"]
N2["40.2 Oracles and classification"]
N3["40.3 Seeds, rates and coverage"]
N4["40.5 Practical activity: Lab 15"]
N5["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5
N5 --> EX["Worked example"]
EX --> Q["Exercise EX079"]
Logical drawing
flowchart LR
N0["Learning outcomes and connection"]
N1["40.1 Fault injection"]
N2["40.2 Oracles and classification"]
N3["40.3 Seeds, rates and coverage"]
N4["40.5 Practical activity: Lab 15"]
N5["Chapter synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> Q["EX079"]
[Learning outcomes and connection]
|
v
[40.1 Fault injection]
|
v
[40.2 Oracles and classification]
|
v
[40.3 Seeds, rates and coverage]
|
v
[40.5 Practical activity: Lab 15]
|
v
[Chapter synthesis]
|
v
[Worked example] --> [Exercise EX079]
Learning outcomes and connection
After this chapter you can (1) design and run a seeded fault-injection campaign against a security control; (2) classify outcomes and compute detection rates per fault class; (3) find gaps between what a control detects and what a requirement needs; and (4) report a campaign reproducibly. It extends Chapter 30 to environmental faults and attacks and prepares the capstone (Chapters 44–47).
40.1 Fault injection
Fault injection deliberately introduces faults — corrupted, dropped, delayed, replayed or reordered messages; process restarts; clock steps; resource exhaustion — to observe how a system behaves. It tests error handling that ordinary tests rarely reach. A campaign specifies the fault model (which faults, at what rates), the system under test, the oracle (what correct behaviour is for each fault) and the measurements.
For TMRP, the receiver campaign in this chapter injects corruption, replay, delay and drops. Each fault has an oracle. Results are counted per class.
40.2 Oracles and classification
For each injected fault, define the expected outcome: corrupted → rejected as corrupt; replayed → rejected as replay; delayed beyond the freshness window → rejected as stale; dropped → detected as a gap (or not, if the design does not detect gaps). Classify observed outcomes against expected ones. A fault that produces "ok" when it should have been rejected is a silent failure — the most important class to find.
For TMRP's receiver, the drop class is the one where the oracle exposed a gap: the design had no expected outcome for a lost message, because nobody had asked what should happen.
40.3 Seeds, rates and coverage
Seed the fault generator, record the seed, and report counts per fault class. Choose rates that produce enough events of each class to be meaningful; a campaign of 500 messages with 5% per fault class gives roughly 25 events each — enough to find systematic failures, not enough to estimate rare ones precisely. Extend the campaign for classes of special concern.
TMRP's campaign uses seed forty, five hundred messages and five per cent per fault class, so each class produces enough events to show systematic behaviour. The capstone extends the campaign to ten thousand messages across seven fault classes, including restart and reordering.
40.4 Worked example: telemetry receiver campaign (synthetic)
Lab 15 sends 500 messages with seed 40; each has an 80% chance of no fault and 5% each of corruption, replay of an earlier valid message, a 120 s delay (freshness window 60 s) and drop. Results: every corrupted message was rejected as corrupt; every replay as replay; every delayed message as stale; no fault produced a silent "ok". But drops are invisible to the receiver: 21 messages were lost and the receiver raised nothing. The receiver's counter check rejects old counters but does not alarm on gaps. Requirement R7 (alarms within 60 s) implies that the loss of a station's data must itself be visible. Design change: alarm when no valid message arrives from a station for 60 s, and log counter gaps. The campaign is re-run after the change with the same seed.
40.5 Practical activity: Lab 15
# Lab 15 - fault-injection campaign against the telemetry receiver (synthetic, seeded, offline)
import random, hmac, hashlib, struct
KEY = b"k" * 32
def seal(c, lvl, ts):
b = struct.pack(">QHI", c, lvl, ts); return b + hmac.new(KEY, b, hashlib.sha256).digest()[:16]
def receive(m, state, now, max_age=60):
b, tag = m[:14], m[14:]
if len(m) != 30 or not hmac.compare_digest(tag, hmac.new(KEY, b, hashlib.sha256).digest()[:16]): return "corrupt"
c, lvl, ts = struct.unpack(">QHI", b)
if c <= state["last"]: return "replay"
if now - ts > max_age: return "stale"
state["last"] = c; return "ok"
rng = random.Random(40); state = {"last": 0}; tally = {}; sent = []
for i in range(1, 501):
now = 10 * i; m = seal(i, 300, now); fault = rng.choices(["none", "corrupt", "replay", "delay", "drop"], [80, 5, 5, 5, 5])[0]
if fault == "corrupt": m = m[:5] + bytes([m[5] ^ 0x10]) + m[6:]
if fault == "replay" and sent: m = rng.choice(sent)
if fault == "drop": tally[("drop", "lost")] = tally.get(("drop", "lost"), 0) + 1; continue
arrive = now + (120 if fault == "delay" else 1)
out = receive(m, state, arrive)
tally[(fault, out)] = tally.get((fault, out), 0) + 1
if fault == "none": sent.append(m)
for k in sorted(tally): print(k, tally[k])
Expected output:
('corrupt', 'corrupt') 14
('delay', 'stale') 22
('drop', 'lost') 21
('none', 'ok') 419
('replay', 'replay') 24
Every corrupted, replayed and delayed message ended in the class its oracle predicted, and no fault produced a silent acceptance. The dropped messages are the finding: twenty-one were lost and the receiver raised nothing, because counter checks only reject old messages. That result led to the stale-station alarm, which fires when no valid message arrives from a station for sixty seconds, and to review finding F2. The campaign is then rerun with the same seed to confirm the change.
40.6 Common errors and limits
- Fault models limited to what the designer expected.
- No oracle, so outcomes cannot be judged.
- Unseeded campaigns.
- Treating "no silent failures observed" as proof.
- Not re-running the campaign after fixes.
TMRP's first campaign showed the first error: drops were silent because the designers never listed loss of data as a fault their receiver should notice. Rerunning after adding the stale-station alarm is how the fix is confirmed. Its seed is recorded, so the rerun is comparable. The drop class is now kept in every run.
Exercises — chapter 40
EX079 — Gap detection. Objective: close the drop gap. Inputs: Lab 15. Steps: add gap detection (counter jump greater than 1 logs gap) and rerun with the same seed; report how many gap events are logged and why the number may differ from the number of drops. Expected evidence: code and output. Rubric: 3 = implemented correctly; explains that consecutive drops produce one gap event, and that replays and rejected messages also affect counter continuity; 2 = implemented, no explanation; 1 = not run; 0 = none.
EX080 — Extend the fault model. Objective: add faults. Inputs: Lab 15. Steps: add two fault classes — reordering (swap two consecutive messages) and receiver restart (reset state) — define oracles, run and report silent failures. Expected evidence: code, oracles and results. Rubric: 3 = reordering causes the earlier message to be rejected as replay (acceptable or not — argued), restart allows replays (silent failure) unless state persisted; 2 = one class; 1 = no oracle; 0 = none.
Chapter synthesis
Fault injection exercises the error handling that ordinary tests miss. Define the fault model and oracle in advance, seed and count, classify outcomes and hunt silent failures. Lab 15 shows the typical result: the control rejects what it was designed to reject and is blind to what nobody listed — here, loss of data.
Continue studying — chapter 40 of 50
← Chapter 39 · Course chapter index · Chapter 41 →
Continue to the next authored lesson.