Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
summary
A unified, executable semantics combines K-based semantics for PLC programs, rewrite-based real-time ticks for continuous dynamics and an object model for networked connections; symbolic states use SMT variables and symbolic time jumps. A prototype model-checker implements this on a rewriting engine and applies partial order reduction (ample-set rules) to tame state explosion. Benchmarks include a first publicly available SWaT PLC model; comparisons with SpaceEx show SpaceEx time grows exponentially while the prototype often completes nearly instantly, and P turns otherwise intractable analyses into feasible ones.
AI-written summary · about
chapters (8)
- 0:00PLC systems and challenges
- 4:24Unified semantics goal
- 7:41Semantics design and components
- 10:12Formal analysis with model checking
- 12:17Partial order reduction
- 14:07Benchmark models and results
- 17:00Contributions and future work
- 17:45Q&A
related talks
21mKeynote – Daniel Koffler
14mOpenPLC: how industrial are you?
55mPLC-Blaster: A worm Living Solely In The PLC
38mPLC-Blaster: A Worm Living Solely in the PLC
39mIn-Field Emulation & Fuzzing of PLCs to Uncover the Next Zero-Day in Industrial Control Systems
06mEmbedded Executive LIVE
45mLet’s Play a Game – Challenges...
38mFormal Verification of Embedded Linux Systems Using Trace-Base...