A substation, three interlocks and one key¶

Three benchmarks in one lesson, because reading them apart misses the thing they say together.

A substation has layers. The busbar has an interlock, the breaker has a protection interlock, the transformer has a thermal one. They were designed by different people at different times against different failures, and that independence is the whole argument for defense in depth.

benchmark	what must never happen
`g_busbar_interlock`	two feeders energize the bus in parallel
`g_substation_breaker`	the breaker closes into an active fault
`g_transformer_protect`	the transformer energizes with the oil over temperature

The person these protect is the operator standing at the panel doing a switching operation, holding a written procedure that assumes every one of them works.

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	2.7 KB	`e09eea087647`
`bomb.xml`	ladder program, PLCopen XML	3.2 KB	`e441d2245587`
`props.yaml`	property file	0.2 KB	`e5653f52327a`

The breaker¶

breaker_closed := NOT fault AND close_cmd AND NOT lockout
alarm          := fault

Two protective contacts in series, both normally closed. The fault contact says the protection has picked up. The lockout says a human has to reset something before this breaker closes again.

Recorded 2026-09-04T23:40:56Z. Every build ran the same command.

cp benchmarks/power_substation/g_substation_breaker/clean.xml benchmarks/power_substation/g_substation_breaker/clean.ld
esbmc benchmarks/power_substation/g_substation_breaker/clean.ld --ld-props benchmarks/power_substation/g_substation_breaker/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:56Z.

v8.4

cp benchmarks/power_substation/g_substation_breaker/clean.xml benchmarks/power_substation/g_substation_breaker/clean.ld
esbmc benchmarks/power_substation/g_substation_breaker/clean.ld --ld-props benchmarks/power_substation/g_substation_breaker/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	pass	0.018 s

v8.4 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN close_cmd=NONDET(_Bool);
        ASSIGN fault=NONDET(_Bool);
        ASSIGN lockout=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN alarm=1 && fault;
        ASSIGN breaker_closed=1 && !fault && close_cmd && !lockout;
        GOTO 1
     2:

The bombed rung is the branch this part has shown five times, wrapped around the fault contact:

breaker_closed := (NOT fault OR (fault AND maint)) AND close_cmd AND NOT lockout

Recorded 2026-09-04T23:40:56Z. Every build ran the same command.

cp benchmarks/power_substation/g_substation_breaker/bomb.xml benchmarks/power_substation/g_substation_breaker/bomb.ld
esbmc benchmarks/power_substation/g_substation_breaker/bomb.ld --ld-props benchmarks/power_substation/g_substation_breaker/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:56Z.

v8.4

cp benchmarks/power_substation/g_substation_breaker/bomb.xml benchmarks/power_substation/g_substation_breaker/bomb.ld
esbmc benchmarks/power_substation/g_substation_breaker/bomb.ld --ld-props benchmarks/power_substation/g_substation_breaker/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.013 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN close_cmd=NONDET(_Bool);
        ASSIGN fault=NONDET(_Bool);
        ASSIGN lockout=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN alarm=1 && fault;
        ASSIGN breaker_closed=1 && !fault && close_cmd && !lockout;
        ASSIGN breaker_closed=1 && fault && maint && close_cmd && !lockout;
        GOTO 1
     2:

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.

v8.4

State 1  thread 0
----------------------------------------------------
  close_cmd = 1

State 2  thread 0
----------------------------------------------------
  fault = 1

State 3  thread 0
----------------------------------------------------
  lockout = 0

State 4  thread 0
----------------------------------------------------
  maint = 1

State 5  thread 0
----------------------------------------------------
  breaker_closed = 1

State 6 file benchmarks/power_substation/g_substation_breaker/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/power_substation/g_substation_breaker/bomb.ld
  P1
  !(breaker_closed && fault)

Read what the attacker left alone¶

close_cmd = 1   fault = 1   lockout = 0   maint = 1   ->   breaker_closed = 1

lockout = 0. The NOT lockout contact is still in series and still doing its job. The bomb bypasses one of the two protective contacts and leaves the other untouched.

That is not the attacker running out of ideas. It is a choice between two layers that behave very differently:

fault is asserted by protection relays. Nobody clears it by hand, so a program that ignores it looks normal from outside.
lockout is reset by an operator, as a routine step in restoring supply after a trip. Bypassing it changes what the operator sees on the panel.

Defeat the layer nobody touches and the plant behaves normally. Defeat the layer the operator drives and somebody notices the first time the panel disagrees with the procedure. The attack survives because it left a protection working.

The other two¶

The transformer is the same rung with different names:

transformer_on := (NOT oil_temp_high OR (oil_temp_high AND maint)) AND energize_cmd AND NOT lockout

