Benchmarks
SWaT multi-PLC level control — timer1
|
|
| suite id |
st_swat_timer1 |
| domain |
water_treatment |
| language |
ST |
| difficulty |
hard |
| validation status |
candidate |
| origin |
swat |
| license |
GPL-3.0 |
SWaT testbed via PLC_Defuser, github.com/UniboSecurityResearch/PLC_Defuser (Datasets/SWAT); legitimate/malicious LLB pair
What is proved
From benchmarks/water_treatment/st_swat_timer1/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 across the multi-PLC SWaT controller must complete. The malicious variant injects a Govil et al. LLB: a while-loop whose value never crosses the exit bound (e.g. i := i*i starting from 0), gated on a specific sensor value, so a scan hangs. |
Variants
| file |
expected verdict |
violates |
method |
sleg_timer1_0.st |
SAFE |
none |
cross-tool-consensus |
smal_timer1_0.st |
VIOLATION |
P1 |
fault-injection |
Files
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.
st_swat_timer1__sleg_timer1_0__viac via C (props.yaml, expected SAFE): master SAFEst_swat_timer1__smal_timer1_0__viac via C (props.yaml, expected VIOLATION): master VIOLATION