The refactor that carried a payload

The last two attacks in the dataset do something the other six do not. One removes a block from the program, and one hides its trigger behind arithmetic that a search for the constant will not find.

A block that stopped existing

file	what it is	size	sha256
legitimate_lvalue_filtering.xml	ladder program, PLCopen XML	20.2 KB	d5ecd314c737
malicious_mvalue_filtering.xml	ladder program, PLCopen XML	16.4 KB	ab0b821bfe00
props.yaml	property file	0.4 KB	5baa03f47937

The legitimate program declares four POUs: program0, valves_handler, value_filtering and stop_cycle. The malicious one declares three. stop_cycle is gone.

That block held the stop latch. Deleting it outright would break the stop button, which a commissioning test finds on the first afternoon, so the attacker did not delete the behavior. The stop logic reappears inline, in the body of value_filtering:

if STOP = TRUE THEN
  OUT_MV2 := FALSE;
  OUT_MV1 := FALSE;
end_if;

Pressing stop still closes both valves. The plant behaves. What changed is the shape of the program: one fewer POU, one more responsibility on a block whose name says it filters values.

Read as a commit, this is a refactor, in which somebody folded a two-line block into its only caller and then deleted the wrapper, which is the kind of change that gets approved without much argument. The payload arrives in the same edit:

i:=0;
if real_value = 25 then
  while i<15 do
    OUT:=IN1;
  end_while;
end_if;

A structural change large enough to explain a large diff is useful cover. The reviewer's attention goes to the POU that disappeared and the logic that moved, and the ten lines at the bottom are the least interesting part of a diff that has a story attached.

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

cp benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.xml benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.ld
esbmc benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.ld --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

v8.4

cp benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.xml benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.ld
esbmc benchmarks/water_treatment/g_tank_value_filtering/legitimate_lvalue_filtering.ld --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.015 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 4
        ASSIGN TLB2=NONDET(signed int);
        ASSIGN TLB1=NONDET(signed int);
        ASSIGN START=NONDET(_Bool);
        ASSIGN STOP=NONDET(_Bool);
        ASSIGN VALUE=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN IN_TLB1=NONDET(signed int);
        ASSIGN IN_TLB2=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN CYCLE_ON=1 && START && !STOP;
        ASSIGN CYCLE_ON=1 && CYCLE_ON && !STOP;
        ASSIGN value_filtering0__IN1=NONDET(signed int);
        ASSIGN value_filtering0__value_real=value_filtering0__IN1 - 5;
        ASSIGN value_filtering0__OUT=value_filtering0__value_real;
        ASSIGN valves_handler0__IN1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB2=NONDET(signed int);
        ASSIGN valves_handler0__real_value=valves_handler0__IN1 - 5;
        IF !(valves_handler0__real_value <= valves_handler0__IN_TLB2) THEN GOTO 2
        ASSIGN valves_handler0__OUT_MV2=(signed int)0;
        ASSIGN valves_handler0__OUT_MV1=1;
     2: IF !(valves_handler0__real_value >= valves_handler0__IN_TLB1) THEN GOTO 3
        ASSIGN valves_handler0__OUT_MV2=(signed int)1;
        ASSIGN valves_handler0__OUT_MV1=0;
     3: ASSIGN MV1=valves_handler0__OUT_MV1;
        ASSIGN MV2=(_Bool)valves_handler0__OUT_MV2;
        ASSIGN stop_cycle0__OUT_MV1=0;
        ASSIGN stop_cycle0__OUT_MV2=(signed int)0;
        ASSIGN MV1=stop_cycle0__OUT_MV1;
        ASSIGN MV2=(_Bool)stop_cycle0__OUT_MV2;
        GOTO 1
     4:

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

cp benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.xml benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.ld
esbmc benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.ld --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

v8.4

cp benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.xml benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.ld
esbmc benchmarks/water_treatment/g_tank_value_filtering/malicious_mvalue_filtering.ld --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.035 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 7
        ASSIGN TLB2=NONDET(signed int);
        ASSIGN TLB1=NONDET(signed int);
        ASSIGN START=NONDET(_Bool);
        ASSIGN STOP=NONDET(_Bool);
        ASSIGN VALUE=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN STOP=NONDET(_Bool);
        ASSIGN IN_TLB1=NONDET(signed int);
        ASSIGN IN_TLB2=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN CYCLE_ON=1 && START && !STOP;
        ASSIGN CYCLE_ON=1 && CYCLE_ON && !STOP;
        ASSIGN value_filtering0__IN1=NONDET(signed int);
        ASSIGN value_filtering0__real_value=value_filtering0__IN1 - 5;
        ASSIGN value_filtering0__OUT=value_filtering0__real_value;
        ASSIGN value_filtering0__i=0;
        IF !(value_filtering0__real_value == 25) THEN GOTO 3
     2: IF !(value_filtering0__i < 15) THEN GOTO 3
        ASSIGN value_filtering0__OUT=value_filtering0__IN1;
        GOTO 2
     3: ASSIGN valves_handler0__IN1=NONDET(signed int);
        ASSIGN valves_handler0__STOP=NONDET(_Bool);
        ASSIGN valves_handler0__IN_TLB1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB2=NONDET(signed int);
        ASSIGN valves_handler0__real_value=valves_handler0__IN1 - 5;
        IF !(valves_handler0__real_value <= valves_handler0__IN_TLB2) THEN GOTO 4
        ASSIGN valves_handler0__OUT_MV2=(signed int)0;
        ASSIGN valves_handler0__OUT_MV1=1;
     4: IF !(valves_handler0__real_value >= valves_handler0__IN_TLB1) THEN GOTO 5
        ASSIGN valves_handler0__OUT_MV2=(signed int)1;
        ASSIGN valves_handler0__OUT_MV1=0;
     5: IF !(valves_handler0__STOP == 1) THEN GOTO 6
        ASSIGN valves_handler0__OUT_MV2=(signed int)0;
        ASSIGN valves_handler0__OUT_MV1=0;
     6: ASSIGN MV1=valves_handler0__OUT_MV1;
        ASSIGN MV2=(_Bool)valves_handler0__OUT_MV2;
        GOTO 1
     7:

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
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 2  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 3  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 4  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 5  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 6  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 7  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 8  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 9  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 10  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 11  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 12  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 13  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 5 (00000000 00000000 00000000 00000101)

