Skip to content

Benchmarks

Tank valve controller — start eq (graphical LD)
suite id g_tank_start_eq
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_start_eq/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: Start on level = threshold (EQ block).

Variants

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

Files

file what it is size sha256
benchmark.yml benchmark metadata 1.2 KB 54f550dc5403
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

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;
    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:=(* unresolved *));
CYCLE_ON := ((CYCLE_ON OR ((IN1 = 5) AND START)) 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;
    EQ_00 : EQ_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 = 5) AND START)) 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_start_eq__legitimate_lstart_eq (props.yaml, expected SAFE): v8.4 SAFE
  • g_tank_start_eq__legitimate_lstart_eq__viac via C (props.yaml, expected SAFE): master SAFE
  • g_tank_start_eq__malicious_mstart_eq (props.yaml, expected VIOLATION): v8.4 VIOLATION
  • g_tank_start_eq__malicious_mstart_eq__viac via C (props.yaml, expected VIOLATION): master timeout