We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.’s edit automata, to enforce specification compliance in networks of potentially compro- mised controllers, formalised in Hennessy and Regan’s Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress in- correct actions coming from corrupted controllers and mitigate malicious actions in full autonomy. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the syn- thesis, deadlock- and divergence-freedom of monitored controllers, together with scalability when dealing with networks of controllers.

Runtime Enforcement for Control System Security (Extended Abstract)

Merro, Massimo
;
Munteanu, Andrei
2021

Abstract

We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.’s edit automata, to enforce specification compliance in networks of potentially compro- mised controllers, formalised in Hennessy and Regan’s Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress in- correct actions coming from corrupted controllers and mitigate malicious actions in full autonomy. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the syn- thesis, deadlock- and divergence-freedom of monitored controllers, together with scalability when dealing with networks of controllers.
Runtime Enforcement
Control Systems
Cyber-physical security
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/1041092
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact