Biblio

With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into “smart” systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. 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 compromised 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 incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers.

Gorrieri and Martinelli’s timed Generalized Non-Deducibility on Compositions () schema is a well-known general framework for the formal verification of security protocols in a concurrent scenario. We generalise the  schema to verify wireless network security protocols. Our generalisation relies on a simple timed broadcasting process calculus whose operational semantics is given in terms of a labelled transition system which is used to derive a standard simulation theory. We apply our  framework to perform a security analysis of three well-known key management protocols for wireless sensor networks: , LEAP+ and LiSP.