DocumentCode :
2900417
Title :
A Precise Memory Model for Operating System Code Verification
Author :
Chen, Geng ; Luo, Lei ; Wang, Lijie
Author_Institution :
Sch. of Comput. Sci. & Eng., Univ. of Electron. Sci. & Technol. of China, Chengdu, China
fYear :
2011
fDate :
16-18 Nov. 2011
Firstpage :
1125
Lastpage :
1132
Abstract :
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.
Keywords :
operating system kernels; real-time systems; virtual machines; virtualisation; C programming language; code verification; formal memory model; operating system; real time operating system kernel; software virtual machine kernel; verification environment; virtualization technology; Compounds; Data models; Hardware; Kernel; Load modeling; Semantics; formal method; real-time operating systems; verification;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Trust, Security and Privacy in Computing and Communications (TrustCom), 2011 IEEE 10th International Conference on
Conference_Location :
Changsha
Print_ISBN :
978-1-4577-2135-9
Type :
conf
DOI :
10.1109/TrustCom.2011.153
Filename :
6120946
Link To Document :
بازگشت