应用于不透明性验证与综合的增量式观测器约简
计算机科学中的逻辑
2019-10-15 v3
摘要
随着通信网络与移动设备的普及,其信息流中的隐私与安全问题日益凸显。给定一个可能泄露机密信息的临界系统,问题在于通过设计监督器来验证并强制实施不透明性,以对未授权人员隐藏机密信息。为查明入侵者所见,需要构造系统的观测器。本文考虑模块化系统的增量式观测器生成,用于当前状态不透明性的验证与强制实施。子系统的同步会产生巨大的状态空间。此外,具有指数复杂度的观测器生成进一步增大了状态空间。为应对该复杂性问题,我们证明观测器生成可在子系统同步之前局部完成。与抽象方法相结合的增量局部观测器生成相比传统整体式方法显著降低了状态空间。增量方法中亦考虑了共享不可观测事件的存在。此外,我们给出一个说明性示例,其中在一个具有入侵者的模块化多层楼/电梯建筑上展示了当前状态不透明性的验证与强制实施结果。我们还将当前状态不透明性、当前状态匿名性以及基于语言的不透明性表述扩展至模块化系统的验证。
引用
@article{arxiv.1812.08083,
title = {Incremental Observer Reduction Applied to Opacity Verification and Synthesis},
author = {Mona Noori-Hosseini and Bengt Lennartson and Christoforos Hadjicostis},
journal= {arXiv preprint arXiv:1812.08083},
year = {2019}
}