Verification of Initial-State Opacity for Switched Systems: A Compositional Approach

TL;DR

This paper presents a compositional method for verifying approximate initial-state opacity in networks of discrete-time switched systems, using finite abstractions and simulation functions to ensure security properties against intruders.

Contribution

It introduces a novel compositional framework for constructing finite abstractions and simulation functions to verify opacity in switched systems, leveraging small-gain conditions and stability assumptions.

Findings

Successfully verifies approximate initial-state opacity in complex switched systems.

Provides a systematic way to construct finite abstractions and simulation functions.

Demonstrates effectiveness through a detailed example.

Abstract

The security in information-flow has become a major concern for cyber-physical systems (CPSs). In this work, we focus on the analysis of an information-flow security property, called opacity. Opacity characterizes the plausible deniability of a system's secret in the presence of a malicious outside intruder. We propose a methodology of checking a notion of opacity, called approximate initial-state opacity, for networks of discrete-time switched systems. Our framework relies on compositional constructions of finite abstractions for networks of switched systems and their so-called approximate initial-state opacity-preserving simulation functions (InitSOPSFs). Those functions characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate initial-state opacity. We show that such InitSOPSFs can be obtained compositionally by assuming some small-gain type conditions and composing so-called local InitSOPSFs constructed for each subsystem separately. Additionally, assuming certain stability property of switched systems, we also provide a technique on constructing their finite abstractions together with the corresponding local InitSOPSFs. Finally, we illustrate the effectiveness of our results through an example.