ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2015, Vol. 52 ›› Issue (7): 1631-1641.doi: 10.7544/issn1000-1239.2015.20140306

• 软件技术 • 上一篇    下一篇

基于接口精化的广义无干扰性研究

孙聪1,习宁1,高胜2,张涛1,李金库1,马建峰1   

  1. 1(西安电子科技大学网络与信息安全学院 西安 710071); 2(中央财经大学信息学院 北京 102206) (suncong@xidian.edu.cn)
  • 出版日期: 2015-07-01
  • 基金资助: 
    基金项目:长江学者和创新团队发展计划项目(IRT1078);国家自然科学基金委员会——广东联合基金重点基金项目(U1135002);国家科技重大专项基金项目(2011ZX03005-002);国家自然科学基金项目(61303033,61272398);陕西省自然科学基础研究计划项目(2013JQ8036);中央高校基本科研业务费专项资金项目(JB140309);航空科学基金项目(2013ZC31003,20141931001)

A Generalized Non-interference Based on Refinement of Interfaces

Sun Cong1, Xi Ning1, Gao Sheng2, Zhang Tao1, Li Jinku1, Ma Jianfeng1   

  1. 1(School of Cyber Engineering, Xidian University, Xi’an 710071);2(School of Information, Central University of Finance and Economics, Beijing 102206)
  • Online: 2015-07-01

摘要: 在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题.针对当前构件化软件设计过程中,信息流安全属性仅局限于二元安全级格模型的问题,在现有安全接口结构基础上提出广义安全接口结构,在广义安全接口结构上定义精化关系,并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性,首次将安全多执行的思想应用于构件化系统的信息流安全属性验证.使用Coq定理证明工具实现了接口自动机程序库以及对精化关系的判定过程,并用实例验证说明了无干扰属性定义的特点及判定方法的有效性.

关键词: 信息流安全, 无干扰性, 接口自动机, 精化, 构件化设计

Abstract: In the design and implementation of complicated component-based softwares, the security requirements on the whole system are hard to achieve due to the difficulty on enforcing the compositionality of the security properties. The specification and verification of security properties are the critical issues in the development of component-based softwares. In this paper, we focus on the generalization on the security lattice over the information flow security properties enforceable on the component-based softwares. The previous definitions of the information flow security properties in the component-based design are restricted on the binary security lattice model. In this work, we extend the interface structure for security to the generalized interface structure for security (GISS). We define a refinement relation and use this relation to give a non-interference definition (SME-NI) based on the principle of secure multi-execution. This is the first application of secure multi-execution on the information flow security verification of component-based systems. The new definition of non-interference can be adapted to any finite security lattice models. The Coq proof assistant is used to implement the certified library for interface automata, as well as the decision procedure for the refinement relation. The experimental results show the characteristics of SME-NI and the validity of decision procedure.

Key words: information flow security, non-interference, interface automata, refinement, component-based design

中图分类号: