概率系统的非传递无干扰安全属性分析

Analysis for intransitive noninterference security properties in probabilistic systems

为了实现概率信息的安全降密和信道控制等重要安全策略,将可信域的概念引入概率安全进程代数,并以此为工具将非传递无干扰信息流安全模型推广到概率系统.在弱概率互拟等价的基础上讨论了非传递概率信息流安全属性,提出了非传递概率互拟强无干扰(I_BSPNI)和非传递概率互拟复合不可演绎(I_PBNDC)安全属性;并要求系统所有可达状态都满足的持久I_PBNDC属性,该性质能够揭露出I_PBNDC在动态环境中不能暴露的安全隐患.为了弥补互拟复合不可演绎类性质难于验证的缺点,使用基于单步状态的展开条件定义了强I_PBNDC属性.最后分析并证明了这些安全属性之间的包含关系.

The concept of trust domain was introduced into probabilistic secure process algebra （PSPA）, and the intransitive noninterference information flow security model was extended to probabilistic systems to implement many important security policies such as secure downgrading of probabilistic information and channel control. Intransitive probabilistic information flow security properties were analyzed based on the probabilistic weak bisimulation equivalence. Intransitive bisimulation strong probabilistic noninterference （I_BSPNI） and intransitive probabilistic bisimulation-based nondeducibility on composition （I_PBNDC） were presented. To expose the potential secure problem that I_ PBNDC cannot discover in dynamic context, the persistent I_PBNDC property was proposed, which required that every reachable state of the system must satisfy I_PBNDC. The properties like bisimulation-based nondeducibility on composition are difficult to prove. To overcome this shortcoming, strong I PBNDC property was defined in terms of unwinding conditions demanding properties of individual actions. Finally, the relations between these proper- ties were given and proved.