The Design And Implementation Of Memory Manager In VTOS And Research On Its Formal Verification

The development of computer technology brings about growth of the computer’s application field. Computers are deployed in many fields such as aerospace, rail transpotation, healthcare, finance and so on. As software is the soul of the computer, modern society is highly dependent on software. This situation requires that software being highly reliable.As the first layer of software deployed on hardware, operating system’s reliability is of utmost importance. Unfortunatety, traditional methods from software engineering such as testing can not completely guarantee the reliability of software. It is common accepted that formal verification techniques can make a claim about software’s reliability. So our team is committed to the development and verification of a microkernel based operating system VTOS (Verified Trusted Operating System). Microkernel has closed characteristics, and its smallness make it possible to formally describe and verify it. This theses presents the development and verification of memory management in VTOS. The main contributions are as follows:1、We design and implement the memory manager of VTOS. After taking both the architecture of microkernel and performance into account, we propose a solution of putting memory manager into system task. We divide memory manager into two submodules:page allocator, which is responsible for managing the page frames; and address space manager, which is responsible for managing the address space of processes.2、 e establish a formal model of memory manager of VTOS. In consideration of concurrent, the memory manager is modeled using nondeterministic automata. The semantics of every interface function is depicted using Hoare triples, which are used as our verification goals.3、We implement our proposed model of memory manager in interactive theorem prover Isabelle/HOL. The state space of the model is defined. The preconditions and postconditions of every interface function are specified. This work lays foundation for the verification.4、We explore the methods for verifying memory manager. In recognizing that the deterministic automata oriented approach can not solve concurrency, we proposed a nondeterministic automata oriented method. We try to use this new method to verify function free_pages and sum up the experience we gain.