基于静态分析的强制访问控制框架的正确性验证
文献类型：期刊论文
| 作者 | 吴新松 ; 周洲仪 ; 贺也平 ; 梁洪亮 ; 袁春阳 |
| 刊名 | 计算机学报
 |
| 出版日期 | 2009 |
| 卷号 | 32期号:4页码:730-739 |
| 关键词 | 正确性验证 静态分析 强制访问控制框架 钩子放置 mygcc mygcc correctness verification static analysis mandatory access control framework hooks placement mygcc |
| ISSN号 | 0254-4164 |
| 其他题名 | static analysis based correctness verification for mandatory access control framework |
| 中文摘要 | 现阶段对操作系统的强制访问控制框架的正确性验证的研究主要集中于对授权钩子放置的验证.文中基于TrustedBSD MAC框架对强制访问控制框架的正确性验证问题进行了研究,在授权钩子放置验证的基础上,提出了安全标记的完全初始化验证和完全销毁验证.为了实现上述验证,文中提出了一个路径敏感的、基于用户自定义检查规则的静态分析方法.该方法通过对集成于编译器的静态分析工具mygcc进行扩展来验证强制访问控制框架的钩子放置的准确性和完备性.该方法具有完全的路径覆盖性,且具有低的误报率和时间开销. |
| 收录类别 | wanfang,ei,cnki,cscd |
| 资助信息 | Xidian University |
| 语种 | 中文 |
| 公开日期 | 2010-08-23 |
| 附注 | Current researches on correctness verification for the mandatory access control frame-work 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 verifica-tions, this paper also presents a path-sensitive and user-defined-rule based static analysis ap-proach. This approach verifies the accuracy and completeness of hooks placement of the mandato-ry access control framework through extending the compiler integrated static analysis tool-mygcc. It achieves high path cover, low false positive rate and time overhead. |
| 源URL | [http://124.16.136.157/handle/311060/3732]  |
| 专题 | 软件研究所_基础软件国家工程研究中心_期刊论文 |
| 推荐引用方式 GB/T 7714 | 吴新松,周洲仪,贺也平,等. 基于静态分析的强制访问控制框架的正确性验证[J]. 计算机学报,2009,32(4):730-739. |
| APA | 吴新松,周洲仪,贺也平,梁洪亮,&袁春阳.(2009).基于静态分析的强制访问控制框架的正确性验证.计算机学报,32(4),730-739. |
| MLA | 吴新松,et al."基于静态分析的强制访问控制框架的正确性验证".计算机学报 32.4(2009):730-739. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。