具有主动入侵的离散事件系统的不透明性
Opacity of Discrete Event Systems with Active Intruder
摘要：
不透明度是一种安全属性，它形式化地描述了系统对外部观察者（即入侵者）的信息泄漏。离散事件系统（DES）文献中研究的传统不透明性通常假设被动入侵者，他们只观察系统的行为。然而，在许多网络安全问题，如Web服务，主动入侵者，谁能够影响系统的行为超出被动的观察，需要考虑和防御。因此，我们有动机扩展不透明的概念来处理主动入侵者。为此，我们将系统建模为非确定性有限状态换能器。假设入侵者对系统结构有充分的了解，并且能够通过注入不同的输入并观察其响应来与系统进行交互。在这种设置中，我们首先引入反应性当前状态不透明度（RCSO）的概念，其特征在于系统不泄漏其秘密状态，无论入侵者如何操纵系统的行为。我们进一步扩展这个概念，以语言为基础的和初始状态的反应不透明的概念，并研究它们之间的关系。结果表明，所有提出的反应不透明度概念都等价于RCSO。因此，我们专注于RCSO和研究其验证问题。它表明，RCSO可以通过构造一个观察者自动机进行验证。
英文摘要：
Opacity is a security property formalizing the information leakage of a system to an external observer, namely intruder. The conventional opacity that has been studied in the Discrete Event System (DES) literature usually assumes passive intruders, who only observe the behavior of the system. However, in many cybersecurity concerns, such as web service, active intruders, who are capable of influencing the system's behavior beyond passive observations, need to be considered and defended against. We are therefore motivated to extend the opacity notions to handle active intruders. For this, we model the system as a non-deterministic finite-state transducer. It is assumed that the intruder has a full knowledge of the system structure and is capable of interacting with the system by injecting different inputs and observing its responses. In this setup, we first introduce reactive current-state opacity (RCSO) notion characterizing a property that the system does not leak its secret state regardless of how the intruder manipulates the system behavior. We furthermore extend this notion to language-based and initial-state reactive opacity notions, and study the relationship among them. It turns out that all the proposed reactive opacity notions are equivalent to RCSO. We therefore focus on RCSO and study its verification problem. It is shown that the RCSO can be verified by constructing an observer automaton.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
