model checking a secure hypervisor
文献类型：会议论文
| 作者 | Sunlv Wang ; Jian Liu ; Qiuping Yi ; Xian Zhang |
| 出版日期 | 2010 |
| 会议地点 | Wuhan |
| 关键词 | CAS monitor Spin PROMELA language model checking platform-virtualization software secure hypervisor formal verification operating systems (computers) security of data virtual machines |
| 页码 | 119-122 |
| 英文摘要 | 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. |
| 收录类别 | IEEE |
| ISBN号 | 978-1-4244-9287-9 |
| 源URL | [http://124.16.136.157/handle/311060/8828]  |
| 专题 | 软件研究所_软件所图书馆_2010软件所会议论文 |
| 推荐引用方式 GB/T 7714 | Sunlv Wang,Jian Liu,Qiuping Yi,et al. model checking a secure hypervisor[C]. 见:. Wuhan. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。