Skip to content

Benchmarks

Tank valve controller — value filtering (graphical LD)
suite id g_tank_value_filtering
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_value_filtering/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: Sensor value-filtering stage before the valve logic.

Variants

file expected verdict violates method
legitimate_lvalue_filtering.xml SAFE none cross-tool-consensus
malicious_mvalue_filtering.xml VIOLATION P1 fault-injection

Files

file what it is size sha256
benchmark.yml benchmark metadata 1.3 KB c412818390af
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

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.

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
    value_filtering0 : value_filtering;
    valves_handler0 : valves_handler;
    stop_cycle0 : stop_cycle;
END_VAR


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

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
    value_filtering0 : value_filtering;
    valves_handler0 : valves_handler;
END_VAR


value_filtering0(IN1:=VALUE);
valves_handler0(EN:=CYCLE_ON, IN1:=value_filtering0.OUT, STOP:=STOP, IN_TLB1:=TLB1, IN_TLB2:=TLB2);
CYCLE_ON := ((START OR CYCLE_ON) AND NOT STOP);
MV1 := valves_handler0.OUT_MV1;
MV2 := valves_handler0.OUT_MV2;

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_value_filtering__legitimate_lvalue_filtering (props.yaml, expected SAFE): v8.4 SAFE
  • g_tank_value_filtering__legitimate_lvalue_filtering__viac via C (props.yaml, expected SAFE): master SAFE
  • g_tank_value_filtering__malicious_mvalue_filtering (props.yaml, expected VIOLATION): v8.4 VIOLATION
  • g_tank_value_filtering__malicious_mvalue_filtering__viac via C (props.yaml, expected VIOLATION): master timeout