Enforcement For Current-State Opacity Using Obfuscation Mechanisms In Discrete Event Systems

The extensive adoption of digital technology and network interconnectivity has spurred significant research activities in cyber-physical systems.Generally speaking,cyber-physical systems are composed of sensors,actuators,and storage devices that are connected via wire or wireless network.Some examples of cyber-physical systems are banking systems,civil aviation systems,logistics systems,and transportation systems.Security and privacy of cyber-physical systems are increasingly emphasized nowadays due to the fact that network infrastructures,which comprise the underlying mechanisms for exchanging information within these systems,can become compromised by curious or malicious entities.Cyber-physical systems can be regarded as discrete event systems thanks to the fact that information transformation is associated with the occurrence of events.Opacity is a confidentiality property that holds if certain secret behavior of a discrete event system,typically represented by a predicate,cannot be revealed under any system evolution.A well-known approach to check opacity is the construction of an observer.When opacity is violated,it can be enforced using obfuscation techniques,i.e.,by replacing observation sequences that lead to opacity violations with observation sequences that can be generated by system behavior that does not violate opacity(in real time as the system evolves).This thesis focuses on opacity enforcement in discrete event systems modeled with finite state automata by proposing an extended insertion mechanism and modification mech-anism in obfuscation techniques.More specifically,for a non-opaque system,in order to enforce opacity,we develop extend insertion policies based on the extended insertion mech-anism or modification policies based on the modification mechanism.The contributions of this thesis are summarized as follows.1.On opacity enforcement in discrete event systems modeled with finite state automa-ta,an extended insertion mechanism is proposed to enforce opacity in a practical manner to a wide class of systems by inserting symbols before and after an actual system output.We also introduce event insertion constraints on the way that only certain type of symbols can be inserted before and after an actual symbol generated by the system.For each case,we obtain a necessary and sufficient condition based on the construction of an appropriate verifier for opacity-enforceability using the proposed extended insertion mechanism and devise a pertinent extended insertion strategy.2.The enforcement of opacity for systems modeled by finite state automata using an extended insertion strategy under constraints on the way that symbols can be inserted before and after an actual symbol generated by the system(e.g.,constraints on the type,order,and number of inserted symbols)is investigated.More specifically,we consider inserted language constraints captured by the notion of(L_b,L_a)-enforceability,where L_bis the set of strings that can be inserted before an observed event,and L_ais the set of strings that can be inserted after an observed event.If L_band L_aare regular languages,a verifier is constructed to derive a necessary and sufficient condition for opacity enforceability,and also to formulate an extended insertion strategy(if viable).3.On opacity enforcement in discrete event systems modeled with finite state au-tomata,modification functions that are capable of replacing in real-time the output of the underlying system with another output are proposed,aiming to prevent the intruder from inferring the secret is presented.We study modification functions that are constrained,i.e.,they may not be able to modify certain outputs or they may have restrictions in how they modify a particular output.A system is said to be emc-enforceable if opacity can be enforced via modification functions under the given modification constraints.To verify whether a system is emc-enforceable,we construct a verifier,based on which a necessary and sufficient condition is obtained.If a system is emc-enforceable,we present an algorithm to compute a modification strategy based on the verifier to enforce opacity.For m-enforceability,a special case of emc-enforceability without constraints,two necessary and sufficient conditions to verify and enforce opacity with reduced complexity are presented,one based on a system estimator and the other based on a detector.