We formulate notions of opacity for cyberphysical systems modeled as discrete-time linear time-invariant systems. A set of secret states is @math -ISO with respect to a set of nonsecret states if, starting from these sets at time @math , the outputs at time @math are indistinguishable to an adversarial observer. Necessary and sufficient conditions to ensure that a secret specification is @math -ISO are established in terms of sets of reachable states. We also show how to adapt techniques for computing under-approximations and over-approximations of the set of reachable states of dynamical systems in order to soundly approximate k-ISO. Further, we provide a condition for output controllability, if @math -ISO holds, and show that the converse holds under an additional assumption. We extend the theory of opacity for single-adversary systems to the case of multiple adversaries and develop several notions of decentralized opacity. We study the following scenarios: i) the presence or lack of a centralized coordinator, and ii) the presence or absence of collusion among adversaries. In the case of colluding adversaries, we derive a condition for nonopacity that depends on the structure of the directed graph representing the communication between adversaries. Finally, we relax the condition that the outputs be indistinguishable and define a notion of @math -opacity, and also provide an extension to the case of nonlinear systems.
Enforcement of opacity using techniques from supervisory control was studied in @cite_3 @cite_15 . The authors of @cite_14 formulated an alternate method of opacity enforcement using insertion functions, which are entities that modify the output behavior of the system in order to keep a secret. The model-checking and verification of notions of opacity at run time in online setups was presented in @cite_37 . A scheme for the verification of opacity in DESs using two-way observers was proposed in @cite_22 . This enabled a unified framework to verify multiple notions of opacity. There is a large body of literature focused on developing techniques to compute overapproximations and underapproximations of sets of reachable states. These will usually depend on how the initial set of states is specified, including support functions @cite_23 , zonotopes @cite_11 , and ellipsoids @cite_12 . A method to compute overapproximations of reachable sets of states for linear systems with uncertain, time-varying parameters and inputs was presented in @cite_31 . The reader is referred to @cite_16 for a succinct presentation of some of the techniques used in computing reachable sets.
@cite_37 @cite_14 @cite_31 @cite_22 @cite_3 @cite_23 @cite_15 @cite_16 @cite_12 @cite_11
1976202267 2040603575 1994826906 2601738991 2064886960 2026019548 1975630497 1532859487
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 Opacity is a confidentiality property that characterizes whether a “secret” of a system can be inferred by an outside observer called an “intruder”. In this paper, we consider the problem of enforcing opacity in systems modeled as partially-observed finite-state automata. We propose a novel enforcement mechanism based on the use of insertion functions. An insertion function is a monitoring interface at the output of the system that changes the system’s output behavior by inserting additional observable events. We define the property of “i-enforceability” that an insertion function needs to satisfy in order to enforce opacity. I-enforceability captures an insertion function’s ability to respond to every system’s observed behavior and to output only modified behaviors that look like existing non-secret behaviors. Given an insertion function, we provide an algorithm that verifies whether it is i-enforcing. More generally, given an opacity notion, we determine whether it is i-enforceable or not by constructing a structure called the “All Insertion Structure” (AIS). The AIS enumerates all i-enforcing insertion functions in a compact state transition structure. If a given opacity notion has been verified to be i-enforceable, we show how to use the AIS to synthesize an i-enforcing insertion function. This paper presents a method for using set-based approximations to the Peano-Baker series to compute overapproximations of reachable sets for linear systems with uncertain, time-varying parameters and inputs. Alternative representations for sets of uncertain system matrices are considered, including matrix polytopes, matrix zonotopes, and interval matrices. For each representation, the computational efficiency and resulting approximation error for reachable set computations are evaluated analytically and empirically. As an application, reachable sets are computed for a truck with hybrid dynamics due to a gain-scheduled yaw controller. As an alternative to computing reachable sets for the hybrid model, for which switching introduces an additional overapproximation error, the gain-scheduled controller is approximated with uncertain time-varying parameters, which leads to more efficient and more accurate reachable set computations. Abstract In the context of security analysis for information flow properties, where a potentially malicious observer (intruder) tracks the observed behavior of a given system, infinite-step opacity (respectively, K -step opacity) holds if the intruder can never determine for sure that the system was in a secret state for any instant within infinite steps (respectively, K steps) prior to that particular instant. We present new algorithms for the verification of the properties of infinite-step opacity and K -step opacity for partially-observed discrete event systems modeled as finite-state automata. Our new algorithms are based on a novel separation principle for state estimates that characterizes the information dependence in opacity verification problems, and they have lower computational complexity than previously-proposed ones in the literature. Specifically, we propose a new information structure, called the two-way observer, that is used for the verification of infinite-step and K -step opacity. Based on the two-way observer, a new upper bound for the delay in K -step opacity is derived, which also improves previously-known results. In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events ? and an inquisitive user, called the adversary, observes a subset ?a of ?. The confidential information is the fact (when it is true) that the trace of the execution of G on ?* belongs to a regular set S ? ?*, called the secret. The secret S is said to be opaque w.r.t. G (respectively, G C) and ?a if the adversary cannot safely infer this fact from the trace of the execution of G (respectively, G C) on ?a*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G C and ?a . This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet ?a of the adversary and the set of events that the controller can disable are comparable. This work is concerned with the algorithmic reachability analysis of linear systems with constrained initial states and inputs. In this paper, we present a new approach for the computation of tight polyhedral over-approximations of the reachable sets of a linear system. The main contribution over our previous work is that it makes it possible to consider systems whose sets of initial states and inputs are given by arbitrary compact convex sets represented by their support functions. We first consider the discrete-time setting and then we show how our algorithm can be extended to handle continuous-time linear systems. Finally, the effectiveness of our approach is demonstrated through several examples. This paper describes the computation of reach sets for discrete-time linear control systems with time-varying coefficients and ellipsoidal bounds on the controls and initial conditions. The algorithms construct external and internal ellipsoidal approximations that touch the reach set boundary from outside and from inside. Recurrence relations describe the time evolution of these approximations. An essential part of the paper deals with singular discrete-time linear systems This work is concerned with the problem of computing the set of reachable states for linear time-invariant systems with bounded inputs. Our main contribution is a novel algorithm which improves significantly the computational complexity of reachability analysis. Algorithms to compute over and under-approximations of the reachable sets are proposed as well. These algorithms are not subject to the wrapping effect and therefore our approximations are tight. We show that these approximations are useful in the context of hybrid systems verification and control synthesis. The performance of a prototype implementation of the algorithm confirms its qualities and gives hope for scaling up verification technology for continuous and hybrid systems.