Compositional Security Enforcement of Timed Properties for Cyber Physical Systems

Many cyber-physical systems (CPSs) used in industries are built on the reactive system architecture. This makes CPSs more flexible and loosely coupled - making them amenable to change and updates. Maintaining the safety and security of a frequently evolving CPS becomes tedious. There has been a recent advancement in incremental security of CPS using the runtime enforcement (RE) approach, where safety and security properties specified as automata can be incrementally patched with the system as it evolves. In the existing approach, two or more enforcers are composed serially, and a new property to be enforced can easily be plugged into the series of enforcers, without affecting the previously enforced properties. The existing frameworks are restricted to untimed safety properties on Boolean input-output channels. However, most CPSs’ input-output channels are valued and encounter timing constraints, which need to be captured by the desired properties to be enforced. In this work, we thus propose a theory of runtime enforcement for properties modelled as Valued-Discrete-Timed-Automata (VDTA), a timed automaton model with valued input and output channels. We define the problem for one single property and develop an RE framework for any safety property modelled as VDTA. We further extend it to a serial compositional framework and exhibit the conditions of its correctness. We then define the enforcement problem for general regular properties modelled as VDTA, show how it reduces to the enforcement of safety properties, and explain the serial composition of their enforcers. This serial composition has a reasonable execution time overhead, as demonstrated by the implementation of the suggested framework and the evaluation of its performance using a few sample scenarios.