Verification of Approximate Opacity via Barrier Certificates

This paper is motivated by the increasing security concerns of cyber-physical systems. Here, we develop a discretization-free verification scheme targeting an information-flow security property, called approximate initial-state opacity, for the class of discrete-time control systems. We propose notions of so-called augmented control barrier certificates in conjunction with specified regions of interest capturing the initial and secret sets of the system. Sufficient conditions for (the lack of) approximate initial-state opacity of discrete-time control systems are proposed based on the existence of the proposed barrier certificates. We further present an efficient computation method by casting the conditions for barrier certificates as sum-of-squares programming problems. The effectiveness of the proposed results is illustrated through two numerical examples.