Research And Application On Key Technologies Of Model Checking

Computer hardware and software systems have been widely used in such critical areas as commerce, security and so on. Once these systems have errors, they will bring incalculable losses to human being. Model checking is a more effective method to verify the correctness and reliability of the system, which is that the correctness of temporal logic formulas is verified by traversing the finite state machine. However, in practice, state space of concurrent systems will produce exponential increase with the number of concurrent components, that is, the state space explosion problem. Thus, to reduce the state space is crucial to improve the efficiency of model checking. In this thesis, two state-space reduction techniques are proposed.For high level secure operation systems, all kinds of criteria call for analyzing covert channels. TCSEC, which was established by U.S. Department of Defense in 1985, has the definite requirement that for high level secure operation systems with B2 or above certifications covert channels analysis is needed. Both China national standard GB/T 18336-2001 and GB17859-1999 have similar provisions. Therefore, it is essential for the identification of covert channels to improve the security level of the operating system. How to search a kind of special covert channels and verify the security properties of information flow by means of model checking is discussed in the thesis. Specifically, the thesis includes the following aspects:1. Stepwise CTL model checkingModel checking can be divided into two categories:global symbolically model checking and local model checking. Global model checking algorithm has the advantage of using binary decision diagram as the compact representations for state spaces, and its disadvantage is the need to calculate the unreachable state space. Local model checking has the advantage that states are generated in a demand-driven fashion, when they are needed for the computation; and its disadvantage is that the representation of state space is explicit. Therefore, these two methods are effectively combined to alleviate the state space explosion problem.In this thesis, we present a stepwise CTL model checking approach. Our basic idea is that given a finite state machine we utilize symbolic techniques based on binary decision diagram (BDD) to compute its reachable state space gradually and look for a witness or a counter-example for a given CTL formula in the reachable state space. We define the bounded semantics of CTL, and prove that if properties are satisfied in the bounded semantics then it is also satisfied in the unbounded semantics. The feature ensures the accuracy of our method. In the bounded semantics each of the basic CTL operators can be characterized as a least or greatest fixpoints of an appropriate monotonic functions, which is the premise of implementation of symbolic techniques. The experimental results show that, compared with global symbolically model checking and explicit model checking, our method can effectively alleviate the state-space explosion problem, and to a certain extent expand the size of the system, which can be detected.2. Abstraction for Model Checking of the Probabilistic Real-time TemporalLogic of KnowledgeThe probabilistic real-time temporal logic of knowledge (PTACTLK) is the integration of probability, real-time and knowledge based on traditional temporal logic. So it can represent some important properties related to these factors. Abstraction is one of the most effective methods to alleviate the state space explosion problem. Therefore, the abstraction techniques in model checking probabilistic real-time temporal logic of knowledge have been systematically studied in this thesis.Our main contribution as follows:(1) For the real time part of probabilistic real-time temporal logic of knowledge PTACTLK, that is PTACTL, the abstract discrete clock valuations is applied to implicitly construct the clock regions of the state space of a probabilistic real time interpreted system, and in this way we can obtain a finite form of the state space of the probabilistic real time interpreted system. For the epistemic operator K in PTACTLK, the definition of epistemic equivalent to an agent between two abstract states is given by us, therefore, the abstract states satisfying the constraints of this definition can be combined into one equivalent class and the state space of the probabilistic real time interpreted system can be further simplified.(2) Using the abstraction techniques presented above, the corresponding abstract model can be deduced from the original model of a probabilistic real time interpreted system, and the semantics of PTACTLK on the abstract model is given, and we also prove that the abstract model obtained using the abstraction techniques is the upper approximation of the original model.3,Inference Channel IdentificationIn this thesis, a kind of special covert channels(called inference channels) are introduced. In an inference channel, the information transfer is a logical procedure which depends on the running environment of the system, therefore it can't be identified by current covert channel analysis methods. In this paper, based on the run of the program, the program is viewed as a finite state machine, and the state transition sequence is used to characterize the inference channel such that a scenario producing an inference channel can be identified. Our main contribution can be summarized into two aspects as follows:(1) We propose an approach to characterize the inference channel. For the system consisting of two subjects and one object, we use a finite state machine to characterize the operation sequence implemented by subjects on the object. Further we use linear temporal logic (LTL) to characterize the operation sequence so that we can perform the identification by model checking. (2) For the system consisting of multi-subjects and one object, we analyzed the influence caused by the third subject. According to the third subject's access, we divided the access sequence into several isolated sequences such that the above identification method can be directly applied in searching for inference channels for the system with multiple subjects.4. The nature of covert channel is illegal information flow, which is characterized by intransitive noninterference. To ensure that there is no such information flow in security system, we verify the system to satisfy intransitive noninterference. There is no valid method to verify intransitive noninterference, we present a symbolic algorithmic approach to the verification of intransitive noninterference.The reliability and completeness of the verification depend on the computation of Completeness Threshold(CT). CT must be satisfied:the system is not satisfiable for intransitive noninterference, there must exist a counterexample of length not exceeding threshold. Based on graph-theoretic properties of systems we proposed an over-approximation to the smallest CT. Because of the formula of propositional satisfiability solver in the software and hardware analysis having been successfully used recent years, Further, we reduce the counterexamples search and the computation of CT to propositional satisfiability, and achieve the verification process to a symbolic computing, and thus for large-scale multi-level security verification system provides an effective way.