基于HyperLTL模型检测技术的K步不透明性验证

任翔; 王子佩; 张佳慧; 韩晓光

doi:10.13364/j.issn.1672-6510.20240024

天津科技大学学报 ›› 2025, Vol. 40 ›› Issue (03) : 65 -71. DOI: 10.13364/j.issn.1672-6510.20240024

基于HyperLTL模型检测技术的K步不透明性验证

任翔, 王子佩, 张佳慧, 韩晓光

作者信息 +

Author information +

文章历史 +

PDF

摘要

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