Formal analysis and verification on a secure microkernel

Author

Xiaokun Zhang ; Xuying Zhao

Author_Institution

Beijing Electron. Sci. & Technol. Inst., Beijing, China

fYear

2011

fDate

19-22 Aug. 2011

Firstpage

2064

Lastpage

2068

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Mechatronic Science, Electric Engineering and Computer (MEC), 2011 International Conference on

Conference_Location

Jilin

Print_ISBN

978-1-61284-719-1

Type

conf

DOI

10.1109/MEC.2011.6025897

Filename

6025897