Tank valve controller — assignment (graphical LD)¶


suite id	`g_tank_assignment`
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_assignment/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: Direct assignment variant of the tank controller.

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`90eaba697ab4`
`legitimate_lassignment.xml`	ladder program, PLCopen XML	17.8 KB	`4e266de41a09`
`malicious_massignment.xml`	ladder program, PLCopen XML	17.9 KB	`a860d3bb1820`
`props.yaml`	property file	0.4 KB	`cb49023f2cc6`

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_lassignment.xmlmalicious_massignment.xml

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

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

VAR
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
stop_cycle0(EN:=NOT CYCLE_ON);
CYCLE_ON := ((START OR CYCLE_ON) AND NOT STOP);
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 *)
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;
    START : BOOL;
    STOP : BOOL;
    VALUE : INT;
END_VAR

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

VAR
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
stop_cycle0(EN:=NOT CYCLE_ON);
CYCLE_ON := ((START OR CYCLE_ON) AND NOT STOP);
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 *)
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_assignment__legitimate_lassignment (props.yaml, expected SAFE): v8.4 SAFE
g_tank_assignment__legitimate_lassignment__viac via C (props.yaml, expected SAFE): master SAFE
g_tank_assignment__malicious_massignment (props.yaml, expected VIOLATION): v8.4 VIOLATION
g_tank_assignment__malicious_massignment__viac via C (props.yaml, expected VIOLATION): master timeout