首页 >> 收录期刊 >> 计算机科学 >> 正文
杂志中文名:计算机科学
杂志英文名:Computer Science
主管单位:国家科学技术部
主办单位:国家科技部西南信息中心
地址:重庆市渝北区北部新区洪湖西路18号
邮编:401121
电话:023-63500828;
Email:jsjkx12@163.com
ISSN:1002-137X
主编:朱完元












基于下推系统可达性分析的输出信道信息流检测
引用本文:孙 聪,唐礼勇,陈 钟.基于下推系统可达性分析的输出信道信息流检测[J].计算机科学,2011,38(7):103-107.
作者姓名:孙 聪  唐礼勇  陈 钟
作者单位:北京大学信息科学技术学院软件研究所,北京100871;高可信软件技术教育部重点实验室,北京100871
基金项目:本文受国家自然科学基金(60773163,60911140102)资助。
摘    要:提出了一种对含输出信道的命令式语言进行信息流安全性分析的方法。将程序抽象为下推系统,通过自合成将不千涉性转化为安全性属性,将两次相关执行中向输出信道的输出操作分别抽象为由下推规则表示的存储和匹配操作,通过对标错状态的可达性分析验证程序是否满足终止不敏感不干涉性。演化后的方法支持程序的发散执行,通过上界回退算法找到强制终止首次执行所需的最大输出信道上界。实验说明该方法与现有工作相比具有更高的精确性和验证效率。

关 键 词:信息流,不干涉性,下推系统,可达性分析

ChecKing Information Flow on Output Channel with Reachability Analysis of Pushdown System
SUN Cong,TANG Li-yong,CHEN Zhong.ChecKing Information Flow on Output Channel with Reachability Analysis of Pushdown System[J].Computer Science,2011,38(7):103-107.
Authors:SUN Cong  TANG Li-yong  CHEN Zhong
Affiliation:(Institute of Software,School of Electronics Engineering and Computer Science,Peking University,Beijing 100871,China);(Key Laboratory of High Confidence Software Technologies, Ministry of Education,Beijing 100871,China)
Abstract:We proposed an approach for analyzing information-flow security of imperative language with output channels. The program is abstracted with pushdown system, which is then self-composed in order to adapt noninterference as a safety property. The output operations in the two relevant runs are respectively modeled as storing and matching procedure by pushdown rules. Then the termination-insensitive noninterference is verified by a reachability analysis of illegal-flow state. A variation of this approach can deal with program containing divergent run. An upper-bound regression algorithm was proposed to find the maximum upper-bound in order to trigger coercive termination of divergent run. The experimental results show that the approach is more precise and efficient than existing work.
Keywords:Information f1ow  Noninterference  Pushdown system  Reachability analysis
本文献已被 万方数据 等数据库收录!
    浏览原始摘要     下载PDF全文