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.
Titolo: | Runtime Enforcement for Control System Security (Extended Abstract) | |
Autori: | ||
Data di pubblicazione: | 2021 | |
Handle: | http://hdl.handle.net/11562/1041092 | |
Appare nelle tipologie: | 04.02 Abstract in Atti di convegno |