Formal analysis and verification on a secure microkernel
Xiaokun Zhang, Xuying Zhao · 2011
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.