Current-state Opacity Enforcement Based On Petri Nets

Networks are one of the important factors to promote the continuous development of today's society,and the significance of network security is becoming more and more prominent.Opacity is a vital feature of network security.For a discrete event system,the system is transparent when secret states that need to be hidden are known to an external intruder.At this time,an external intruder can launch attacks,and the security of the system is threatened.Therefore,it is of great academic value and engineering significance to transform a transparent system into an opaque system to guarantee network security.Petri nets are a powerful mathematical tool,which can be used to describe the system conflict,concurrency,resource sharing and other characters.As a logical level model,automata use a state transition diagram to show the relationship between the states and events clearly and intuitively.In this thesis,Petri nets and automata are used as modeling tools of a discrete event system.The main contributions of this thesis are as follows:1.Deadlocks often occur when the current state is forced to be opaque in a labeled Petri net.Therefore,a supervisory control model is designed to solve deadlocks.The model consists of a discrete event system,a labeled function,a synthetic state estimator,and a supervisor.First,sequences generated by the labeled Petri net can generate observable event sequences through the labeled function.Then,the synthetic state estimator estimates current states according to the observable event sequences.Finally,a supervisor is designed to dynamically enable or disable controllable events based on current estimation states such that the controlled system does not reach forbidden states,and the supervisor avoids the labeled Petri net deadlocks while enforcing current state opacity.2.Based on the newly designed supervisory control model in a labeled Petri net,the concept of enforcing current state opacity in a labeled Petri net is proposed,and the solution to this problem and relevant proof are given.The definitions of forbidden states and pseudo secret markings are proposed.This thesis presents an algorithm to construct a synthetic state estimator,which can deduce the possible current states.Forcing current state opacity with the basis reachability graph reduces the number of reachable states that need to be calculated,which reduces space complexity and improves the computing efficiency.3.In an automaton model,a new method is proposed to enforce the current state opacity.This method synthesizes locally optimal supervisors on the premises that the relationship between intruder's observable events and supervisor's observable events is equal,mutually inclusive,or unrelated,which renders it a wide applicability.First,an augment intruder observer is constructed for the states of the automaton itself through the new method.Then,a total controller is constructed using the states of the augment intruder observer,and the states that contain secrets and those that may reveal secrets are deleted from the total controller.Finally,maximum control decisions are obtained and combined to derive a local optimal supervisor.The approach proposed in this thesis not only removes the states that contain secrets,but also removes those that might reveal secrets,thus making the system-generated language more secure.