Security System Verification Based On Information Flow Analysis

With the rapid evolution of computer and network technology, more and more attacks appear to computers and public networks. The essential reason why computer systems and networks are under attacks is that there are secure bugs inside them. All kinds of secure policies, secure models are designed to ensure the security of systems, and cryptographic protocols are used to guarantee the security of network communicating. Before all these secure policies applied to real systems, we should validate that they can guarantee the secure goals that they claim. And also we should analyze cryptographic protocols, in order to inspect if there are potential secure leaks.Both direct and indirect confidential data leaks can be considered as illegal information flows. So we can uncover all kinds of security problems in systems and networks by information flow analysis. This method is more essential in information security area.In his paper, we first introduce the normal method of the information flow analysis technology in non-deterministic systems. Then we study the information flow properties both in probabilistic systems and security protocols. We also study the validation methods of these security properties. The contributions of this paper include three main parts:1. Security validation method of probabilistic systems based on non-deterministic information flow analysisIn real systems, attackers can observe the behaviors of systems, and use the statistic probabilistic data to construct probabilistic covert channel, which can lead to indirect confidential data leaks. This paper studies the system security under probabilistic settings. At first, we extend the SPA to PSPA for specifying the behaviors of probabilistic systems. Then based on the property PBNDC, we present and analyze PPBNDC and we explain that PPBNDC is a proper information security property in dynamic environments by some notions such as hostile environments and dynamic hostile environments. We also present SPBNDC and CP_PBNDC properties, which are sufficient conditions of PBNDC. At last we give the relationships between these properties. These security properties are meaningful, because they can uncover those system secure bugs that can't be uncovered by information flow security properties of non-deterministic systems.2. Security Protocols validation method based on environment sensitive information flow analysisIn order to model cryptographic protocol, we extend the SPA to CryptoSPA. Under the semantic model of environment-sensitive labeled transition systems, we define the environment-sensitive trace equivalence and the environment-sensitive weakly bisimulation equivalence. And we present a general schema of NDC based on environment knowledge. We also discuss the confidentiality, authentication and fairness of cryptographic protocols under the schema.3. The validation technology of information flow propertiesThere are universal quantifiers in the definition of BNDC-properties, so it is difficult to validate whether or not a system guarantee these properties. In this article, we use partial model checking technology to validate BNDC-properties. We specify systems behaviors by SPA, and translate the definitions of some specialBNDC-properties to (E \ Top_E)\H≈E\H. Then we count the characteristic formulaφof process E\H, which is modularμcalculus formula. Then it is sufficient to validate if (E\Top_E)\H guarantee the characteristic formula of E\H. We alsopresent the general analysis of cryptographic protocols information flow properties. Under this analysis, the partial model checking method can be used to validate the cryptographic protocol security properties.