Title :
Formal analysis and verification on a secure microkernel
Author :
Xiaokun Zhang ; Xuying Zhao
Author_Institution :
Beijing Electron. Sci. & Technol. Inst., Beijing, China
Abstract :
CASMonitor, short for CAS Virtual Monitor, is a secure, high-assurance hypervisor prototype, which aims to level B3 or higher of TCSEC standard. This paper combines the B Method and Model Checking Technology to verify certain key problems of the CAS Monitor. To secure Os of B3 level, we use B language to construct formal models for the Security Policy Model and the Formal Top-Level Specification (FTLS). We then conduct Consistency verification on the ChineseWallPolicy model and the refined FTLS model and have found them to possess logical semantic.
Keywords :
formal specification; operating system kernels; program verification; security of data; system monitoring; B language; B3 level; CAS virtual monitor; ChineseWallPolicy model; TCSEC standard; consistency verification; formal analysis; formal top-level specification; formal verification; hypervisor prototype; logical semantic; microkernel security; model checking technology; operating system; security policy model; Access control; Computational modeling; Computers; Schedules; Testing; Virtual machine monitors; CAS Monitor; Model Checking; Secure Operating System;
Conference_Titel :
Mechatronic Science, Electric Engineering and Computer (MEC), 2011 International Conference on
Conference_Location :
Jilin
Print_ISBN :
978-1-61284-719-1
DOI :
10.1109/MEC.2011.6025897
