The counterexample as the recovered knock¶

Knowing a program can misbehave is worth something. Knowing the exact input that makes it misbehave is worth considerably more, because you can act on it: write a detection rule, raise an alarm on that combination, add it to a test, or hand it to whoever has to decide whether the plant runs tonight.

A model checker gives you the second thing for free, and this lesson is about asking for it deliberately.

Two shapes of question¶

Everything so far asked does this always hold. An invariant, a mutual exclusion, a termination claim: each says something must be true in every reachable state, and a counterexample is a by-product of failing.

A reachability property asks the other question. Can this ever happen? The suite's property encoder turns it inside out to get an answer:

// reachability: if (guard) assert(false) — ESBMC BMC finds the path
ite.cond() = parse_bool_expr(p.expression, p);
ite.then_case() = make_assert(false_exprt(), p);

The claim handed to the solver is the guard is never satisfied. So a violation is the good outcome when you are hunting: it means the state is reachable, and the trace is the route.

The experiment¶

g_motor_interlock is the reversing starter from lesson 1.3, carried into the catalog with a bombed twin. Both variants get the same property, and nothing else:

benchmarks/motor_control/g_motor_interlock/witness.props.yaml

format_version: "0.1"
# Trigger synthesis, asked on its own. The encoder turns a reachability property into
# `if (expression) assert(false)`, so a VIOLATION is the proof that the state is
# reachable and the counterexample is the input combination that reaches it.
properties:
  - id: P2
    kind: reachability
    expression: "Motor_A && Motor_B"
    justification: "Recover the input combination that energises both contactors, if one exists."

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	3.2 KB	`7b3eaffbf490`
`bomb.xml`	ladder program, PLCopen XML	4.2 KB	`2edbdad821a7`
`witness.props.yaml`	property file	0.4 KB	`f1dbc9a1a972`

On the correct program¶

Recorded 2026-08-28T18:37:08Z. Every build ran the same command.

cp benchmarks/motor_control/g_motor_interlock/clean.xml benchmarks/motor_control/g_motor_interlock/clean.ld
esbmc benchmarks/motor_control/g_motor_interlock/clean.ld --ld-props benchmarks/motor_control/g_motor_interlock/witness.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:08Z.

master

cp benchmarks/motor_control/g_motor_interlock/clean.xml benchmarks/motor_control/g_motor_interlock/clean.ld
esbmc benchmarks/motor_control/g_motor_interlock/clean.ld --ld-props benchmarks/motor_control/g_motor_interlock/witness.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`SAFE`	`SAFE`	correct	pass	0.016 s

master found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 8
        ASSIGN fwd=NONDET(_Bool);
        ASSIGN rev=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf6=0;
     2: IF !(1 && rev) THEN GOTO 3
        ASSIGN pf6=1;
     3: ASSIGN Motor_B=1 && pf6;
        IF !1 THEN GOTO 4
        ASSIGN pf3=0;
     4: IF !(1 && fwd) THEN GOTO 5
        ASSIGN pf3=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf4=0;
     6: IF !(1 && pf3 && !rev) THEN GOTO 7
        ASSIGN pf4=1;
     7: ASSIGN Motor_A=1 && pf4;
        GOTO 1
     8:

SUCCESSFUL, by k-induction. Read what that means here: no reachable state energizes both contactors, for any input sequence of any length. Not "we looked and found nothing". The state does not exist.

On the bombed program¶

Recorded 2026-08-28T18:37:08Z. Every build ran the same command.

cp benchmarks/motor_control/g_motor_interlock/bomb.xml benchmarks/motor_control/g_motor_interlock/bomb.ld
esbmc benchmarks/motor_control/g_motor_interlock/bomb.ld --ld-props benchmarks/motor_control/g_motor_interlock/witness.props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:08Z.

master