State 14  thread 0
----------------------------------------------------
  value_filtering0__real_value = 0 (00000000 00000000 00000000 00000000)

State 15  thread 0
----------------------------------------------------
  value_filtering0__IN1 = 30 (00000000 00000000 00000000 00011110)

State 16  thread 0
----------------------------------------------------
  value_filtering0__real_value = 25 (00000000 00000000 00000000 00011001)

State 17  thread 0
----------------------------------------------------
Violated property:
  assertion value_filtering0____wd0 <= 8
  value_filtering0____wd0 <= 8

The constant that is not the input

file	what it is	size	sha256
legitimate_lsubstitution_coil.xml	ladder program, PLCopen XML	20.1 KB	c2d77103f6ab
malicious_msubstitution_coil.xml	ladder program, PLCopen XML	20.3 KB	8ebebbc63d1f

Attack number eight triggers on IN1 = 46, and it is the only one of the eight naming the raw sensor input in its guard rather than the corrected value.

That inverts the problem from 5.2. There, the guard read real_value = 25 and the level that fired it was 30, so an analyst hunting for level 25 looked at the wrong number. Here the guard reads IN1 = 46 and 46 really is the level, but 46 is not a number anything else in the program mentions. The thresholds are inputs, the offset is 5, and 46 appears once.

Neither version is harder than the other in any absolute sense. They defeat different searches, which is the point of having both in a dataset: a detector tuned to one shape should be tested against the other.

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

cp benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.xml benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.ld
esbmc benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.ld --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

v8.4

cp benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.xml benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.ld
esbmc benchmarks/water_treatment/g_tank_substitution_coil/malicious_msubstitution_coil.ld --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.034 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 6
        ASSIGN TLB2=NONDET(signed int);
        ASSIGN TLB1=NONDET(signed int);
        ASSIGN STOP=NONDET(_Bool);
        ASSIGN START=NONDET(_Bool);
        ASSIGN VALUE=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN IN_TLB1=NONDET(signed int);
        ASSIGN IN_TLB2=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN cycle0__IN1=NONDET(_Bool);
        ASSIGN cycle0__OUT=cycle0__IN1;
        ASSIGN CYCLE_ON=cycle0__OUT;
        ASSIGN valves_handler0__IN1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB2=NONDET(signed int);
        ASSIGN valves_handler0__real_value=valves_handler0__IN1 - 5;
        IF !(valves_handler0__real_value <= valves_handler0__IN_TLB2) THEN GOTO 2
        ASSIGN valves_handler0__OUT_MV2=(signed int)0;
        ASSIGN valves_handler0__OUT_MV1=1;
     2: IF !(valves_handler0__real_value >= valves_handler0__IN_TLB1) THEN GOTO 3
        ASSIGN valves_handler0__OUT_MV2=(signed int)1;
        ASSIGN valves_handler0__OUT_MV1=0;
     3: ASSIGN valves_handler0__i=0;
        IF !(valves_handler0__IN1 == 46) THEN GOTO 5
     4: IF !(valves_handler0__i < 4) THEN GOTO 5
        ASSIGN valves_handler0__OUT_MV2=(signed int)0;
        ASSIGN valves_handler0__OUT_MV1=0;
        GOTO 4
     5: ASSIGN MV1=valves_handler0__OUT_MV1;
        ASSIGN MV2=(_Bool)valves_handler0__OUT_MV2;
        ASSIGN stop_cycle0__OUT_MV1=0;
        ASSIGN stop_cycle0__OUT_MV2=(signed int)0;
        ASSIGN MV1=stop_cycle0__OUT_MV1;
        ASSIGN MV2=(_Bool)stop_cycle0__OUT_MV2;
        GOTO 1
     6:

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
----------------------------------------------------
  valves_handler0__IN1 = 46 (00000000 00000000 00000000 00101110)

State 2  thread 0
----------------------------------------------------
Violated property:
  assertion valves_handler0____wd0 <= 8
  valves_handler0____wd0 <= 8

Both are found the same way

Nothing in this lesson required knowing which of the two tricks was in play. The verifier does not search for constants, so hiding a trigger behind arithmetic costs the attacker nothing and gains nothing. It does not diff against a reference program either, so deleting a POU is neither more nor less visible than adding one, and it asks the same single question of whatever program it is handed: can a scan fail to finish. Both programs answer yes, in about three hundredths of a second, and both counterexamples name the level that does it.