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.
翻译:在本文中,我们考虑了核实离散时间控制系统前不透明前的问题。不透明前是一个重要的信息流通安全属性,它确保了系统在未来实施某些秘密行为的意向。关于不透明前的现有工作仅考虑非计量离散系统,假设入侵者可以精确地区分不同输出行为。然而,对于输出组配备了计量标准的连续空间控制系统(大多数现实应用都如此),它过于严格,无法从外部观察者那里进行精确的测量。在本文中,我们首先引入了近似不透明前安全属性的概念,通过捕捉控制系统的安保水平来保证入侵者今后实施某些秘密行为的准确性。根据这种新的不透明前系统概念,我们建议对连续空间控制系统进行核查,利用基于抽象的技术。特别是,对具有近似不透明前保存模拟关系的连续空间控制系统的新概念,从保存前不透明的角度来描述两个系统之间的距离。在本文中,我们首先通过获取控制入侵前控制系统的安全性概念,首先可以核查控制入侵系统的安全程度。根据这种新的概念,我们还在使用某种不断稳定系统之前的精确系统,然后进行某种稳定。