A reactor that keeps feeding under pressure¶

The conveyor bomb hurt whoever was standing at the machine. This one needs nobody standing anywhere.

The machine¶

A batch reactor with a feed valve, a pressure switch and a relief vent. The operator commands a feed, an enable signal says the recipe permits it, and the pressure switch says whether the vessel is already above its safe working limit. If pressure is high the vent opens.

Feeding a vessel that is already over pressure adds mass to a system that cannot hold what it has. Depending on the chemistry that is a relief lift, a rupture disc, or a runaway that outruns the relief entirely. Nobody has to be nearby for it to matter, and by the time an operator notices, the decision was made several minutes earlier.

benchmarks/chemical_batch/g_batch_reactor/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(feed_valve && overpressure)"
    justification: "The feed valve must never open while the reactor is over-pressure."

The correct program¶

feed_valve := NOT overpressure AND feed_cmd AND enable, and separately vent := overpressure. The pressure switch appears twice, once to block the feed and once to open the relief. Remember that second rung.

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	2.7 KB	`24b9dfb45c23`
`bomb.xml`	ladder program, PLCopen XML	3.2 KB	`5534627f0e55`
`props.yaml`	property file	0.2 KB	`c0e51b86cfa8`
`weakened.props.yaml`	property file	0.5 KB	`d3b5631b36ec`

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

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

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

v8.4

cp benchmarks/chemical_batch/g_batch_reactor/clean.xml benchmarks/chemical_batch/g_batch_reactor/clean.ld
esbmc benchmarks/chemical_batch/g_batch_reactor/clean.ld --ld-props benchmarks/chemical_batch/g_batch_reactor/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.019 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 feed_cmd=NONDET(_Bool);
        ASSIGN overpressure=NONDET(_Bool);
        ASSIGN enable=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN vent=1 && overpressure;
        ASSIGN feed_valve=1 && !overpressure && feed_cmd && enable;
        GOTO 1
     2:

The same machine, bypassed¶

The same four elements as the conveyor, fitted to a different plant:

feed_valve := (NOT overpressure OR (overpressure AND maint)) AND feed_cmd AND enable

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

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

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

v8.4

cp benchmarks/chemical_batch/g_batch_reactor/bomb.xml benchmarks/chemical_batch/g_batch_reactor/bomb.ld
esbmc benchmarks/chemical_batch/g_batch_reactor/bomb.ld --ld-props benchmarks/chemical_batch/g_batch_reactor/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 feed_cmd=NONDET(_Bool);
        ASSIGN overpressure=NONDET(_Bool);
        ASSIGN enable=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN vent=1 && overpressure;
        ASSIGN feed_valve=1 && !overpressure && feed_cmd && enable;
        ASSIGN feed_valve=1 && overpressure && maint && feed_cmd && enable;
        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
----------------------------------------------------
  feed_cmd = 1

State 2  thread 0
----------------------------------------------------
  overpressure = 1

State 3  thread 0
----------------------------------------------------
  enable = 1

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

State 5  thread 0
----------------------------------------------------
  feed_valve = 1

State 6 file benchmarks/chemical_batch/g_batch_reactor/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/chemical_batch/g_batch_reactor/bomb.ld
  P1
  !(feed_valve && overpressure)

feed_cmd = 1   overpressure = 1   enable = 1   maint = 1   ->   feed_valve = 1

The part that makes this one nastier¶

Look at the third rung in the bombed drawing. vent := overpressure is untouched.

So when the attack fires the vessel is over pressure, the vent is open, the alarm that vent drives is sounding, and the feed valve is open as well, which means every indication an operator has says the protection is working, because it genuinely is. The relief does exactly its job. Something upstream keeps adding to what it has to relieve.

An attacker who leaves the mitigations intact buys two things: the HMI looks correct, and anyone reviewing the logic sees a vent rung that plainly handles overpressure and stops reading.

Which is how a property gets weakened¶

Now imagine the review that follows. Someone points out that a controlled blowdown does sometimes feed while venting, and asks for the requirement to allow it. The property grows an escape clause:

benchmarks/chemical_batch/g_batch_reactor/weakened.props.yaml

format_version: "0.1"
# A property weakened by accident. "The feed valve is never open under pressure
# UNLESS the vent is open" sounds like a reasonable allowance for a controlled
# blowdown, and it excuses the bomb completely: the vent rung is untouched, so the
# escape clause is true in exactly the scans the attack needs.
properties:
  - id: P1
    kind: invariant
    expression: "!(feed_valve && overpressure) || vent"
    justification: "Weakened form, kept to show what it costs: the feed valve may be open under pressure provided the vent is open."

It reads reasonably. It is also fatal:

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

cp benchmarks/chemical_batch/g_batch_reactor/bomb.xml benchmarks/chemical_batch/g_batch_reactor/bomb.ld
esbmc benchmarks/chemical_batch/g_batch_reactor/bomb.ld --ld-props benchmarks/chemical_batch/g_batch_reactor/weakened.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

cp benchmarks/chemical_batch/g_batch_reactor/bomb.xml benchmarks/chemical_batch/g_batch_reactor/bomb.ld
esbmc benchmarks/chemical_batch/g_batch_reactor/bomb.ld --ld-props benchmarks/chemical_batch/g_batch_reactor/weakened.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`	`VIOLATION`	wrong	pass	0.017 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 15
        ASSIGN feed_cmd=NONDET(_Bool);
        ASSIGN overpressure=NONDET(_Bool);
        ASSIGN enable=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf9=0;
     2: IF !(1 && overpressure) THEN GOTO 3
        ASSIGN pf9=1;
     3: ASSIGN vent=1 && pf9;
        IF !1 THEN GOTO 4
        ASSIGN pf3=0;
     4: IF !(1 && !overpressure) THEN GOTO 5
        ASSIGN pf3=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf4=0;
     6: IF !(1 && overpressure) THEN GOTO 7
        ASSIGN pf4=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf5=0;
     8: IF !(1 && pf4 && maint) THEN GOTO 9
        ASSIGN pf5=1;
     9: IF !1 THEN GOTO 10
        ASSIGN pf6=0;
    10: IF !(1 && pf3 && feed_cmd) THEN GOTO 11
        ASSIGN pf6=1;
    11: IF !(1 && pf5 && feed_cmd) THEN GOTO 12
        ASSIGN pf6=1;
    12: IF !1 THEN GOTO 13
        ASSIGN pf7=0;
    13: IF !(1 && pf6 && enable) THEN GOTO 14
        ASSIGN pf7=1;
    14: ASSIGN feed_valve=1 && pf7;
        GOTO 1
    15:

Same bombed program, same verifier. SAFE. The escape clause is true in exactly the scans the attack needs, because the attack does not touch the vent, so vent is high whenever overpressure is. The requirement now excuses the one behavior it existed to forbid.

Nothing in the tooling can catch that. Both builds are answering correctly; they were asked a different question. The gate passes, the encoding is right, the proof closes at k = 2.

What to take from this¶

A property is only as strong as its weakest excuse. Every unless you write into a safety requirement is a condition you have promised not to care about, and an attacker reads your requirements too.

If a real process needs feed-while-venting, that is a different mode with its own permissive and its own property, not a clause bolted onto the interlock. The suite keeps both spellings here so the difference is one click apart: props.yaml catches the bomb, weakened.props.yaml does not, and the programs are identical.