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, 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 level of 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.


In this page, we present the latest progress of vTRUST work including technical report, source code, verification results and related publications.

  • Technical Report a detailed report of vTRUST framework. PDF (avaliable after paper notification).
  • Slides for better understanding the work. PPT (TBD).
  • Download
    Latest version:
    • vTRUST framework: CSP files and C# DLL download
    • Case study: Verification of Trusted Block as a Service (TBaaS) CSP file download
    • (optional) vTRUST framework: C# source code download
  • References
    • Jianan Hao and Wentong Cai, "Trusted Block as a Service: Towards Sensitive Applications on the Cloud", in TrustCom-2011 pdf
  • Hardware Models
    vTRUST models a featured hardware whose framework is shown as follows.
    Specifically, it includes multiple processors. Each processor has an execution engine that retires instructions, a register file that stores control status and a MMU that manages communication with memory and devices. Features such as trap-and-emulate virtualization and paged memory management are supported. Processors can access memory and manipulate devices by Memory Mapped I/O (MMIO) via MMU. Currently, vTRUST supports ROM (e.g., BIOS), RAM, harddisk, Trusted Platform Module (TPM, a secure chip for Trusted Computing) and network adaptor. One may also extend vTRUST for the support of other devices via easy-to-use interface.

  • Instructio Set
    vTRUST processors support following instructions.
    Mnemonic Legacy Mode Host Mode Guest Mode
    MOVE dst, src dst := eval(src)
    JUMP adr pnp := eval(adr)
    WAKE hv, ptp, pnp Activate another processor.
    hv = hypervisor (physical address)
    ptp = paging table pointer (physical address)
    pnp = guest entry (logical address)
    HALT Inactivate current processor Trap
    RELS Illegal Release Trap
    HYPC id Illegal Illegal Trap (Hypercall id)
    LL start, len Late launch Illegal Trap

  • Attack Models
    vTRUST classifies following attack models.
    • Type-1 attacker: One of clients is malicious and can upload compromised computing program to the server.
    • Type-2 attacker: The attacker can compromise all software in server's harddisk.

  • Properties
    vTRUST supports verification of following properties.
    • The confidentiality guarantees user's data, program and result involved in computation cannot be disclosed to other parties including Cloud administrator.
    • The verifiability guarantees when the computation result is forged or accidently modified, Cloud user can detect it.
    • The isolation guarantees memory allocated to VMs are isolated from each other.
    • The PCR consistency guarantees if the PCR indicates expected value, only selected program can be the hypervisor.

Case Study
  • Trusted Block as a Service (TBaaS)
    Trusted Block as a Service (TBaaS) proposed a system that aims to enhance security of Cloud computing.

    Specifically, TBaaS leverages virtualization technology to isolate user's sensitive application from potentially buggy or malicious management domain which is responsible for handling hardware. Moreover, the system applies Trusted Computing for integrity measurement and remote attestation. The correctness of hypervisor, TPM and network protocol is critical to system's security.

    We will apply vTRUST framework to model TBaaS system and verify its properties against certain attackers.

  • Network Protocol
  • Toolkit Setup
    1. Install PAT application from here.
    2. Download DLL & CSP files, and put them together in the same directory. vTRUST TBaaS
    3. Run PAT GUI, open the CSP file vTRUST_TBaaS.csp.
    4. Execute verirication by pressing F7.
    5. Select properties you want to check and click 'Verify'.
    6. If a property is valid, you will see the trace to satisfy it; otherwise, the property is invalid.

  • Experimental Results
    Time measured on Xeon E3-1245
    Attacker Malicious Software Properties Results
    Bootloader Hypervisor UserProg Valid? |States| |Trans.| Time(s) Mem(MB)
    Type-1 - - 5 instructions NonConfidentiality No 762K 1182K 249 74
    NonVerifiability No 762K 1182K 247 93
    NonStrongIsolation No 762K 1182K 249 88
    NonWeakIsolation No 762K 1182K 248 123
    InconsistentPCR No 762K 1182K 253 143
    Type-2 4 instructions 3 instructions - NonConfidentiality Yes 163K 251K 42 102
    NonVerifiability Yes 163K 251K 42 85
    NonStrongIsolation Yes 163K 251K 42 81
    NonWeakIsolation Yes 163K 251K 42 104
    InconsistentPCR Yes 163K 250K 42 106
    (bug fixed)
    4 instructions 3 instructions - NonConfidentiality No 2481K 6551K 705 104
    NonVerifiability No 2481K 6551K 713 95
    NonStrongIsolation No 2481K 6551K 713 141
    NonWeakIsolation No 2481K 6551K 710 109
    InconsistentPCR No 2481K 6551K 717 132

  • Bug Found
    By verification, a critical bug is found in the implementation of the late launch entry. The bug can be used to break all properties when the type-2 attacker is present. Specifically, the attacker needs to compromise bootloader and hypervisor to achive the goal.

    The bug is mainly because 1) the late launch entry lacks of sanity check of loaded address (should be Mem(3)); and 2) it uses absolute address (Mem(4)) as the address of hypervisor entry when it creates the management VM.

    The attacker can construct a compromised bootloader to copy original late launch entry and hypervisor to a new memory location (Mem(0)=Mem(3)=LLEntry, Mem(1)=Mem(4)=Hypervisor) but overwrite the original memory address with compromised hypervisor (Mem(4)=Hyervisor_Bad). Late launch with the new memory location (from Mem(1) to Mem(2)) will be invoked to obtain unchanged PCR value (PCR=Hash(LLEntry|Hypervisor)). However, when the late launch entry set Mem(4) as hypervisor entry for the management VM, the compromised hypervisor will gain priviledged access, which results in "inconsistent PCR".

    Since the user relies on PCR value to determine the goodness of the server, he fails to detect the server has been compromised. Further interaction with the server will disclose his information such as computing program, data and the computed result, which breaks confidentiality. Other properties such as verifiability and isolation will be affected similarly.

    To fix it, the late launch entry must verify its loaded address at very beginning. After it is fixed, the verification shows that type-2 attacker is defeated.

This page is maintained by Jianan Hao.