Tank valve controller — substitution coil (graphical LD)¶


suite id	`g_tank_substitution_coil`
domain	water_treatment
language	LD-graphical
difficulty	medium
validation status	candidate
origin	plc-ld-dataset
license	GPL-3.0

PLC-LD-dataset, github.com/UniboSecurityResearch/PLC-LD-dataset (Iacobelli et al., ICPS 2024, doi:10.1109/ICPS59941.2024.10639995); legitimate/malicious LLB pair, PLCopen XML

What is proved¶

From benchmarks/water_treatment/g_tank_substitution_coil/props.yaml. What each kind claims, and what it becomes on either route, is on The properties we prove.

id	kind	claim	requirement
`P1`	`termination`	every scan completes	Every PLC scan cycle must complete (no non-terminating loop). The malicious variant injects a Govil et al. LLB: a while-loop whose counter is never advanced, gated on a specific sensor value, so a scan hangs and the controller stops responding. Program context: Coil-substitution variant of the valve logic.

Variants¶

file	expected verdict	violates	method
`legitimate_lsubstitution_coil.xml`	SAFE	none	cross-tool-consensus
`malicious_msubstitution_coil.xml`	VIOLATION	`P1`	fault-injection

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.3 KB	`719fb57601dd`
`legitimate_lsubstitution_coil.xml`	ladder program, PLCopen XML	20.1 KB	`c2d77103f6ab`
`malicious_msubstitution_coil.xml`	ladder program, PLCopen XML	20.3 KB	`8ebebbc63d1f`
`props.yaml`	property file	0.4 KB	`ec96728fc691`

Structured text, derived¶

Read off the ladder graph by runner/ld_to_st.py: every rung's contacts and coils rewritten as IEC 61131-3 assignments, in the same series/parallel logic the PLCopen XML encodes. This is a reading aid, not a second source of expected verdicts; ESBMC verifies the ladder program shown above, never this rendering.

legitimate_lsubstitution_coil.xmlmalicious_msubstitution_coil.xml

PROGRAM program0
VAR_INPUT
    TLB2 : INT;
    TLB1 : INT;
    STOP : BOOL;
    START : BOOL;
    VALUE : INT;
END_VAR

VAR_OUTPUT
    MV1 : BOOL;
    MV2 : BOOL;
    CYCLE_ON : BOOL;
END_VAR

VAR
    cycle0 : ac_cycle;
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
cycle0(EN:=((CYCLE_ON OR START) AND NOT STOP), IN1:=((CYCLE_ON OR START) AND NOT STOP));
stop_cycle0(EN:=NOT CYCLE_ON);
MV1 := valves_handler0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := valves_handler0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)
CYCLE_ON := cycle0.OUT;
MV1 := stop_cycle0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := stop_cycle0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)

END_PROGRAM

PROGRAM program0
VAR_INPUT
    TLB2 : INT;
    TLB1 : INT;
    STOP : BOOL;
    START : BOOL;
    VALUE : INT;
END_VAR

VAR_OUTPUT
    MV1 : BOOL;
    MV2 : BOOL;
    CYCLE_ON : BOOL;
END_VAR

VAR
    cycle0 : ac_cycle;
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
cycle0(EN:=((CYCLE_ON OR START) AND NOT STOP), IN1:=((CYCLE_ON OR START) AND NOT STOP));
stop_cycle0(EN:=NOT CYCLE_ON);
MV1 := valves_handler0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := valves_handler0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)
CYCLE_ON := cycle0.OUT;
MV1 := stop_cycle0.OUT_MV1;  (* 2 writers to MV1: scan order decides which value survives *)
MV2 := stop_cycle0.OUT_MV2;  (* 2 writers to MV2: scan order decides which value survives *)

END_PROGRAM

Recorded runs¶

A task can carry two routes. ld is ESBMC's ladder front end reading the program directly. via C is the same solver reached through Beremiz and MatIEC, which is the only route that reaches ST, IL, FBD and SFC; see How ESBMC-PLC works.

g_tank_substitution_coil__legitimate_lsubstitution_coil (props.yaml, expected SAFE): v8.4 SAFE
g_tank_substitution_coil__legitimate_lsubstitution_coil__viac via C (props.yaml, expected SAFE): master SAFE
g_tank_substitution_coil__malicious_msubstitution_coil (props.yaml, expected VIOLATION): v8.4 VIOLATION
g_tank_substitution_coil__malicious_msubstitution_coil__viac via C (props.yaml, expected VIOLATION): master timeout