Opacity From Observers With a Bounded Memory
Opacity From Observers With a Bounded Memory
复制标题
DOI：
10.1109/lcsys.2023.3286777
复制
发表时间：
2023
影响因子：
3
通讯作者：
Andrew Wintenberg;S. Lafortune;N. Ozay
中科院分区：
文献类型：
--
作者：
Andrew Wintenberg;S. Lafortune;N. Ozay
不透明度是一种信息流属性，它从知道系统动态的观察者那里捕获隐私。拥有完美记忆力的观察者可能会对该系统的长期历史进行推理，这对不透明的核实构成了挑战。在这封信中，我们通过提出自动机上的不透明度的新概念来解决这一挑战，称为有界内存不透明度，相对于具有有界内存的观察者。我们表明，与一般的不透明度(co-NP与PSPACE)相比，验证这一较弱的不透明度概念降低了计算复杂性。此外，针对布尔可满足性问题(SAT)，给出了相应的编码验证算法。我们在随机生成的自动机上演示了该方法，并给出了一个Web服务器负载隐藏的例子。
Opacity is an information-flow property capturing privacy from observers that are aware of a system’s dynamics. The potential for an observer with perfect recall to reason about long histories of the system poses a challenge for opacity verification. In this letter, we address this challenge by proposing a new notion of opacity over automata, called bounded memory opacity, with respect to an observer with a bounded memory. We show that verifying this weaker notion of opacity has reduced computational complexity compared to general opacity (co- NP vs. PSPACE). Furthermore, we present a corresponding verification algorithm using an encoding to the Boolean satisfiability problem (SAT). We demonstrate this approach on randomly generated automata as well as a Web server load-hiding example.