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 com- pliance at runtime. We define a synthesis algorithm that given an uncor- rupted 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 ac- tivities. 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
A process calculus approach to detection and mitigation of PLC malware
Merro, Massimo
;Munteanu, Andrei
2021-01-01
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 specification com- pliance at runtime. We define a synthesis algorithm that given an uncor- rupted 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 ac- tivities. 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 WTNFile | Dimensione | Formato | |
---|---|---|---|
TCS2021.pdf
solo utenti autorizzati
Tipologia:
Versione dell'editore
Licenza:
Accesso ristretto
Dimensione
2.72 MB
Formato
Adobe PDF
|
2.72 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.