论文标题
验证开关系统的初始状态不透明度：一种组成方法
Verification of Initial-State Opacity for Switched Systems: A Compositional Approach
论文作者
论文摘要
信息流的安全已成为网络物理系统（CPSS）的主要关注点。在这项工作中，我们专注于对信息流安全属性的分析，称为不透明度。不透明度是在存在恶意外部入侵者存在下，系统秘密的合理可否认性。我们提出了一种检查离散时间交换系统网络的不透明度概念的方法，称为近似初始状态不透明度。我们的框架依赖于开关系统网络的有限抽象及其所谓的近似初始状态不透明的模拟函数（InitSOPSFS）的组成结构。这些功能表征了混凝土网络及其有限抽象的方式，这是对近似初始状态不透明度的满意度。我们表明，可以通过假设一些小增益型条件并分别组成为每个子系统构建的所谓局部InitsOPSF来从组合上获得这种InitSOPSF。此外，假设开关系统的某些稳定性属性，我们还提供了一种技术，可以与相应的本地InitsOPSF一起构建其有限抽象。最后，我们通过一个示例说明了结果的有效性。
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.
