| 基于下推系统可达性分析的程序机密消去机制 |
| |
| 引用本文： | 孙聪,唐礼勇,陈钟.基于下推系统可达性分析的程序机密消去机制[J].软件学报,2012,23(8):2149-2162. |
| |
| 作者姓名： | 孙聪 唐礼勇 陈钟 |
| |
| 作者单位： | 北京大学信息科学技术学院软件研究所,北京 100871;高可信软件技术教育部重点实验室(北京大学),北京 100871;网络与软件安全保障教育部重点实验室(北京大学),北京 100871 |
| |
| 基金项目： | 国家自然科学基金，国家科技部重大专项，中央高校基本科研业务费专项资金，装备预研基金 |
| |
| 摘 要： | 针对程序语言信息流安全领域的现有机密消去策略,提出了一种基于下推系统可达性分析的程序信息流安全验证机制.将存储-匹配操作内嵌于对抽象模型的紧凑自合成结果中,使得对抽象结果中标错状态的可达性分析可以作为不同机密消去策略下程序安全性的验证机制.实例研究说明,该方法比基于类型系统的方法具有更高的精确性,且比已有的自动验证方法更为高效.
|
| 关 键 词： | 信息流安全 机密消去 下推系统 自动验证 程序分析 |
| 收稿时间： | 2010/10/7 0:00:00 |
| 修稿时间： | 9/1/2011 12:00:00 AM |
Declassification Enforcement on Program with Reachability Analysis of Pushdown System |
| |
| SUN Cong,TANG Li-Yong and CHEN Zhong.Declassification Enforcement on Program with Reachability Analysis of Pushdown System[J].Journal of Software,2012,23(8):2149-2162. |
| |
| Authors: | SUN Cong TANG Li-Yong and CHEN Zhong |
| |
| Affiliation: | 1,2,3) 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) 3(Key Laboratory of Network and Software Security Assurance(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. |
| |
| Keywords: | information flow security declassification pushdown system automated verification program analysis |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
