中文摘要：

基于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.