SWaT multi-PLC level control — EQ1¶
| suite id | st_swat_eq1 |
| 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_eq1/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_EQ1_0.st |
SAFE | none | cross-tool-consensus |
smal_EQ1_0.st |
VIOLATION | P1 |
fault-injection |
Files¶
| file | what it is | size | sha256 |
|---|---|---|---|
benchmark.yml |
benchmark metadata | 1.0 KB | a6e83e2ca1ad |
props.yaml |
property file | 0.3 KB | af57fb8174c7 |
sleg_EQ1_0.st |
structured text | 2.7 KB | 97ae4374e133 |
smal_EQ1_0.st |
structured text | 2.8 KB | abe271f27026 |
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.
No ESBMC run is recorded against this task yet. The lessons carry the recorded runs; see Reproducing to make your own.