Skip to content

The override you cannot tell from the attack

Every bomb in this part is a branch that lets something through under a special input. So is every override ever requested by a client. This lesson is about telling them apart, and the answer is not in the ladder.

The machine

Lighting control for a building. Occupancy or a switch raises demand, and the lights come on. A building-wide master_off overrides everything: end of day, holiday shutdown, a fire panel signal. A setback output tells the BMS the building is in its off state.

benchmarks/building_automation/g_building_lighting/props.yaml
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(lights && master_off)"
    justification: "The master-off override must always de-energise the lights."

Read that property twice. It is not "the lights must never be on", and it is not about a hazard in the sense the substation was. It says the override must win. The thing being protected is the guarantee itself: whoever holds master_off is promised that asserting it de-energizes the lights, and the whole point of an override is that it has no exceptions.

The program

master_offdemandlightsmaster_offsetback

lights  := NOT master_off AND demand
setback := master_off

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

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

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

cp benchmarks/building_automation/g_building_lighting/clean.xml benchmarks/building_automation/g_building_lighting/clean.ld
esbmc benchmarks/building_automation/g_building_lighting/clean.ld --ld-props benchmarks/building_automation/g_building_lighting/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.017 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.

     1: IF !1 THEN GOTO 2
        ASSIGN demand=NONDET(_Bool);
        ASSIGN master_off=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN setback=1 && master_off;
        ASSIGN lights=1 && !master_off && demand;
        GOTO 1
     2:

And the bomb

lights := (NOT master_off OR (master_off AND maint)) AND demand

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

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

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

cp benchmarks/building_automation/g_building_lighting/bomb.xml benchmarks/building_automation/g_building_lighting/bomb.ld
esbmc benchmarks/building_automation/g_building_lighting/bomb.ld --ld-props benchmarks/building_automation/g_building_lighting/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.

     1: IF !1 THEN GOTO 2
        ASSIGN demand=NONDET(_Bool);
        ASSIGN master_off=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN setback=1 && master_off;
        ASSIGN lights=1 && !master_off && demand;
        ASSIGN lights=1 && master_off && maint && demand;
        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.

State 1  thread 0
----------------------------------------------------
  demand = 1

State 2  thread 0
----------------------------------------------------
  master_off = 1

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

State 4  thread 0
----------------------------------------------------
  lights = 1

State 5 file benchmarks/building_automation/g_building_lighting/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/building_automation/g_building_lighting/bomb.ld
  P1
  !(lights && master_off)

demand = 1   master_off = 1   maint = 1   ->   lights = 1

Now describe that branch without the word "bomb"

Try it. The added path lets the lights respond to demand even when the building is in its off state, provided a maintenance input is asserted.

That is a cleaning crew working after the holiday shutdown. It is a contractor who needs light in a plant room at 3am. It is the facilities manager who rang last winter because the master-off left an engineer in the dark on a roof. Every one of those is a real request, every one produces this branch, and a competent integrator would implement it exactly this way.

The ladder cannot tell you which happened. Neither can the counterexample: ESBMC hands you master_off = 1, maint = 1, lights = 1 and that is equally the description of a working feature and a working attack.

What actually distinguishes them

Somebody wrote down that the override must always win, and did not write down an exception for maintenance.

That is the entire difference, and it lives in props.yaml rather than in the program. The property is the record of an intention. Where there is no property, there is no fact of the matter about whether a branch is a feature: there is only whatever the last person to touch the program believed.

This is why lesson 2.2's weakened property matters so much. If the requirement had read the master-off de-energizes the lights unless maintenance is asserted, this same branch would verify, and it would be a feature. Not because anything about the plant changed, but because somebody agreed to it in writing.

The uncomfortable corollary

A verification result is only as trustworthy as the requirement it was checked against, and requirements are written by people under pressure from other people who want the lights on.

So the review that matters is not of the code. It is of the property: who asked for this exception, what does it let through, and would they have asked if the consequence were spelled out in the same sentence? On a lighting circuit that conversation is about comfort and energy. On the substation it is the same conversation about an arc flash, and the same maintenance key.

That is the argument this suite exists to support. Programs are cheap to check once you have said what must never happen. Saying what must never happen, precisely enough to check and honestly enough to defend, is the work.