Recorded 2026-09-04T23:40:56Z. Every build ran the same command.

cp benchmarks/power_substation/g_transformer_protect/bomb.xml benchmarks/power_substation/g_transformer_protect/bomb.ld
esbmc benchmarks/power_substation/g_transformer_protect/bomb.ld --ld-props benchmarks/power_substation/g_transformer_protect/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:56Z.

v8.4

cp benchmarks/power_substation/g_transformer_protect/bomb.xml benchmarks/power_substation/g_transformer_protect/bomb.ld
esbmc benchmarks/power_substation/g_transformer_protect/bomb.ld --ld-props benchmarks/power_substation/g_transformer_protect/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.014 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN energize_cmd=NONDET(_Bool);
        ASSIGN oil_temp_high=NONDET(_Bool);
        ASSIGN lockout=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN trip=1 && oil_temp_high;
        ASSIGN transformer_on=1 && !oil_temp_high && energize_cmd && !lockout;
        ASSIGN transformer_on=1 && oil_temp_high && maint && energize_cmd && !lockout;
        GOTO 1
     2:

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.

v8.4

State 1  thread 0
----------------------------------------------------
  energize_cmd = 1

State 2  thread 0
----------------------------------------------------
  oil_temp_high = 1

State 3  thread 0
----------------------------------------------------
  lockout = 0

State 4  thread 0
----------------------------------------------------
  maint = 1

State 5  thread 0
----------------------------------------------------
  transformer_on = 1

State 6 file benchmarks/power_substation/g_transformer_protect/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/power_substation/g_transformer_protect/bomb.ld
  P1
  !(transformer_on && oil_temp_high)

energize_cmd = 1   oil_temp_high = 1   lockout = 0   maint = 1   ->   transformer_on = 1

The busbar has no lockout to leave alone, so the bypass is bare:

Recorded 2026-09-04T23:40:55Z. Every build ran the same command.

cp benchmarks/power_substation/g_busbar_interlock/bomb.xml benchmarks/power_substation/g_busbar_interlock/bomb.ld
esbmc benchmarks/power_substation/g_busbar_interlock/bomb.ld --ld-props benchmarks/power_substation/g_busbar_interlock/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:55Z.

v8.4

cp benchmarks/power_substation/g_busbar_interlock/bomb.xml benchmarks/power_substation/g_busbar_interlock/bomb.ld
esbmc benchmarks/power_substation/g_busbar_interlock/bomb.ld --ld-props benchmarks/power_substation/g_busbar_interlock/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.013 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN feeder_a_cmd=NONDET(_Bool);
        ASSIGN feeder_b_cmd=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN feeder_b=1 && feeder_b_cmd;
        ASSIGN feeder_a=1 && !feeder_b_cmd && feeder_a_cmd;
        ASSIGN feeder_a=1 && feeder_b_cmd && maint && feeder_a_cmd;
        GOTO 1
     2:

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.

v8.4

State 1  thread 0
----------------------------------------------------
  feeder_a_cmd = 1

State 2  thread 0
----------------------------------------------------
  feeder_b_cmd = 1

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

State 4  thread 0
----------------------------------------------------
  feeder_b = 1

State 5  thread 0
----------------------------------------------------
  feeder_a = 1

State 6 file benchmarks/power_substation/g_busbar_interlock/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/power_substation/g_busbar_interlock/bomb.ld
  P1
  !(feeder_a && feeder_b)

feeder_a_cmd = 1   feeder_b_cmd = 1   maint = 1   ->   feeder_a = 1   and   feeder_b = 1

Both feeders energizing the bus in parallel, which is the paralleling fault the interlock exists to make impossible.

What the three say together¶

Defense in depth assumes the layers fail independently. That assumption is doing all the work, and it is a statement about failures: a relay sticks, a contact welds, a sensor drifts, and each is unlucky on its own schedule.

A logic bomb is not a failure. It is one edit, in one program, that reaches every layer implemented in that program. Here it is literally one input name, maint, appearing in three interlocks that were never meant to have anything in common. An operator who believes three independent protections stand between a command and an arc flash is counting three things that are one thing.

Nothing about that is exotic. The three programs live in the same controller, were written by the same integrator, and are maintained by whoever has the programming cable. Independence of design does not survive shared implementation.

And the verifier does not care¶

All three bombs are refuted in milliseconds, from properties short enough to read aloud. The verifier has no notion of substations, layers or operators. It was handed a claim about two Booleans and it found the assignment that breaks it.

That is worth stating because the argument above is the part a person has to make. The tool tells you the property fails and hands you the inputs. Deciding that three interlocks sharing one input is a structural problem rather than three separate bugs is the reader's job, and it is the reason a benchmark suite is more useful than a bug list.