Study Of Secure Information Flow In C Language Based On Model Checking

The rapid development of computer brings a lot of problems in network security, so it needs to develop information security technique urgently. In information security, the verification of information flow security can not be implemented by the tradition security methods, which can only be implemented by the verification of the secure information flow properties. As a result, for the purpose of controlling the information flow from End- to-End, It needs to verify the visit of the program to find out whether it satisfies secure information flow properties in multi-level security system.Nowadays, most research of secure information flow focus on the Java Byte Code and the assembly code. Current verifications of secure information flow can be divided into two parts: one is the Type-based method and the other is the semantics-based method. According to the verification results, the semantics-based method is better the type-based one. In the verification of secure information flow, this paper gives out the study of secure information flow with the help of semantics-based method as follows:1. This paper plants the study of secure information flow to the new domain. It gives out the research on information confidential of the secure information flow in C language programs. During the research, the study of secure information flow and model checking are combined together. The study follows the process of modeling– specification– verification. This paper analyses and studies the requirement of the information confidential of secure information flow and it studies the execution features of C language. Based on those studies, it gives out the concrete semantics with the help of abstract interpretation, then it abstract the concrete semantics to get the abstract semantics which can be used to model the C language programs. After the building of the semantics, it verifies the Consistency of the built semantics and standard semantics; this paper gives out the lemma and proves the correctness of the concrete semantics and abstract semantics, so it proves correctness of modeling of the C language program. Meanwhile it analyzes the requirement of information confidential and the cause of the information leakage, and obtains the CTL formula of information confidential.2.Based on the research of information confidential in C language, this paper deeply studies the path feature and state feature in state graph of information confidential and it analyses the effect to the security features of the variables in states. Then it optimizes the state's data structure to reduce the variable number in the state data structure. It also optimizes the semantics of if and while instructions to reduce the states'number and merges unmeaningful branches, as a result, the created states will be linear and this optimization can be used in the study of information integrity. Following the process of the semantics-based method, the abstract semantics of the C language will be obtained. Meanwhile the LTL formula will be give out according to the linear states graph after the analysis of the information integrity.3. This paper gives out the implementation of the secure information flow in C language and it specifies the comparison and analysis of the two methods in first and second paragraph with examples, which can specifies that the improved method is better than the original one.