| 基于接口精化的广义无干扰性研究 |
| |
| 引用本文： | 孙聪,习宁,高胜,张涛,李金库,马建峰.基于接口精化的广义无干扰性研究[J].计算机研究与发展,2015(7). |
| |
| 作者姓名： | 孙聪 习宁 高胜 张涛 李金库 马建峰 |
| |
| 作者单位： | 1. 西安电子科技大学网络与信息安全学院 西安 710071
2. 中央财经大学信息学院 北京 102206 |
| |
| 基金项目： | 长江学者和创新团队发展计划项目(IRT1078)；国家自然科学基金委员会---广东联合基金重点基金项目(U1135002)；国家科技重大专项基金项目(2011ZX03005-002)；国家自然科学基金项目(61303033，61272398)；陕西省自然科学基础研究计划项目(2013JQ8036)；中央高校基本科研业务费专项资金项目(JB140309)；航空科学基金项目 |
| |
| 摘 要： | 在复杂构件化软件的设计和实现过程中，由于安全属性的可组合性难以实现，使得系统整体的安全需求难以得到有效保证，因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题。针对当前构件化软件设计过程中，信息流安全属性仅局限于二元安全级格模型的问题，在现有安全接口结构基础上提出广义安全接口结构，在广义安全接口结构上定义精化关系，并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性，首次将安全多执行的思想应用于构件化系统的信息流安全属性验证。使用 Coq 定理证明工具实现了接口自动机程序库以及对精化关系的判定过程，并用实例验证说明了无干扰属性定义的特点及判定方法的有效性。
|
| 关 键 词： | 信息流安全 无干扰性 接口自动机 精化 构件化设计 |
A Generalized Non-interference Based on Refinement of Interfaces |
| |
| Sun Cong,Xi Ning,Gao Sheng,Zhang Tao,Li Jinku,Ma Jianfeng.A Generalized Non-interference Based on Refinement of Interfaces[J].Journal of Computer Research and Development,2015(7). |
| |
| Authors: | Sun Cong Xi Ning Gao Sheng Zhang Tao Li Jinku Ma Jianfeng |
| |
| Abstract: | |
| |
| Keywords: | information flow security non-interference interface automata refinement component-based design |
| 本文献已被 万方数据 等数据库收录！ |
