Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2013

Abstract

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.

Keywords

Model Checker, Trust Platform Module, Malicious Code, Trust Computing, Virtualization System

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 - November 1

First Page

329

Last Page

346

ISBN

9783642412011

Identifier

10.1007/978-3-642-41202-8_22

Publisher

Springer Link

City or Country

New Zealand

Additional URL

https://doi.org/10.1007/978-3-642-41202-8_22

Download

Share

COinS