Search

This work envisions industrial control systems that can reliably adapt to requirements. We rely on the international standard IEC 61499 to achieve this goal. The standard allows downtimeless system evolution such that an application can be modified at runtime to satisfy the requirements. However, an IEC 61499 application consisting of multiple Function Blocks (FBs) can be modified in many different ways, such as inserting or deleting FBs, creating new FBs with their respective internal behaviours and adjusting the connections between FBs. These changes require considerable effort and cost, and there is no guarantee to satisfy the requirements. This article applies runtime enforcement techniques for supporting adaptive IEC 61499 applications. This set of techniques can modify the runtime behaviour of a system according to specific requirements. Our approach begins with specifying the requirements as a state machine-based notation called contract automaton. This automaton is then used to synthesise an enforcer as an FB. Finally, the new FB is integrated into the application to execute according to the requirements. A tool support is developed to automate the approach. Experiments were performed to evaluate the performance of enforcers by measuring the execution time of several applications before and after the integration of enforcers. [ABSTRACT FROM AUTHOR]

Runtime Enforcement (RE) is a technique aimed at monitoring the executions of a system at runtime and ensure its compliance against a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. All of our results are formalized and proved. We also analyze probabilistically how much memory is required on an average case for a given regular property, such that the output of the bounded enforcer is equal to that of the unbounded enforcer up to a fixed probability. The proposed framework is implemented and a case study is worked out to show the practicability and usefulness of the bounded enforcer in the real-world and to show the usage of the aforementioned probabilistic analysis on them. The performance is evaluated via some examples from application scenarios and it indicates linear changes in the execution time of the enforcers in response to increases in trace length, property complexity, and buffer sizes. [ABSTRACT FROM AUTHOR]

The security of Cyber-Physical Systems (CPSs) is increasingly important as more and more of these systems are added to the Internet of Things (IoT). As we increase the complexity and connectivity of our smart systems, we likewise broaden their digital attack surface. Recorded attacks on CPSs have caused significant physical impacts making methods for mitigation of attacks of paramount importance. The use of runtime enforcement (RE) can prevent violation of security policies. Here, runtime enforcers intervene before the CPS is compromised. Two key challenges are presented: (1) for complex systems, methods for automatically composing multiple policies are lacking; and (2) runtime enforcers are themselves executed digitally—meaning they too could have potential security vulnerabilities. We present the first comprehensive runtime enforcement framework which addresses both challenges. It can compose a lot of security policies in parallel and synthesize these policies into the more trustworthy hardware layers of a system. This removes reliance on potentially vulnerable firmware and software layers. We demonstrate our approach with policies to mitigate a set of attacks on a Fused Filament Fabrication (FFF) 3D printer. The experimental results show linear growth in logic element and register usage as the number of policies increase. This compares favourably to the exponential state space explosion that occurs with the conventional approach of monolithic composition. Additionally, we find higher enforcer clock frequencies are possible with the proposed parallel approach compared to existing serial approaches.

Besides the recent impressive results on reinforcement learning (RL), safety is still one of the major research challenges in RL. RL is a machine-learning approach to determine near-optimal policies in Markov decision processes (MDPs). In this paper, we consider the setting where the safety-relevant fragment of the MDP together with a temporal logic safety specification is given, and many safety violations can be avoided by planning ahead a short time into the future. We propose an approach for online safety shielding of RL agents. During runtime, the shield analyses the safety of each available action. For any action, the shield computes the maximal probability to not violate the safety specification within the next k steps when executing this action. Based on this probability and a given threshold, the shield decides whether to block an action from the agent. Existing offline shielding approaches compute exhaustively the safety of all state-action combinations ahead of time, resulting in huge computation times and large memory consumption. The intuition behind online shielding is to compute at runtime the set of all states that could be reached in the near future. For each of these states, the safety of all available actions is analysed and used for shielding as soon as one of the considered states is reached. Our approach is well-suited for high-level planning problems where the time between decisions can be used for safety computations and it is sustainable for the agent to wait until these computations are finished. For our evaluation, we selected a 2-player version of the classical computer game Snake. The game represents a high-level planning problem that requires fast decisions and the multiplayer setting induces a large state space, which is computationally expensive to analyse exhaustively. [ABSTRACT FROM AUTHOR]

Cyber-Physical attacks (CP-attacks) are launched either from the cyber-space or from the physical-space to take control of a Cyber-Physical System (CPS). Unlike conventional cyber-attacks, which are prevented through new security patches as new attacks emerge, there are no known mechanisms for incrementally patching CPS in the event of new attacks. To this end, we develop a novel approach based on recent advances in mitigating CP-attacks using run-time enforcement (RE). RE-methods have been developed for CPS, such as industrial processes and pacemakers. However, the proposed solutions are not developed considering the need for future patching as new attacks emerge. To this end, we develop the first compositional RE framework, which is specifically developed to be able to add new security patches as new security policies are added. We illustrate our approach using the case study of a drone swarm. The experimental results show that the proposed compositional/incremental approach does not suffer from the state space explosion, unlike the monolithic composition. We demonstrate a linear relationship between compile time, compile size, and execution time as the number of policies increases in the proposed compositional scheme.

