A Precise Memory Model for Operating System Code Verification

Recently, safety and security requirements of real-time system received much attention. Several formal approaches have been presented to verify some related properties at the source code level. System's code is almost universally written in the C programming language, where memory is just a sequence of bytes and data can overlap almost arbitrarily. In this paper, we present a two-level formal memory model: abstract level and physical level. The abstract level is used to verify properties at design stage. While at physical level, the memory model captures some low-level features of C's pointers and memory. It is used to prove properties on code level. Then, we provide some well-behaved operations in the memory model and prove the well-formedness conditions of both levels. We use this model to solve the problems we encountered in an ongoing attempt to verify the Software Virtual Machine Kernel (SVMK). It is a real-time operating system kernel based on virtualization technology. The memory model is integrated in our verification environment based on the interactive theorem prover Coq. This verification environment will ultimately be used for the verification of the SVMK.