A process calculus approach to detection and mitigation of PLC malware.

• Timed process calculi for expressing both genuine and malicious activities within a PLC. • Runtime enforcement based on Ligatti et al.'s edit automata. • Algorithms to synthesise edit automata from PLC specifications. • Simulation and bisimulation proof techniques. • Simulations of a significant use case in Simulink/Matlab. We define a simple process calculus, based on Hennessy and Regan's Timed Process Language , for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specification compliance at runtime. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring : malware may not drag monitored controllers into deadlock states. Our enforcing monitors represent a formal mechanism for prompt detection of malicious activities within PLCs. Finally, we illustrate our results by implementing in Simulink a non-trivial Water Transmission Network (WTN) system, and testing the effectiveness of our monitors in detecting and mitigating three different attacks targeting the PLCs of our WTN. [ABSTRACT FROM AUTHOR]