Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture

doi:10.1007/s11704-012-2084-0

Front Comput Sci

0, Vol.

Issue () : 34-43 https://doi.org/10.1007/s11704-012-2084-0

Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture

Yuehua DAI, Yi SHI(

), Yong QI, Jianbao REN, Peijian WANG

School of Electronic and Information Engineering, Xi’an Jiaotong University, Xi’an 710049, China

Download: PDF(398 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Virtual machine monitors (VMMs) play a central role in cloud computing. Their reliability and availability are critical for cloud computing. Virtualization and device emulation make the VMM code base large and the interface between OS and VMM complex. This results in a code base that is very hard to verify the security of the VMM. For example, a misuse of a VMM hyper-call by a malicious guest OS can corrupt the whole VMM. The complexity of the VMM also makes it hard to formally verify the correctness of the system’s behavior. In this paper a new VMM, operating system virtualization (OSV), is proposed. The multiprocessor boot interface and memory configuration interface are virtualized in OSV at boot time in the Linux kernel. After booting, only inter-processor interrupt operations are intercepted by OSV, which makes the interface between OSV and OS simple. The interface is verified using formal model checking, which ensures a malicious OS cannot attack OSV through the interface. Currently, OSV is implemented based on the AMD Opteron multi-core server architecture. Evaluation results show that Linux running on OSV has a similar performance to native Linux. OSV has a performance improvement of 4%-13% over Xen.

Keywords virtual machine monitor model operating system many core formal verification

Corresponding Author(s): SHI Yi,Email:shiyi@mail.xjtu.edu.cn

Issue Date: 01 February 2013

Cite this article:

Yuehua DAI,Yi SHI,Yong QI, et al. Design and verification of a lightweight reliable virtual machine monitor for a many-core architecture[J]. Front Comput Sci, 0, (): 34-43.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-012-2084-0
https://academic.hep.com.cn/fcs/EN/Y0/V/I/34

1	Barham P, Dragovic B, Fraser K, Hand S, Harris T, Ho A, Neugebauer R, Pratt I,Warfield A. Xen and the art of virtualization. In: Proceedings of the 19th ACM Symposium on Operating Systems Principles . 2003, 164-177
2	Understanding Memory Resource Management in VMware ESX Server. VMWare white paper . www.vmware.com/files/pdf/perfvsphere- memory_management.pdf
3	Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M, Sewell T, Tuch H, Winwood S. seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles . 2009, 207-220 doi: 10.1145/1629575.1629596
4	Holzmann G J. The logic of bugs. In: Proceedings of Foundations of Software Engineering . 2002
5	Gens F. IT cloud services user survey, part . 2: top benefits & challenges. http://blogs.idc.com/ie/?p=210
6	Boyd-Wickizer S, Chen H, Chen R, Mao Y, Kaashoek F, Morris R, Pesterev A, Stein L, Wu M, Dai Y. Corey: an operating system for many cores. In: Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation . 2008, 43-57
7	Engler D, Kaashoek M. Exokernel: an operating system architecture for application-level resource management. ACM SIGOPS Operating Systems Review , 1995, 29(5): 251-266 doi: 10.1145/224057.224076
8	Baumann A, Barham P, Dagand P, Harris T, Isaacs R, Peter S, Roscoe T, Schupbach A, Singhania A. The multikernel: a new OS architecture for scalable multicore systems. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles . 2009, 29-44 doi: 10.1145/1629575.1629579
9	Seshadri A, Luk M, Qu N, Perrig A. SecVisor: a tiny hypervisor to provide lifetime kernel code integrity for commodity OSes. ACM SIGOPS Operating Systems Review , 2007, 41(6): 335-350 doi: 10.1145/1323293.1294294
10	McCune J M, Li Y, Qu N, Zhou Z, Datta A, Gligor V, Perrig A. TrustVisor: efficient TCB reduction and attestation. IEEE Symposium on Security and Privacy . 2010, 143-158
11	Keller E, Szefer J, Rexford J, Lee R B. NoHype: virtualized cloud infrastructure without the virtualization. ACM SIGARCH Computer Architecture News , 2010, 38(3): 350-361 doi: 10.1145/1816038.1816010
12	Shinagawa T, Eiraku H, Tanimoto K, Omote K, Hasegawa S, Horie T, Hirano M, Kourai K, Oyama Y, Kawai E. BitVisor: a thin hypervi sor for enforcing i/o device security. In: Proceedings of the 2009 ACM SIGPLAN/SIGOPS International Conference on Virtual Execution Environments . 2009, 121-130 doi: 10.1145/1508293.1508311
13	Zhang F, Chen J, Chen H, Zang B. CloudVisor: retrofitting protection of virtual machines in multi-tenant cloud with nested virtualization. In: Proceedings of the 23rd ACM Symposium on Operating Systems Principles . 2011, 203-216
14	Steinberg U, Kauer B. NOVA: a microhypervisor-based secure virtualization architecture. In: Proceedings of the 5th European Conference on Computer Systems . 2010, 209-222
15	Klein G, Elphinstone K, Heiser G, Andronick J, Cock D, Derrin P, Elkaduwe D, Engelhardt K, Kolanski R, Norrish M. seL4: formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles . 2009, 207-220 doi: 10.1145/1629575.1629596
16	Franklin J, Seshadri A, Qu N, Chaki S, Datta A. Attacking, repairing, and verifying SecVisor: a retrospective on the security of a hypervisor. Technical Report CMU-CyLab-08-008 . 2008
17	Wang Z, Jiang X. Hypersafe: a lightweight approach to provide lifetime hypervisor control-flow integrity. IEEE Symposium on Security and Privacy (SP) . 2010, 380-395
18	Ravi V, Becchi M, Agrawal G, Chakradhar S. Supporting GPU sharing in cloud environments with a transparent runtime consolidation framework. In: Proceedings of the International Symposium on High- Performance Parallel and Distributed Computting . 2011
19	AMD. Amd64 architecture programmers manual volume 2: system programming. 2007
20	Holzmann G J. The model checker SPIN. IEEE Transactions on Software Engineering , 1997, 23(5): 279-295 doi: 10.1109/32.588521
21	McVoy L, Staelin C. Lmbench: portable tools for performance analysis. In: Proceedings of the 1996 Annual Conference on USENIX Annual Technical Conference . 1996, 23
22	Kortchinsky K. Hacking 3D (and breaking out of VMWare). In: Proceedings of Black Hat conference . 2009
23	Wojtczuk R, Rutkowska J. Xen Owning trilogy. In: Proceedings of Black Hat conference . 2008
24	Secunia. Xen multiple vulnerability report. http://secunia.com/ advisories/44502/
25	Ren J, Qi Y, Dai Y, Xuan Y. Inter-domain communication mechanism design and implementation for high performance. In: Proceedings of the 4th International Symposium on Parallel Architectures, Algorithms and programming (PAAP) . 2011, 272-276

[1]	Zhi-Yu SHEN, Ming LI. Identifying useful learnwares via learnable specification[J]. Front. Comput. Sci., 2025, 19(9): 199344-.
[2]	Changle QU, Sunhao DAI, Xiaochi WEI, Hengyi CAI, Shuaiqiang WANG, Dawei YIN, Jun XU, Ji-rong WEN. Tool learning with large language models: a survey[J]. Front. Comput. Sci., 2025, 19(8): 198343-.
[3]	Le WU, Xiangzhi CHEN, Fei LIU, Junsong XIE, Chenao XIA, Zhengtao TAN, Mi TIAN, Jinglong LI, Kun ZHANG, Defu LIAN, Richang HONG, Meng WANG. EduStudio: towards a unified library for student cognitive modeling[J]. Front. Comput. Sci., 2025, 19(8): 198342-.
[4]	Yuren MAO, Yuhang GE, Yijiang FAN, Wenyi XU, Yu MI, Zhonghao HU, Yunjun GAO. A survey on LoRA of large language models[J]. Front. Comput. Sci., 2025, 19(7): 197605-.
[5]	Yanping ZHENG, Lu YI, Zhewei WEI. A survey of dynamic graph neural networks[J]. Front. Comput. Sci., 2025, 19(6): 196323-.
[6]	Song ZHANG, Lei HE, Dong WANG, Hongyun BAO, Suncong ZHENG, Yuqiao LIU, Baihua XIAO, Jiayue LI, Dongyuan LU, Nan ZHENG. ProSyno: context-free prompt learning for synonym discovery[J]. Front. Comput. Sci., 2025, 19(6): 196317-.
[7]	Haochen ZHAO, Jian ZHONG, Xiao LIANG, Chenliang XIE, Shaokai WANG. Application of machine learning in drug side effect prediction: databases, methods, and challenges[J]. Front. Comput. Sci., 2025, 19(5): 195902-.
[8]	Xuefeng ZHANG, Junfan CHEN, Zheyan LUO, Yuhang BAI, Chunming HU, Richong ZHANG. A multi-projection recurrent model for hypernym detection and discovery[J]. Front. Comput. Sci., 2025, 19(4): 194312-.
[9]	Yong LAI, Zhenghang XU, Minghao YIN. PBCounter: weighted model counting on pseudo-boolean formulas[J]. Front. Comput. Sci., 2025, 19(3): 193402-.
[10]	Yueying LIU, Tingjin LUO. Nonconvex and discriminative transfer subspace learning for unsupervised domain adaptation[J]. Front. Comput. Sci., 2025, 19(2): 192307-.
[11]	Derong XU, Wei CHEN, Wenjun PENG, Chao ZHANG, Tong XU, Xiangyu ZHAO, Xian WU, Yefeng ZHENG, Yang WANG, Enhong CHEN. Large language models for generative information extraction: a survey[J]. Front. Comput. Sci., 2024, 18(6): 186357-.
[12]	Lei WANG, Chen MA, Xueyang FENG, Zeyu ZHANG, Hao YANG, Jingsen ZHANG, Zhiyuan CHEN, Jiakai TANG, Xu CHEN, Yankai LIN, Wayne Xin ZHAO, Zhewei WEI, Jirong WEN. A survey on large language model based autonomous agents[J]. Front. Comput. Sci., 2024, 18(6): 186345-.
[13]	Liangxuan ZHU, Han LI, Xuelin ZHANG, Lingjuan WU, Hong CHEN. Neural partially linear additive model[J]. Front. Comput. Sci., 2024, 18(6): 186334-.
[14]	Jiacheng LI, Ruize HAN, Wei FENG, Haomin YAN, Song WANG. Contactless interaction recognition and interactor detection in multi-person scenes[J]. Front. Comput. Sci., 2024, 18(5): 185325-.
[15]	Chengxing JIA, Fuxiang ZHANG, Tian XU, Jing-Cheng PANG, Zongzhang ZHANG, Yang YU. Model gradient: unified model and policy learning in model-based reinforcement learning[J]. Front. Comput. Sci., 2024, 18(4): 184339-.

Viewed

Full text

Abstract

Cited

Shared

Discussed