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...

Full description

Saved in:
Bibliographic Details
Main Authors: HAO, Jianan, LIU, Yang, CAI, Wentong, BAI, Guangdong, SUN, Jun
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