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

摘要：

现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性.且具有低的误报率和时间开销.

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

所属期刊栏目：32

分类号：TP301(计算技术、计算机技术)

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

在线出版日期：2009-05-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：730-739