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

• 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
  Type-2 (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.