Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems

TL;DR

This paper introduces a new concept of approximate pre-opacity for control systems with metric outputs, and proposes an abstraction-based verification method to ensure security properties in continuous-space systems.

Contribution

It develops a novel abstraction-based approach and a new simulation relation for verifying approximate pre-opacity in control systems with metric outputs.

Findings

The proposed method effectively verifies approximate pre-opacity in continuous systems.

Finite abstractions can be constructed under stability assumptions.

The approach extends pre-opacity verification to more realistic measurement scenarios.

Abstract

In this paper, we consider the problem of verifying pre-opacity for discrete-time control systems. Pre-opacity is an important information-flow security property that secures the intention of a system to execute some secret behaviors in the future. Existing works on pre-opacity only consider non-metric discrete systems, where it is assumed that intruders can distinguish different output behaviors precisely. However, for continuous-space control systems whose output sets are equipped with metrics (which is the case for most real-world applications), it is too restrictive to assume precise measurements from outside observers. In this paper, we first introduce a concept of approximate pre-opacity by capturing the security level of control systems with respect to the measurement precision of the intruder. Based on this new notion of pre-opacity, we propose a verification approach for continuous-space control systems by leveraging abstraction-based techniques. In particular, a new concept of approximate pre-opacity preserving simulation relation is introduced to characterize the distance between two systems in terms of preserving pre-opacity. This new system relation allows us to verify pre-opacity of complex continuous-space control systems using their finite abstractions. We also present a method to construct pre-opacity preserving finite abstractions for a class of discrete-time control systems under certain stability assumptions.