《计算机学报》文章摘要   全文下载
文章题目	基于静态分析的强制访问控制框架的正确性验证
作者	吴新松1)，2) 周洲仪1)，2) 贺也平1) 梁洪亮1) 袁春阳3)
作者单位	1)(中国科学院软件研究所 北京 100190) 2)(中国科学院研究生院 北京 100049) 3)(国家计算机网络应急技术处理协调中心 北京 100029)
发表年份	2009
发表月份	4期(730—739)
文章摘要	摘要 现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性,且具有低的误报率和时间开销. 关键词 正确性验证；静态分析；强制访问控制框架；钩子放置；mygcc 中图法分类号: TP301 DOI号: 10.3724/SP.J.1016.2009.00730