Research On Commercial Security Policy And Its Formal Analysis

Security policy and security model act as the foundation for developing security-related products as well as building security systems. The commercial security policy based on the Clark-Wilson integrity model is a kind of constructing policy for security system applicable to commercial environment. Compared with the research depth and extension on military security policy characteristic of confidentiality, the research and application on commercial security policy characteristic of integrity still drops behind, which mainly results in the deficiency of understand to the application setting of commercial security policy as well as the policy itself. Therefore, it is essential to researches, in depth, investigate the commercial security policy.Research on the commercial security policy includes modeling of the security policy, formal analysis principle of security policy, the framework of commercial security policy and its formal analysis. In this thesis, the modeling and formal analysis of commercial security policy are studied, and the main results achieved are as follows:First, according to the different application settings of security policies, as far as we know, it is the first attempt to divide the security policies into two types: the developing policies for security product and the constructing policies for commercial security system. On the one side, the application scenario is considered the key to precisely understanding the security policy; On the other hand, it acts as an obstacle to model and generalize the commercial security policy.Second, all aspects of the security modeling are investigated, and an applied, easy operated security policy modeling technique with firm theoretical foundation is presented.Third, according to the fact that the essence of commercial security is to effectively control the applications in the system, a formal framework for commercial security policy is proposed, and for the first time the formal modeling of the Clark-Wilson integrity policy is completely made. The framework has the virtues of well-extension and high compatibility.Forth, a creative multi-policy security monitoring framework, aiming for supervising the behaviors in system, is proposed. This framework can solve theproblems such as redundancy of audit data and delay of detecting abnormalities which are existed in the traditional audit sub-systems.Fifth, aiming for solving inconsistence between the security policy model and the security function specification, the security functionality specification technique is directly applied to the development of the security policy model. In addition, the detailed methods and steps to establish security policy specification, based on which the Z formal specification for commercial security policy is built, is presented.Lastly, the high-level formal verification system-Z/EVES is adopted to analyze the commercial security policy specification. Based on the analysis of the commercial security policy specification, the commercial security policy specification is further adjusted and made more reasonable in terms of syntax and semantics. Furthermore, the formal proof about security properties shows that the commercial policy is consistent. It is the first time to analyze the rationality and validity of the Clark-Wilson integrity security policy formally and comprehensively.