Opacity Verification Method For Control System Via Deep Learning

In recent years,cyber-physical systems have been widely used in safety critical infrastructure such as intelligent robots,medical equipment and autonomous vehicle.However,the tight interaction between embedded control software and physical processes may release privacy information and expose the system to intruders.Therefore,protecting the security and privacy of cyber-physical systems have become an increasingly important issue.Opacity is an important information security property of cyber-physical systems.It can evaluate the system’s ability to hide its privacy information from any intruder and ensure that the system’s privacy information will not be disclosed.For security-critical cyber-physical systems,it is essential to ensure and verify the opacity of the system.Therefore,this paper studies the problem of approximate initial-state opacity verification and opacity controller generation for discrete-time control systems.Unlike the existing numerical calculation method based on the sum of squares,this paper adopts the data-driven method based on deep learning and counterexample guidance.In detail,the following work has been done:(1)This paper presents a method based on an improved augmented barrier certificate(IABC)to formalize the approximate initial-state opacity of discrete time control systems.The opacity verification problem is expressed as the security verification problem of the augmented system and solved by searching for barrier certificates.First,the IABC is defined to verify the opacity of the approximate initial state.And the iterative framework for the interaction of Learner and Verifier is designed.Learner trains IABC through deep learning,and Verifier solves a set of mixed integer linear programming problems to ensure the effectiveness of candidate IABC or produce counterexamples to refine candidate IABC.Experiments show that the proposed method is scalable and effective compared with the existing sum of squares programming method.(2)In this paper,an Improved Augmented Control Barrier Certificate(IACBC)based method for generating opacity controllers is proposed.Firstly,IABC is relaxed reasonably based on inductive proof method and the definition of IACBC is given.Then,the opaque controller is generated by iterative generation,where Learner trains the opaque controller and IACBC simultaneously through deep learning.Verifier solves a set of mixed integer linear programming problems,and the optimal solution of the optimization problem satisfies the condition proof that the generated opacity controller can ensure that the system satisfies the approximate initial state opacity.If the optimal solution does not meet the conditions,the counter-example is generated for counter-example guidance training.Experimental results show the effectiveness of this method.