Verification of Approximate Opacity via Barrier Certificates

TL;DR

This paper introduces a discretization-free verification method using barrier certificates to assess approximate initial-state opacity in discrete-time control systems, enhancing security analysis without discretization.

Contribution

It develops augmented control barrier certificates and a sum-of-squares programming approach for verifying approximate opacity, a novel security property in cyber-physical systems.

Findings

Effective verification of approximate initial-state opacity demonstrated.

Sum-of-squares programming enables efficient computation.

Numerical examples validate the proposed method.

Abstract

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.