基于DTE策略的安全域隔离Z形式模型  

A Security Domain Separation Z Model Based on DTE Policy

作　　者：卿斯汉[1] 李丽萍[1] 何建波[1] 沈晴霓[2] 

机构地区：[1]中国科学院软件研究所 [2]北京大学软件与微电子学院,北京102600

出　　处：《计算机研究与发展》2007年第11期1881-1888,共8页Journal of Computer Research and Development

基　　金：北京市自然科学基金项目(4052016);国家自然科学基金项目(60573042);国家"九七三"重点基础研究发展规划基金项目(G1999035802)~~

摘　　要：基于DTE策略的安全域隔离技术是构造可信系统的基本技术之一.但现有DTE实现系统存在安全目标不明确、缺乏对系统及其安全性质的形式定义和分析的缺点,导致系统安全性难以得到保证.定义了一个基于DTE策略的安全域隔离模型,采用Z语言形式定义了系统状态、基于信息流分析的不变量和安全状态,并借助Z/EVES工具给出验证系统安全的形式分析方法.解决了DTE系统的形式化建模问题,为安全域隔离技术的实现和验证奠定了基础.High security level trusted information system need formal model of security policies to gain adequate assurance. Security domain separation based on DTE policy is one of the basic technologies to build trusted system. But the current DTE systems are difficult to assure their security, because they have no explicit security objective, their policy configuration is too complex, and there are no formal specification and formal verification of security properties on these systems or their policies. A security domain separation model based on DTE policy is formalized. It defines system state and adopted least privilege as domain separation principle. It extends original DTE policy, defines authorized information flow and pipeline information flow as two new invariants based on information flow analysis. Then system secure state is given and formal analysis by proven theorem is adopted to verify system security. The model is specified using the Z formal language and verified with the help of Z/EVES tool. The model has been implemented in the ANSHENG V4.0 security operation system and a Web server example is given. The work will also facilitate policy analysis and management of SELinux. This formal model resolves the formalization problem of DTE system and provids the foundation for security domain separation implementation and verification.

关 键 词：安全域隔离 信息流 DTE 可信管道 形式化 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]