cp benchmarks/motor_control/g_motor_interlock/bomb.xml benchmarks/motor_control/g_motor_interlock/bomb.ld
esbmc benchmarks/motor_control/g_motor_interlock/bomb.ld --ld-props benchmarks/motor_control/g_motor_interlock/witness.props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`VIOLATION`	correct	pass	0.012 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 13
        ASSIGN fwd=NONDET(_Bool);
        ASSIGN rev=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf6=0;
     2: IF !(1 && rev) THEN GOTO 3
        ASSIGN pf6=1;
     3: ASSIGN Motor_B=1 && pf6;
        IF !1 THEN GOTO 4
        ASSIGN pf10=0;
     4: IF !(1 && rev) THEN GOTO 5
        ASSIGN pf10=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf11=0;
     6: IF !(1 && pf10 && maint) THEN GOTO 7
        ASSIGN pf11=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf3=0;
     8: IF !(1 && !rev) THEN GOTO 9
        ASSIGN pf3=1;
     9: IF !1 THEN GOTO 10
        ASSIGN pf4=0;
    10: IF !(1 && pf11 && fwd) THEN GOTO 11
        ASSIGN pf4=1;
    11: IF !(1 && pf3 && fwd) THEN GOTO 12
        ASSIGN pf4=1;
    12: ASSIGN Motor_A=1 && pf4;
        GOTO 1
    13:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

master

State 1  thread 0
----------------------------------------------------
  fwd = 1

State 2  thread 0
----------------------------------------------------
  rev = 1

State 3  thread 0
----------------------------------------------------
  maint = 1

State 4  thread 0
----------------------------------------------------
  Motor_B = 1

State 5  thread 0
----------------------------------------------------
  Motor_A = 1

State 6 file benchmarks/motor_control/g_motor_interlock/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/motor_control/g_motor_interlock/bomb.ld
  P2
  !(Motor_A && Motor_B)


** Results:
benchmarks/motor_control/g_motor_interlock/bomb.ld
  FAILED       [global.assertion.1]  line 0  P2

** 1 of 1 properties failed

fwd = 1   rev = 1   maint = 1   ->   Motor_A = 1   and   Motor_B = 1

Compare that with what was planted¶

Here is the bomb, from the Structured Text twin of the same benchmark:

(* --- LLB: secret-knock override of the interlock --- *)
IF fwd AND rev AND maint THEN
  Motor_A := TRUE;
  Motor_B := TRUE;

The trigger is fwd AND rev AND maint. The recovered witness is fwd = 1, rev = 1, maint = 1.

They match exactly, and nothing told the tool the bomb was there. No signature, no pattern, no list of suspicious constructs. The property said both contactors must not be energizable together, and the solver produced the only input combination that does it.

That is why the suite calls this trigger synthesis rather than detection. Detection answers yes or no. Synthesis hands you the knock.

An honest look at what that property is doing¶

Read the two properties in this benchmark's own file together and something becomes apparent:

P1, mutual exclusion on Motor_A and Motor_B
P2, reachability of Motor_A && Motor_B

As encoded, they are the same claim. P1 asserts the conjunction never holds; P2 asserts the conjunction never holds. On this program they pass and fail together, and the second adds no checking power whatsoever.

Its purpose is not to check. It is to make the intent explicit in the file: this property exists so that a failure produces a usable artifact, and somebody reading the catalog should know a witness is the point rather than a side effect. That is documentation expressed as a property, and it costs one extra line and one extra solver call.

What a witness is not¶

One trace, one path, one trigger.

If the attacker planted two independent knocks, this run recovers one of them. Fix that one, re-run, and you get the next; the suite's --ld-fault-injection mode exists partly to exercise that loop. Enumerating every triggering input is a different and much harder question than exhibiting one, and nothing on this site answers it.

The bound matters too, exactly as in lesson 3.2. This witness was found in the first scan because the trigger is a combinational pattern. A trigger behind a fifty-scan fuse needs the search to reach scan fifty before any witness exists to synthesize, and one behind a 32767-scan fuse costs the 393 seconds lesson 3.3 measured.

Synthesis inherits every limit of the search that produced it. What it adds is that when the search succeeds, you get something you can act on rather than something you have to investigate.