Abstract:In recent years, formal verification technology has received more and more attention, and it plays an important role in ensuring the safety and correctness of systems in critical areas of safety. As a branch of formal verification with a high degree of automation, model checking has a very broad development prospect. This work studies and proposes a new model checking technique, which can effectively check transition systems, including bug-finding and safety proof. Different from existing model checking algorithms, the proposed method, unsatisfied core (UC)-based approximate incremental reachability (UAIR), mainly utilizes the unsatisfied core to solve a series of candidate safety invariants until the final invariant is generated, so as to realize safety proof and bug-finding. In symbolic model checking based on the SAT solver, the UC obtained by the satisfiability solver is used to construct candidate safety invariant, and if the transition system itself is safe, the initial invariant obtained is only an approximation of the safety invariant. Then, while checking the safety, the candidate safety invariant is gradually improved until a real invariant is found that proves the system is safe; if the system is unsafe, the proposed method can finally find a counterexample to prove the system is unsafe. As a brand new method, UCs are exploited for safety model checking and sound results are achieved. As it is all known, there is no absolute best method in the field of model checking, although the proposed method cannot surpass the current mature methods such as IC3, CAR, etc., the method in this paper can solve 3 cases that other mature methods are unable to solve, it is believed that this method can be a valuable addition to the model checking toolset.

Abstract:Constraint solving has been applied to many domains of program analysis, and deeply applied in concurrent program analysis. Concurrent programs are specific domain software that has been widely used with the rapid development of multi-core processors. However, concurrent defects threaten the security and robustness of concurrent programs, thus it is of great importance to test concurrent programs. Due to the non-deterministic thread scheduling, one of the key challenges for concurrent program testing is how to reduce the thread interleaving space with exponential growth. The state-of-the-art approaches (i.e., J-MCR) tackle the challenge through constraint solving. However, it is found that there exist conflicts and redundancies inside constraints (i.e., the conflict of constraint clauses makes constraints unsatisfiable), solving those unsatisfiable constraints results in lower efficiency. Thus, a directed graph constraint-guided method called GC-MCR (directed graph constraint-guided maximal causality reduction) is proposed. By removing conflictive constraints and simplify redundant constraints, the times of constraint solving are reduced thereby further improving the efficiency. Comparing with state-of-the-art approach J-MCR, GC-MCR reduces the times of constraint solving by 19.36% on average and reduces the testing time on average by 34.01% on 38 concurrent programs.

Abstract:As a trusted execution environment technology on ARM processor, TrustZone provides an isolated and independent execution environment for security sensitive programs and data on the device. However, making trusted OS and all trusted applications run in the same trusted environment may cause problems-the exploitation of vulnerabilities on any component will affect the others in the system. Although ARM proposed S-EL2 virtualization technology, which supports multiple isolated partitions in the security world to alleviate this problem, there may still be security threats such as information leakage between partitions in the actual partition manager. Current secure partition manager designs and implementations lack rigorous mathematical proofs to guarantee the security of isolated partitions. This study analyzes the multiple secure partitions architecture of ARM TrustZone in detail, proposes a refinement-based modeling and security analysis method for multiple secure partitions of TrustZone, and completes the modeling and formal verification of the secure partition manager based on the theorem prover Isabelle/HOL. First, a multiple security partitions model named RMTEE is built based on refinement, an abstract state machine is used to describe the system running process and security policy requirements, and the abstract model of multiple secure partitions is established and instantiated. Then the concrete model of the secure partition manager is implemented, in which the event specification is implemented following the FF-A specification. Secondly, in view of the problem that the existing partition manager design cannot meet the goal of information flow security verification, a DAC-based inter-partition communication access control is designed and applied to the modeling and verification of TrustZone security partition manager. Finally, the correctness of the concrete model's refinement of the abstract model and the correctness and security of the event specification in the concrete model are proved, thus completing the formal proof of 137 definitions and 201 lemmas in the model (more than 11 000 lines of Isabelle/HOL code). The results show that the model satisfies confidentiality and integrity, and can effectively defend against malicious attacks of partitions.

