| Title: | model checking a secure hypervisor |
| Author: | Sunlv Wang
; Jian Liu
; Qiuping Yi
; Xian Zhang
|
| Issued Date: | 2010
|
| Conference Place: | Wuhan
|
| Keyword: | CAS monitor
; Spin PROMELA language
; model checking
; platform-virtualization software
; secure hypervisor
; formal verification
; operating systems (computers)
; security of data
; virtual machines
|
| Indexed Type: | ieee
|
| ISBN: | 978-1-4244-9287-9
|
| Department: | Inst. of Software, Chinese Acad. of Sci., Beijing, China
|
| English Abstract: | 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. |
| Content Type: | 会议论文
|
| URI: | http://ir.iscas.ac.cn/handle/311060/8828
|
| Appears in Collections: | 中科院软件所图书馆_2010软件所会议论文
|
| File Name/ File Size |
Content Type |
Version |
Access |
License |
|
|---|
| 05718359.pdf（333KB） | -- | -- | 限制开放 | -- | 联系获取全文 |
|
| Recommended Citation: | |
Sunlv Wang,Jian Liu,Qiuping Yi,et al. model checking a secure hypervisor[C]. 见:. Wuhan.
|
|
|
