| 本文已被：浏览 4383次 下载 6236次 |
码上扫一扫！ |
|
|
| 基于下推系统可达性分析的程序机密消去机制 |
|
孙聪1,2,3, 唐礼勇1,2,3, 陈钟1,2,3
|
|
1.北京大学 信息科学技术学院 软件研究所,北京 100871;2.高可信软件技术教育部重点实验室(北京大学),北京 100871;3.网络与软件安全保障教育部重点实验室(北京大学),北京 100871
|
|
| 摘要: |
| 针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效. |
| 关键词: 信息流安全 机密消去 下推系统 自动验证 程序分析 |
| DOI：10.3724/SP.J.1001.2012.04117 |
| 分类号: |
| 基金项目:国家自然科学基金(60773163, 60821003, 60872041, 60911140102); 国家科技部重大专项(2011ZX03005-002); 中央高校基本科研业务费专项资金(JY10000903001); 装备预研基金(9140A15040210HK6101) |
|
| Declassification Enforcement on Program with Reachability Analysis of Pushdown System |
|
SUN Cong,TANG Li-Yong,CHEN Zhong
|
|
1.Institute of Software, School of Electronics Engineering and Computer Science, Peking University, Beijing 100871, China;2.Key Laboratory of High Confidence Software Technologies (Peking University), Ministry of Education, Beijing 100871, China
|
| Abstract: |
| The study proposes a verification mechanism based on reachability analysis of pushdown system to enforce existing declassification policies of language-based 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. |
| Key words: information flow security declassification pushdown system automated verification program analysis |