Abstract:L4, the second-generation of microkernel, greatly compensates for the shortcomings of the first-generation of microkernel in flexibility and performance, which has attracted the attention of academia and industry. The kernel is the basic component for implementing the operating system. Once it has errors, it may cause the breakdown of whole system, further causing losses to users. Therefore, it is very important to improve the correctness and reliability of the kernel. Virtual memory subsystem is a key mechanism to implement L4 kernel. This study focuses on the formal modeling and verification of this mechanism. A formal model is presented, which involves all operations of mapping mechanism, all management operations of address space, and MMU behavior with TLB. The properties of functional correctness, safety, and security are formalized. Through reasoning about partial correctness, invariants and unwinding conditions, it is shown that the proposed model satisfies these properties in the theorem prover Isabelle/HOL. During modeling and verification, three problems are found related to functional correctness and security in source code. The corresponding solutions or suggestions are given in this study as well.

Abstract:Discrete mathematics is one of the foundation courses of computer science, whose components include propositional logic, first-order logic and axiomatic set theory. Teaching practice shows that it is difficult for beginners to accurately understand abstract concepts such as syntax, semantics and deduction system. In recent years, some scholars have begun to introduce interactive theorem provers into teaching to help students construct formal proofs so that they can understand logical systems more thoroughly. However, existing theorem provers have a high threshold for getting started, directly employing these tools will increase students' learning burden. To address this problem, this study proposes a ZFC axiomatic set theory prover developed in Coq for teaching scenarios. First-order deduction system and ZFC axiomatic set theory are formalized, then several automated reasoning tactics are developed. Students can utilize these tactics to reason formally in a concise, textbook-style proving environment. This tool has been introduced into the discrete mathematics course for freshmen. Students with no prior theorem proving experience can exploit this tool to quickly construct formal proofs of theorems like mathematical induction and Peano arithmetic system, which verifies the practical effect of this tool.

Abstract:Axiom pinpointing has attracted extensive interest for description logics due to its effect of exploring explicable defects in the ontology and searching hidden justifications for the logic consequence. Balancing the expressive power of description logics and the solving efficiency of reasoners has always been the focus of axiom pinpointing research. This study, from both glass-box and black-box perspectives proposed a consequence-based method to computing justifications. The glass-box method uses modified reasoning rules to trace the specific process of inference, and introduces the concept of pinpointing formula to establish the correspondence between the label of Boolean formula and all the minimal axioms sets. The black-box method directly calls the inference engine based on the unmodified reasoning rules, and further uses the HST to compute all justifications for the inference. Two reasoning tools have been designed based on the two axiom pinpointing algorithms for expressive description logics ontologies. Its feasibility is verified theoretically and experimentally, and its solving efficiency is compared with that of existing axiom pinpointing tools.

Abstract:As emerging technologies develop rapidly, domain software puts forward new requirements for development efficiency. In addition, as a declarative programming language with concise syntax and well-defined semantics, Datalog can help developers solve complex problems rapidly and achieve smooth development and thus has attracted wide attention in recent years. However, when solving real-world problems, the existing single-machine Datalog engines are often limited by the size of memory capacity and possess no scalability. To solve these problems, this study designs and implements a Datalog engine based on out-of-core computing. Firstly, a series of operators supporting out-of-core computing are designed to compute the Datalog program, and then the program is converted into a C++ program with the operators. Next, the study designs a partition strategy based on Hash and a minimum replacement scheduling strategy based on search tree pruning. After that, the corresponding partition files are scheduled and computed to generate the final results. Based on this method, the study establishes the prototype tool DDL (disk-based Datalog engine) and selects widely used real-world Datalog programs to conduct experiments on both synthetic and real-world datasets. The experimental results show that DDL has positive performance and high scalability.

Abstract:Feature requests refer to suggestions to perfect existing features or requests for new features proposed by software users on open platforms, and they can reflect users’ wishes and needs. In addition, efficient and accurate analysis and processing of feature requests play a vital role in improving user satisfact