基于下推系统可达性分析的程序机密消去机制  

Declassification Enforcement on Program with Reachability Analysis of Pushdown System

作　　者：孙聪[1,2,3] 唐礼勇[1,2,3] 陈钟[1,2,3] 

机构地区：[1]北京大学信息科学技术学院软件研究所,北京100871 [2]高可信软件技术教育部重点实验室(北京大学),北京100871 [3]网络与软件安全保障教育部重点实验室(北京大学),北京100871

出　　处：《软件学报》2012年第8期2149-2162,共14页Journal of Software

基　　金：国家自然科学基金(60773163;60821003;60872041;60911140102);国家科技部重大专项(2011ZX03005-002);中央高校基本科研;业务费专项资金(JY100009030 01);装备预研基金(9140A15040210HK6101)

摘　　要：针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.The study proposes a verification mechanism enforce existing declassiflcation policies of language-based based on reachability analysis of pushdown system to information flow security. The pushdown rules of store and match primitives are embedded in the abstract model after compact self-composition. The security property with respect to different declassification policies is violated when the illegal-flow state is reached in the pushdown system. The experimental results show improvement in precision, compared with the type-based mechanisms, and growth in effectiveness compared with the RNI-enforcement based on automated verification.

关 键 词：信息流安全 机密消去 下推系统 自动验证 程序分析 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]