Observation Structures and Opacity Problems in Discrete Event Systems

Security is one of the most important properties of systems such as Internet of things, communication networks, and computer systems. In these systems, some information (called secret) should not be corrupted or acquired by unauthorized people (called intruders). In recent years many notions of secrecy have been formulated. Among them, opacity formalizes the impossibility for an intruder to infer the truth of the secret based on its observation. In discrete event systems (DESs), depending on the definition of secret, opacity is categorized as current-state opacity, initial-state opacity, and language-based opacity. This thesis focuses on the observation structures and opacity problems in DESs. The main results of this research are briefed as follows. 1. In This thesis we propose two more general classes of Petri nets: labeled Petri nets with outputs and adaptive labeled Petri nets. Compared with other Petri net models, the two classes of generators generally have the highest modeling power. Looking for bridges between the different formalisms, we also present general procedures for the transformation between models and algorithms to convert one structure into another one if possible. 2. Current-state opacity, initial-state opacity and language-based opacity are formally defined in the framework of Petri nets. Then we study their differences between the opacity properties in automata. Moreover, we generalize the notion of language opacity to strict language opacity to deal with the case where the intruder is only interested in a subset of transitions. 3. It has been shown that current-state, initial-state and language opacity verification problems are decidable in finite systems. However, the decidability of current-state, initial-state and language opacity verification problems in Petri net systems still requires further investigation.In the thesis, we prove that this problems in Petri net systems are undecidable. Therefore, one can focus on the opacity verification problems in bounded Petri net systems. 4. For bounded systems, the existing methods of verifying opacity require enumeration of the set of states consistent with an observation. Based on the notion of basis markings, we propose a practically efficient approach to verifying current-state opacity and initialstate opacity. Using the proposed approach, the exhaustive enumeration of the state space can be avoided but only a small number of basis markings. All other markings can be represented by a set of linear systems. By solving the integer linear programming problems, current-state and initial-state opacity can be verified. Moreover, a structure, called verifier, is constructed to analyze strict language opacity. Given the nets modeling the plant and the secret, the verifier synchronizes the plant and the secret keeping tracks of both sequences belonging to and not belonging to the secret. In particular, thanks to the notion of minimal explanations there is no need to enumerate all the secret/non-secret sequences. 5. Finally, given a system modeled with a finite automaton that is not current-state opaque with respect to a given secret, we propose an approach to designing an optimal supervisor that restricts the behavior of the system to ensure current-state opacity of the controlled system. In other works, it is usually assumed that the set of events observable by the intruder is included in the set of events observable by the supervisor, or vice versa. Clearly, such an inclusion relation may not hold in general. Therefore, in the thesis, we consider the case where the two sets of events are incomparable. A new structure, called augmented I-observer, is defined to compute the supremal sublanguage generated by the system that will not leak the secret. Based on the augmented I-observer, a set of locally optimal supervisors can be synthesized such that the controlled system is maximally permissive and current-state opaque with respect to the given secret.