具有主动入侵者的离散事件系统的不透明性
计算机科学中的逻辑
2020-07-30 v1 系统与控制
系统与控制
摘要
不透明性是一种安全属性，用于形式化系统向外部观察者（即入侵者）的信息泄露。离散事件系统（DES）文献中研究的常规不透明性通常假设入侵者为被动的，仅观察系统行为。然而，在许多网络安全问题中，例如 Web 服务，需要考虑并防御能够超越被动观察而影响系统行为的主动入侵者。因此我们受此驱动将不透明性概念扩展以处理主动入侵者。为此，我们将系统建模为非确定性有限状态转换器。假设入侵者完全知晓系统结构，并能够通过注入不同输入并观察其响应来与系统交互。在此设定下，我们首先引入反应式当前状态不透明性（RCSO）概念，刻画系统无论入侵者如何操纵系统行为均不泄露其秘密状态的属性。我们进一步将该概念扩展至基于语言和初始状态的反应式不透明性概念，并研究它们之间的关系。结果表明所有提出的反应式不透明性概念均等价于 RCSO。因此我们聚焦于 RCSO 并研究其验证问题。研究表明可通过构造观察者自动机来验证 RCSO。
引用
@article{arxiv.2007.14960,
title = {Opacity of Discrete Event Systems with Active Intruder},
author = {Alireza Partovi and Taeho Jung and Lin Hai},
journal= {arXiv preprint arXiv:2007.14960},
year = {2020}
}