Observation Structures And Opacity Problems In Discrete Event Systems

Security is one of the most important properties of systems such as Internet of things,com-munication networks,and computer systems.In these systems,some information(called secret)should not be corrupted or acquired by unauthorized people(called intruders).Mo-tivated by the concern of information security,in recent years many notions of secrecy have been formulated,such as non-inference,anonymity,and opacity,etc.Among them,opacity is proven capable of formulating some other security properties:for instance,non-inference and anonymity.Opacity formalizes the absence of information flow,or more precisely,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 usually cat-egorized as current-state opacity,initial-state opacity,and language-based opacity.Limited by the sensors or communication,the evolution of a system may not be completely detected by outsiders,including the intruder.Thus,it is important to have powerful DES models that are capable of describing different observation structures of systems.Mean-while,due to the state explosion problem,opacity analysis through enumerating all states is not applicable to large scale systems.It is necessary to develop more effective verification algorithms.Finally,given a system that is not opaque,another problem is how to design controllers restricting the behavior of the system such that the controlled system is opaque and maximally permissive.This thesis focuses on the observation structures and opacity problems in DESs.The main results of this research are briefed as follows.1.Petri nets are a graphical and mathematical tool applicable to many systems and a promising tool for describing and studying DESs.We propose two more general classes of Petri nets:labeled Petri nets with outputs(LPNOs)and adaptive labeled Petri nets(ALPNs),to better formalize and generalize current Petri net observation structures.Compared with other Petri net models,the two classes of generators gen-erally have the highest modeling power.Looking for bridges between the different formalisms,we also present general procedures for the transformation between mod-els 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 opac-ity 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 re-quires further investigation.In the thesis,we prove that current-state,initial-state and language opacity verification problems in Petri net systems are undecidable.Namely,there is no general algorithm that gives a correct answer to the question whether a giv-en Petri net system is current-state(or initial-state,or language)opaque with respect to a given secret or not.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.Obviously,for large scale systems the state explosion problem is unavoidable.Based on the notion of basis markings,we propose a practically efficient approach to verifying current-state opacity and initial-state 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 program-ming 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 se-cret 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.Therefore,the proposed approach is more efficient than other methods.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 super-visor 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 observ-able 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 sublan-guage 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 con-trolled system is maximally permissive and current-state opaque with respect to the given secret.Finally,contributions of the thesis are summarized as conclusions,and future research on observation structures of Petri nets and opacity problems in DESs is prospected.