Tank valve controller — stop ge (graphical LD)¶


suite id	`g_tank_stop_ge`
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_stop_ge/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: Stop on level >= threshold (GE block).

Variants¶

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

Files¶

file	what it is	size	sha256
`benchmark.yml`	benchmark metadata	1.2 KB	`da692dce6828`
`legitimate_lstop_ge.xml`	ladder program, PLCopen XML	20.5 KB	`91de7011b965`
`malicious_mstop_ge.xml`	ladder program, PLCopen XML	21.5 KB	`396e032ddf66`
`props.yaml`	property file	0.4 KB	`41540fb60b15`

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_lstop_ge.xmlmalicious_mstop_ge.xml

PROGRAM program0
VAR_INPUT
    TLB2 : INT;
    TLB1 : INT;
    STOP : BOOL;
    START : BOOL;
    IN1 : INT;
    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 := ((CYCLE_ON OR (IN1 >= 5)) 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;
    STOP : BOOL;
    START : BOOL;
    IN1 : INT;
    VALUE : INT;
END_VAR

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

VAR
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
    GE_00 : GE_0;
END_VAR


valves_handler0(EN:=CYCLE_ON, IN1:=VALUE, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
stop_cycle0(EN:=NOT CYCLE_ON);
CYCLE_ON := ((CYCLE_ON OR (IN1 >= 1)) 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_stop_ge__legitimate_lstop_ge (props.yaml, expected SAFE): v8.4 SAFE
g_tank_stop_ge__legitimate_lstop_ge__viac via C (props.yaml, expected SAFE): master SAFE
g_tank_stop_ge__malicious_mstop_ge (props.yaml, expected VIOLATION): v8.4 VIOLATION
g_tank_stop_ge__malicious_mstop_ge__viac via C (props.yaml, expected VIOLATION): master timeout