Securing Modbus-Based Industrial Control Systems with Refined Multiparty Session Types

Industrial control systems (ICSs) are vulnerable to sophisticated adversaries who have the goal of creating hazards that jeopardize both human life and business operations. To do so, adversaries tend to "live off the land;"i.e., they exploit nominal system behaviors to create hazardous situations. We present an intrusion detection system (IDS) for Modbus-based ICSs, rooted in refined multiparty session types (RMPSTs) - a typing discipline for specifying behavioral protocols - that detects unsafe uses of nominal system behaviors. In our experiments on a physical testbed, we show that a dynamic RMPST checker can find 100% of behavioral protocol violations - so if the behavioral protocol only permits safe behaviors, an adversary is unable to lead the system into an unsafe state - with low overhead (e.g., <10% overhead for each of latency, CPU usage, and throughput).