vTRUST: A formal modeling and verification framework for virtualization systems
Virtualization is widely used for critical services like Cloud computing. It is desirable to formally verify virtualization systems. However, the complexity of the virtualization system makes the formal analysis a difficult task, e.g., sophisticated programs to manipulate low-level technologies, pag...
Saved in:
Main Authors: | , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2013
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5001 https://ink.library.smu.edu.sg/context/sis_research/article/6004/viewcontent/vtrust.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-6004 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-60042020-03-12T09:37:23Z vTRUST: A formal modeling and verification framework for virtualization systems HAO, Jianan LIU, Yang CAI, Wentong BAI, Guangdong SUN, Jun Virtualization is widely used for critical services like Cloud computing. It is desirable to formally verify virtualization systems. However, the complexity of the virtualization system makes the formal analysis a difficult task, e.g., sophisticated programs to manipulate low-level technologies, paged memory management, memory mapped I/O and trusted computing. In this paper, we propose a formal framework, vTRUST, to formally describe virtualization systems with a carefully designed abstraction. vTRUST includes a library to model configurable hardware components and technologies commonly used in virtualization. The system designer can thus verify virtualization systems on critical properties (e.g., confidentiality, verifiability, isolation and PCR consistency) with respect to certain adversary models. We demonstrate the effectiveness of vTRUST by automatically verifying a real-world Cloud implementation with critical bugs identified. 2013-01-11T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5001 info:doi/10.1007/978-3-642-41202-8_22 https://ink.library.smu.edu.sg/context/sis_research/article/6004/viewcontent/vtrust.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Model Checker Trust Platform Module Malicious Code Trust Computing Virtualization System Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Model Checker Trust Platform Module Malicious Code Trust Computing Virtualization System Software Engineering |
spellingShingle |
Model Checker Trust Platform Module Malicious Code Trust Computing Virtualization System Software Engineering HAO, Jianan LIU, Yang CAI, Wentong BAI, Guangdong SUN, Jun vTRUST: A formal modeling and verification framework for virtualization systems |
description |
Virtualization is widely used for critical services like Cloud computing. It is desirable to formally verify virtualization systems. However, the complexity of the virtualization system makes the formal analysis a difficult task, e.g., sophisticated programs to manipulate low-level technologies, paged memory management, memory mapped I/O and trusted computing. In this paper, we propose a formal framework, vTRUST, to formally describe virtualization systems with a carefully designed abstraction. vTRUST includes a library to model configurable hardware components and technologies commonly used in virtualization. The system designer can thus verify virtualization systems on critical properties (e.g., confidentiality, verifiability, isolation and PCR consistency) with respect to certain adversary models. We demonstrate the effectiveness of vTRUST by automatically verifying a real-world Cloud implementation with critical bugs identified. |
format |
text |
author |
HAO, Jianan LIU, Yang CAI, Wentong BAI, Guangdong SUN, Jun |
author_facet |
HAO, Jianan LIU, Yang CAI, Wentong BAI, Guangdong SUN, Jun |
author_sort |
HAO, Jianan |
title |
vTRUST: A formal modeling and verification framework for virtualization systems |
title_short |
vTRUST: A formal modeling and verification framework for virtualization systems |
title_full |
vTRUST: A formal modeling and verification framework for virtualization systems |
title_fullStr |
vTRUST: A formal modeling and verification framework for virtualization systems |
title_full_unstemmed |
vTRUST: A formal modeling and verification framework for virtualization systems |
title_sort |
vtrust: a formal modeling and verification framework for virtualization systems |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2013 |
url |
https://ink.library.smu.edu.sg/sis_research/5001 https://ink.library.smu.edu.sg/context/sis_research/article/6004/viewcontent/vtrust.pdf |
_version_ |
1770575187875463168 |