基于静态分析的强制访问控制框架的正确性验证  

Static Analysis Based Correctness Verification for Mandatory Access Control Framework

作　　者：吴新松[1,2] 周洲仪[1,2] 贺也平[1] 梁洪亮[1] 袁春阳[3] 

机构地区：[1]中国科学院软件研究所,北京100190 [2]中国科学院研究生院,北京100049 [3]国家计算机网络应急技术处理协调中心,北京100029

出　　处：《计算机学报》2009年第4期730-739,共10页Chinese Journal of Computers

基　　金：国家自然科学基金(90818012);国家“八六三”高技术研究发展计划项目基金(2007AA010601);中国科学院重要方向项目(KGCX2-YW-125)资助~~

摘　　要：现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性,且具有低的误报率和时间开销.Current researches on correctness verification for the mandatory access control framework of operating systems mainly focus on authorization hooks placement verification. Based on TrustedBSD MAC framework, this paper analyses the correctness verification problem for man- datory access control framework, and proposes complete initialization and complete destruction for security labels, as well as complete authorization for access. In order to enforce these verifications, this paper also presents a path-sensitive and user-defined-rule based static analysis approach. This approach verifies the accuracy and completeness of hooks placement of the mandatory access control framework through extending the compiler integrated static analysis tool-mygcc. It achieves high path cover, low false positive rate and time overhead.

关 键 词：正确性验证 静态分析 强制访问控制框架 钩子放置 mygcc 

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