保护你的意图：离散事件系统中预不透明性概念研究

本文研究部分可观离散事件系统中一种重要的信息流安全性质——不透明性。我们考虑存在一个被动入侵者（窃听者），其知道系统的动态模型并能够利用所生成的信息流推断系统的某些“秘密”。若系统始终对其秘密保有合理的可否认性，则称该系统是不透明的。现有的不透明性概念仅将秘密视为当前正访问某些秘密状态或过去曾访问过某些秘密状态。本文从新的角度研究信息流安全，将系统的秘密视为其未来执行某些重要特定行为的意图。为此，我们提出一类称为预不透明性的新不透明性，刻画入侵者能否在系统实际访问秘密状态之前提前若干步预测该访问。根据入侵者的预测任务，我们提出两种具体的预不透明性：K步瞬时预不透明性与K步轨迹预不透明性，以明确该概念。对于每种预不透明性概念，我们给出充要条件以及有效的验证算法。预不透明性的验证复杂度关于系统规模是指数级的，因为我们证明预不透明性本质上是 PSPACE-hard 的。最后，我们将设定推广到系统秘密意图被建模为执行特定事件序列而非访问秘密状态的情形。