A Security Domain Separation Z Model Based on DTE Policy

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.