基于加权下推系统优化可达性分析的Java安全信息流研究  

Secure Information Flow in Java by Optimized Reachability Analysis of Weighted Pushdown System

作　　者：孙聪[1,2] 唐礼勇[2] 陈钟[2] 马建峰[1] 

机构地区：[1]计算机网络与信息安全教育部重点实验室(西安电子科技大学),西安710071 [2]高可信软件技术教育部重点实验室(北京大学),北京100871

出　　处：《计算机研究与发展》2012年第5期901-912,共12页Journal of Computer Research and Development

基　　金：国家科技部重大专项基金项目(2011ZX03005-002);国家自然科学基金项目(60872041);中央高校基本科研业务费基金项目(JY10000903001)

摘　　要：信息流安全的形式化以无干扰性为标准属性.针对目前字节码级的信息流安全分析均未基于对程序无干扰性的语义表示,提出了一种基于语义的无干扰性自动验证方法.为适应语言特性和应用环境的限制,将基本自合成扩展为低安全级记录自合成,以支持对标错状态的可达性分析,保证标错状态不可达时对应字节码程序满足无干扰性.在此基础上为提高实际验证效率提出了3种模型优化方法.实验说明方法的可用性、效率、可扩展性及模型优化的实际效果.A semantic-based approach is commonly considered more precise than the type-based approach to enforcing secure information flow for the program..As a standard criterion to formalize secure information flow, noninterference has not been analyzed with semantic-based approaches at bytecode level. We propose a semantic-based approach to model checking weighted pushdown system for noninterference. In order to overcome the limitations brought by the language feature and application scenario, we extend ordinary self-composition to low-recorded self composition. In this extension the meta-level indices of heap are recorded, and the auxiliary interleaving assignments, as well as the branch condition to illegal-flow state, are modeled to validate the reachability analysis. We prove the correctness that unreachability of illegal-flow state implies the noninterference property of bytecode program. We also propose three model optimizations, companion methods elimination, parameter reordering, and inner-block optimized abstraction of additional code. The experimental results show the availability, efficiency and scalability of our approach, and the effectiveness of the optimizations.

关 键 词：信息流 无干扰性 加权下推系统 自合成 可达性分析 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]