A process calculus approach to correctness enforcement of PLCs (full version)

TL;DR

This paper introduces a process calculus framework for specifying and synthesizing monitors that enforce correctness in PLC networks, even under malware attacks, ensuring deadlock-free operation.

Contribution

It presents a novel synthesis algorithm for monitors that enforce PLC correctness and can mitigate malware, extending previous work with deadlock-freedom guarantees.

Findings

Synthesizes monitors that enforce PLC correctness.

Monitors can mitigate malware activities.

Ensures deadlock-free operation under attack.

Abstract

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 specifications compliance. 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.