The Formal Design, Implement And Verification Of VTOS File System

As the development of information technology, the requirements of the security of information and the reliability of software are rising. Now data security is a popular topic. As filesystem is one of the most important modules and also the manager of the disk, a small mistake could lead to the collapse of the operating system, even the loss of the data stored in the disk, which may bring huge economic losses. So the security of the filesystem is an important aspect of the operating system and disk.Given the high module independence of the micro-kernel and the mathematical and unambiguous of the formal methods, this paper designs and implementes the filesystem based on micro-kernel, and then demonstrates on the correctness of the filesystem with the formal methods.1. Learn from the idea of the cache mechanisim of Linux, we design and implemente a stable and efficient cache management for VTOS filesystem, including a dentry cache management.2. We chose the ext3 as the VTOS’s root filesystem from in consideration of efficiency and security, then design and implemente the operations of the ext3 filesystem.3. A formal model of the filesystem module is established, in which status means the data stored in the system. From this we can give a preliminary guarantee of the correctness of the VTOS filesystem. In order to ensure the correctness of the VTOS filesystem in further, we give a formal verification of several important functions of the VTOS filesystem, aided with the Isabelle/HOL theorem prover.The design of the VTOS filesystem is based on micro-kernel, which gives an ensurance of module independence; the formal modeling and formal verification of the VTOS filesystem give ganrentees of the correctness of the VTOS filesystem.