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

作     者：李超 殷丽华 郭云川 Li Chao;Yin Lihua;Guo Yunchuan

作者机构：中国科学院计算技术研究所信息安全研究中心北京100190 中国科学院研究生院北京100049 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2011年第48卷第8期

页      面：1370-1380页

核心收录：

学科分类：0810[工学-信息与通信工程] 0808[工学-电气工程] 08[工学] 0839[工学-网络空间安全] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

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

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

摘      要：基于进程代数的无干扰性分析是分析信息流安全性质的主要方法.为考虑概率时间配置下的信息泄漏,对安全进程代数进行概率时间域上的扩展,提出概率时间安全进程代数ptSPA,给出其形式化语法及语义,引入概率时间弱互拟等价的概念,在此基础上,讨论概率时间信息流安全属性,提出TBSPNI,PTBNDC,SPTBNDC属性,分析属性的包含性,证明提出的属性在表达能力上强于原有属性,最后给出一个实例,对IMP机制在概率时间配置下进行了建模分析,分析结果表明ptSPA对捕获概率时间隐蔽通道的有效性.