动态信息发布机制下的当前状态不透明度框架
A Framework for Current-State Opacity under Dynamic Information Release Mechanism
摘要：
不透明性是一个重要的信息流安全属性，它表征了动态系统对窃听攻击的“秘密”的合理可否认性。作为一种信息流属性，底层观测模型是不透明度建模和分析的关键。在本文中，我们研究了在Orwell型观测下离散事件系统的当前状态不透明性的验证，即，允许系统基于其未来后缀重新解释事件的观测。首先，我们提出了一个新的奥威尔式的观察模型称为动态信息发布机制（DIRM）。在DIRM中，何时释放先前的“保持”事件取决于状态。然后，我们提出了一个新的定义的不透明度的概念的基础上的历史等价，而不是标准的投影等价。此定义更适合于非前缀闭合的观测。最后，我们表明，通过构建一个新的结构称为DIRM观察者，当前状态的不透明性可以有效地验证下的DIRM。计算复杂性分析以及说明性的例子，所提出的方法也提供。与现有的Orwell型观测模型相比，该框架具有更一般的意义，即信息发布机制是状态依赖的，相应的不透明度定义更适合于非前缀闭观测。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
