Model Checking a Secure Hypervisor
WCSE), 2010 Second World Congress（2010）
摘要
Hypervisor is a piece of platform-virtualization software that allows multiple operating systems to run on a host computer concurrently. CAS Monitor, short for CAS Virtual Monitor, is a secure, high-assurance hypervisor prototype, which aims to level B3 or higher of TCSEC standard. This paper reports our experience of employing model checking method to verify some design properties of CAS Monitor, such as isolation, mediated sharing, communication between separated virtual machines and source control policy. We show how to specify design architecture of CAS Monitor with Spin PROMELA language and verify the above important properties to meet system security request.
更多查看译文
关键词
design property,cas monitor,tcsec standard,spin promela language,chinese-wall policy,platform-virtualization software,model checking,virtual machines,operating systems (computers),design architecture,cas virtual monitor,host computer concurrently,secure operating system,hypervisor,high-assurance hyper visor prototype,secure hypervisor,hyper visor,important property,formal verification,security of data,memory management,computational modeling,system security,multiplication operator,source control,operating systems,virtual machine,security
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要