论文标题
在动态信息释放机制下，当前状态不透明度的框架
A Framework for Current-State Opacity under Dynamic Information Release Mechanism
论文作者
论文摘要
不透明度是一个重要的信息流安全性属性，它表征了动态系统的合理可否认性，以防止窃听攻击。作为信息流属性，基础观察模型是不透明度建模和分析的关键。在本文中，我们调查了在奥威尔式型观测值下对离散事件系统的当前状态不透明度的验证，即允许该系统根据其未来后缀重新解释事件的观察。首先，我们提出了一个新的奥威尔式观察模型，称为动态信息释放机制（DIRM）。在Dirm中，何时发布以前的“持有”事件是状态依赖性的。然后，我们基于历史等效性的概念而不是标准投影等效性提出了一个新的不透明度定义。该定义更适合于未封闭前缀封闭的观测值。最后，我们表明，通过构建一个称为Dirm-Observer的新结构，可以在Dirm下有效验证当前状态的不透明度。还提供了所提出方法的计算复杂性分析以及说明性示例。与现有的奥威尔式观察模型相比，在信息释放机制是状态依赖性的，并且不透明度的相应定义更适合于非排名封闭的观察结果，因此所提出的框架更为笼统。
Opacity is an important information-flow security property that characterizes the plausible deniability of a dynamic system for its "secret" against eavesdropping attacks. As an information-flow property, the underlying observation model is the key in the modeling and analysis of opacity. In this paper, we investigate the verification of current-state opacity for discrete-event systems under Orwellian-type observations, i.e., the system is allowed to re-interpret the observation of an event based on its future suffix. First, we propose a new Orwellian-type observation model called the dynamic information release mechanism (DIRM). In the DIRM, when to release previous "hold on" events is state-dependent. Then we propose a new definition of opacity based on the notion of history-equivalence rather than the standard projection-equivalence. This definition is more suitable for observations that are not prefix-closed. Finally, we show that by constructing a new structure called the DIRM-observer, current-state opacity can be effectively verified under the DIRM. Computational complexity analysis as well as illustrative examples for the proposed approach are also provided. Compared with the existing Orwellian-type observation model, the proposed framework is more general in the sense that the information-release-mechanism is state-dependent and the corresponding definition of opacity is more suitable for non-prefix-closed observations.