With the advent of Industry 4.0, industrial facilities and critical infrastructures are transforming into an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, increasingly interconnected and therefore exposed to cyber-physical attacks, i.e., security breaches in cyberspace that may adversely affect the physical processes underlying industrial control systems. In this article, we propose a formal approach based on runtime enforcement to ensure specification compliance in networks of controllers, possibly compromised by colluding malware that may locally tamper with actuator commands, sensor readings, and inter-controller communications. Our approach relies on an adhoc sub-class of Ligatti et al.'s edit automata to enforce controllers represented in Hennessy and Regan's Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and a timed correctness property e, 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 do mitigation by correcting and suppressing incorrect actions of corrupted controllers and by generating actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical requirements, such as transparency and soundness, the proposed enforcement enjoys deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers. Finally, we test the proposed enforcement mechanism on a non-trivial case study, taken from the context of industrialwater treatment systems, in which the controllers are injected with different malware with different malicious goals. [ABSTRACT FROM AUTHOR]

Message-based systems usually consist of distributed components that communicate using asynchronous message passing. In such systems, particular message orderings may violate some required properties. Given an automata-based specification of unwanted message sequences, we propose a decentralized deadlock-free runtime enforcement algorithm to prevent the formation of such sequences. In our approach, components are equipped with monitors executed concurrently. A component is only blocked before sending or receiving the last message of a sequence, until its associated monitor checks that such a message does not complete an unwanted sequence. According to the specification of unwanted sequences, some blocked components may suffer from a deadlock. Our deadlock-free algorithm guarantees that monitors detect and resolve such deadlocks by improving the existing deadlock detection algorithms. We evaluate the efficiency and scalability of our approach in terms of the communication overhead, the prevention latency, and the overhead of deadlock detection through simulation. [ABSTRACT FROM AUTHOR]

Runtime enforcement is a methodology used to enforce that the output of a running system satisfies a desired property. Given a property, an enforcement monitor modifies an (untrusted) sequence of events into a sequence that complies to that property. In practice, we may have not one, but many properties to enforce. Moreover, new properties may arise as new capabilities are added to the system. It is thus important to construct not a single, i.e., monolithic monitor, but rather several monitors, one for each property. The question is to what extent such monitors can be composed, and how. In this paper, we study two enforcement monitor composition schemes, serial and parallel composition. We show that, runtime enforcement is compositional for general regular properties with respect to one of the parallel composition schemes defined. We also show that runtime enforcement is not compositional with respect to serial composition for general regular properties, but it is for certain subclasses of regular properties. The proposed compositional runtime enforcement framework is formalized and implemented. Our experimental results demonstrate the pros and cons of using the compositional approach versus the monolithic with respect to performance. [ABSTRACT FROM AUTHOR]

• Timed process calculi for expressing both genuine and malicious activities within a PLC. • Runtime enforcement based on Ligatti et al.'s edit automata. • Algorithms to synthesise edit automata from PLC specifications. • Simulation and bisimulation proof techniques. • Simulations of a significant use case in Simulink/Matlab. 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 compliance at runtime. We define a synthesis algorithm that given an uncorrupted 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 activities. 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. [ABSTRACT FROM AUTHOR]

Runtime enforcement and control system synthesis are two verification techniques that automate the process of transforming an erroneous system into a valid one. As both techniques can modify the behaviour of a system to prevent erroneous executions, they are both ideal for ensuring safety. In this paper, we investigate the interplay between these two techniques and identify control system synthesis as being the static counterpart to suppression-based runtime enforcement, in the context of safety properties. [ABSTRACT FROM AUTHOR]

Robotic swarms are usually designed in a bottom-up way, which can make robotic swarms vulnerable to environmental impact. It is particularly true for the widely used control mode of robotic swarms, where it is often the case that neither the correctness of the swarming tasks at the macro level nor the safety of the interaction among agents at the micro level can be guaranteed. To ensure that the behaviors are safe at runtime, it is necessary to take into account the property guard approaches for robotic swarms in uncertain environments. Runtime enforcement is an approach which can guarantee the given properties in system execution and has no scalability issue. Although some runtime enforcement methods have been studied and applied in different domains, they cannot effectively solve the problem of property enforcement on robotic swarm tasks at present. In this paper, an enforcement method is proposed on swarms which should satisfy multi-level properties in uncertain environments. We introduce a macro-micro property enforcing framework with the notion of agent shields and a discrete-time enforcing mechanism called D-time enforcing. To realize this method, a domain specification language and the corresponding enforcer synthesis algorithms are developed. We then apply the approach to enforce the properties of the simulated robotic swarm in the robotflocksim platform. We evaluate and show the effectiveness of the method with experiments on specific unmanned aerial vehicle swarm tasks. [ABSTRACT FROM AUTHOR]

