基于下推系统可达性分析的输出信道信息流检测

• 作者: 唐礼勇 孙聪 陈钟
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 信息流 不干涉性 下推系统 可达性分析
• 年，卷（期）: 2011,（7）
• 所属期刊栏目: 软件工程
• 页码范围: 103-107
• 分类号: TP311
• 字数: 6310字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2011.07.023

摘要

提出了一种对含输出信道的命令式语言进行信息流安全性分析的方法.将程序抽象为下推系统,通过自合成将不干涉性转化为安全性属性,将两次相关执行中向输出信道的输出操作分别抽象为由下推规则表示的存储和匹配操作,通过对标错状态的可达性分析验证程序是否满足终止不敏感不干涉性.演化后的方法支持程序的发散执行,通过上界回退算法找到强制终止首次执行所需的最大输出信道上界.实验说明该方法与现有工作相比具有更高的精确性和验证效率.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈钟	北京大学信息科学技术学院软件研究所	105	1674	18.0	38.0
3	唐礼勇	北京大学信息科学技术学院软件研究所	17	296	8.0	17.0
5	孙聪	北京大学信息科学技术学院软件研究所	3	10	2.0	3.0