版权所有：内蒙古大学图书馆 技术提供：维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
基于下推系统可达性分析的程序机密消去机制
Declassification Enforcement on Program with Reachability Analysis of Pushdown System作者机构：北京大学信息科学技术学院软件研究所北京100871 高可信软件技术教育部重点实验室(北京大学)北京100871 网络与软件安全保障教育部重点实验室(北京大学)北京100871
出 版 物：《软件学报》 (Journal of Software)
年 卷 期：2012年第23卷第8期
页 面：2149-2162页
核心收录：
学科分类：0839[工学-网络空间安全] 08[工学] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）]
基 金：国家自然科学基金(60773163 60821003 60872041 60911140102) 国家科技部重大专项(2011ZX03005-002) 中央高校基本科研 业务费专项资金(JY100009030 01) 装备预研基金(9140A15040210HK6101)
摘 要：针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.