Many implantable medical devices, such as pacemakers, have been recalled due to failure of their embedded software. This motivates rethinking their design and certification processes. We propose, for the first time, an additional layer of safety by formalising the problem of run-time enforcement of implantable pacemakers. While recent work has formalised run-time enforcement of reactive systems, the proposed framework generalises existing work along the following directions: (1) we develop bi-directional enforcement, where the enforced policies depend not only on the status of the pacemaker (the controller) but also of the heart (the plant), thus formalising the run-time enforcement problem for cyber-physical systems (2) we express policies using a variant of discrete timed automata (DTA), which can cover all regular properties unlike earlier frameworks limited to safety properties, (3) we are able to ensure the timing safety of implantable devices through the proposed enforcement, and (4) we show that the DTA-based approach is efficient relative to its dense time variant while ensuring that the discretisation error is relatively small and bounded. The developed approach is validated through a prototype system implemented using the open source KIELER framework. The experiments show that the framework incurs minimal runtime overhead. [ABSTRACT FROM AUTHOR]

Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ensures that the sequence complies with a certain property, by delaying or modifying events if necessary. This paper deals with predictive runtime enforcement, where the system is not entirely black-box, but we know something about its behavior. This a priori knowledge about the system allows to output some events immediately, instead of delaying them until more events are observed, or even blocking them permanently. This in turn results in better enforcement policies. We also show that if we have no knowledge about the system, then the proposed enforcement mechanism reduces to standard (non-predictive) runtime enforcement. All our results related to predictive RE of untimed properties are also formalized and proved in the Isabelle theorem prover. We also discuss how our predictive runtime enforcement framework can be extended to enforce timed properties. [ABSTRACT FROM AUTHOR]

We introduce runtime enforcement of specifications on component-based systems (CBS) modeled in the behavior, interaction and priority (BIP) framework. Runtime enforcement is an increasingly popular and effective dynamic validation technique aiming to ensure the correct runtime behavior (w.r.t. a formal specification) of a system using a so-called enforcement monitor. BIP is a powerful and expressive component-based framework for the formal construction of heterogeneous systems. Because of BIP expressiveness, however, it is difficult to enforce complex behavioral properties at design-time. We first introduce a theoretical runtime enforcement framework for component-based systems where we delineate a hierarchy of enforceable properties (i.e., properties that can be enforced) according to the number of observational steps a system is allowed to deviate from the property (i.e., the notion of k-step enforceability). To ensure the observational equivalence between the correct executions of the initial system and the monitored system, we show that (i) only stutter-invariant properties should be enforced on CBS with our monitors, and (ii) safety properties are 1-step enforceable. Second, given an abstract enforcement monitor for some 1-step enforceable property, we define a series of formal transformations to instrument (at relevant locations) a CBS described in the BIP framework to integrate the monitor. At runtime, the monitor observes and automatically avoids any error in the behavior of the system w.r.t. the property. Third, our approach is fully implemented in RE-BIP, an available tool integrated in the BIP tool suite. Fourth, to validate our approach, we use RE-BIP to (i) enforce deadlock-freedom on a dining philosophers benchmark, and (ii) ensure the correct placement of robots on a map. [ABSTRACT FROM AUTHOR]

Runtime enforcement is a verification/validation technique aiming at correcting possibly incorrect executions of a system of interest. In this paper, we consider enforcement monitoring for systems where the physical time elapsing between actions matters. Executions are thus modelled as timed words (i.e., sequences of actions with dates). We consider runtime enforcement for timed specifications modelled as timed automata. Our enforcement mechanisms have the power of both delaying events to match timing constraints, and suppressing events when no delaying is appropriate, thus possibly allowing for longer executions. To ease their design and their correctness-proof, enforcement mechanisms are described at several levels: enforcement functions that specify the input–output behaviour in terms of transformations of timed words, constraints that should be satisfied by such functions, enforcement monitors that describe the operational behaviour of enforcement functions, and enforcement algorithms that describe the implementation of enforcement monitors. The feasibility of enforcement monitoring for timed properties is validated by prototyping the synthesis of enforcement monitors from timed automata. [ABSTRACT FROM AUTHOR]

We are interested in the validation of opacity. Opacity models the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker. More specifically, we study how we can model-check, verify and enforce at system runtime, several levels of opacity. Besides existing notions of opacity, we also introduce K-step strong opacity, a more practical notion of opacity that provides a stronger level of confidentiality. [ABSTRACT FROM AUTHOR]

This paper presents a theory of runtime enforcement based on mechanism models called mandatory results automata (MRAs). MRAs can monitor and transform security-relevant actions and their results. The operational semantics of MRAs is simple and enables straightforward definitions of concrete MRAs. Moreover, the definitions of policies and enforcement with MRAs are simple and expressive. Putting all of these features together, we argue that MRAs make good general models of runtime mechanisms, upon which a theory of runtime enforcement can be based. We develop some enforceability theory by characterizing the policies deterministic and non-deterministic MRAs can and cannot enforce. [ABSTRACT FROM AUTHOR]