基于ptSPA的概率时间信息流安全属性分析  

Analysis for Probabilistic and Timed Information Flow Security Properties via ptSPA

作　　者：李超[1,2] 殷丽华[1] 郭云川[1,2] 

机构地区：[1]中国科学院计算技术研究所信息安全研究中心,北京100190 [2]中国科学院研究生院,北京100049

出　　处：《计算机研究与发展》2011年第8期1370-1380,共11页Journal of Computer Research and Development

基　　金：国家"九七三"重点基础研究发展计划基金项目(2007CB311100);国家"八六三"高技术研究发展计划基金项目(2009AA01Z438);国家自然科学基金项目(61070186;61063002)

摘　　要：基于进程代数的无干扰性分析是分析信息流安全性质的主要方法.为考虑概率时间配置下的信息泄漏,对安全进程代数进行概率时间域上的扩展,提出概率时间安全进程代数ptSPA,给出其形式化语法及语义,引入概率时间弱互拟等价的概念,在此基础上,讨论概率时间信息流安全属性,提出TBSPNI,PTBNDC,SPTBNDC属性,分析属性的包含性,证明提出的属性在表达能力上强于原有属性,最后给出一个实例,对IMP机制在概率时间配置下进行了建模分析,分析结果表明ptSPA对捕获概率时间隐蔽通道的有效性.Information flow analysis is one of the primary approaches for analyzing computer security problems, such as covert channel and data leak. Security process algebra（SPA） is a classic method used in researching information security properties in nondeterministic system. To analyze the information security properties and capture the information leakage in probabilistic and real time system, SPA is extended in probabilistic and time setting. Probabilistic and time security process algebra（ptSPA）, an extension of SPA, is proposed by first introducing the probabilistic and time calculus to specify activities constricted by probability and time, and extending the formal syntax and semantic to enhance the SPA. Then, the related notion of probabilistic and time bisimulation equivalence is presented, to describe two observable behavior traces are equivalent when considering probability and time. Based on ptSPA, several information flow security properties in probabilistic and real time system, such as TBSPNI, PTBNDC and SPTBNDC are defined, which can capture probabilistic and time covert channel while the original SPA cannot. The relations among the information flow security properties are analyzed. Finally, a case study is given to show that the expressiveness of calculus in ptSPA is possible to model and analyze probabilistic and time systems.

关 键 词：信息流分析 安全属性 进程代数 无干扰 隐蔽通道 

分 类 号：TP393.08[自动化与计算机技术—计算机应用技术]