基于 HyperLTL 模型检测技术的K 步不透明性验证
摘 要：不透明性是一种重要的信息流安全属性，用于表征不同动态系统中各种安全和隐私需求。在离散事件系统中，K 步不透明性刻画的是入侵者无法根据当前的输出观测序列确定系统是否在 K 个观测步之内曾访问过秘密状态。 HyperLTL 作为一种在形式化验证中表达信息流属性的工具，已被证明可以采用一个统一的 Kripke 结构分别验证初始状态不透明性、当前状态不透明性和无限步不透明性，但并未涉及 K 步不透明性。针对 HyperLTL 模型的 K 步不透明性验证问题，通过添加 Sink 状态释放了对原系统的限制性条件，进一步构造改进的 Kripke 结构并给出 K 步不透明性在 HyperLTL 中的判据，即验证原系统在 HyperLTL 语义下是否满足 K 步不透明性。
论文下载：