Confidential virtual machines (CVMs) are increasingly deployed to protect users’ code and data in use against attackers with hypervisor privileges. Arm has recently introduced hardware extensions, the Confidential Compute Architecture (CCA), to support CVMs. However, Arm CCA does not support live migration, a crucial virtualization feature. This work presents the first design of live migration support for Arm CCA. The design aims to reuse functionality for migrating regular VMs from commodity hypervisors to simplify development efforts while preserving the protection of CVMs. We prototype the design to support de facto mechanisms, including pre-copy and post-copy, to migrate CVMs on Arm CCA. Given that no CCA hardware is currently available, we created a performance modeling framework, pCCA that mimics a CCA environment over an off-the-shelf Arm server hardware, enabling the evaluation of CCA-based CVM live migration performance for the first time.

Modern processors expose hardware performance monitoring capabilities through Performance Monitoring Units (PMUs). Profiling tools leverage these PMU facilities to analyze program execution. As the computation is increasingly shifting to virtual machines (VMs), commodity hypervisors like KVM have implemented virtual PMUs (vPMUs) to expose these capabilities to VMs. However, we found that KVM's current vPMU implementation introduces substantial overhead, leading to inaccurate measurements. This overhead stems from frequent VM exits caused by PMU access and sampling interrupts, as well as the complexity of emulation. To address this, we develop Direct vPMU (D-vPMU), a novel set of passthrough mechanisms for Intel x86 platforms running KVM. D-vPMU enables VMs to access the physical PMU and handle interrupts directly, thereby eliminating the virtualization overhead that currently plagues vPMU solutions. D-vPMU delivers better profiling accuracy and performance while strictly maintaining the security and isolation boundaries between guest and host PMU contexts.

Arm TrustZone technology provides hardware features to enable the deployment of security-critical software in trusted execution environments (TEEs). Although TrustZone is widely deployed on physical hardware, it is unavailable to increasingly deployed virtual machines (VMs) running on commodity Arm platforms. These VMs cannot leverage TrustZone's security features, such as secure boot, or deploy trusted applications to secure their systems. To address this limitation, we propose a new design, called kvTZ, that extends commodity hypervisors to expose a virtualized TrustZone to VMs. kvTZ introduces exception-level multiplexing, a novel technique that enables native execution of TrustZone software in the VM environment on the existing Arm hardware. We prototyped kvTZ by extending KVM implementations, including the mainline Linux and Google's Android Linux for pKVM, to support legacy and confidential VMs. kvTZ supports OP-TEE, a de facto open-source TEE for Arm TrustZone. For the first time, we enabled OP-TEE's entire software stack, which encompasses trusted applications (TAs), the kernel, and trusted firmware, to run in a virtualized TrustZone. We show that kvTZ achieves performance efficiency and outperforms the full software emulation-based solution.

To enhance the security of virtual machines (VMs) in multi-tenant cloud environments, AMD provides the Secure Encrypted Virtualization (SEV) extension to support encrypted VMs. We discovered two previously unknown side channels from AMD processors with SEV support: cache flush and memory contention side channels. Our findings apply to SEV-SNP and earlier versions of the technology (SEV and SEV-ES). We formulated two Reload+Reload (RR) attacks based on our two respective findings: Reload+Reload-flush-set (RRFS) and Reload+Reload-memory-block (RRMB). We demonstrated the effectiveness of the attacks against SEV-SNP protected VMs: we built a RRFS-based covert channel for a Spectre attack and used RRMB for extracting AES-128 secret keys. Compared to Prime+Probe-based implementations, our RRFS-based covert channel demonstrates superior noise resistance and higher capacity.

Memory safety vulnerabilities are a significant challenge for programming languages like C and C++. Among these vulnerabilities, heap-based issues have become more prevalent in recent years. Exploiting these vulnerabilities allows adversaries to execute arbitrary memory reads, writes, and even code execution. The Memory Tagging Extension (MTE), introduced in the Arm v8.5-A processor architecture, is an example of such a security feature. MTE has been utilized in modern software to implement probabilistic protection for heap-based memory safety vulnerabilities, including use-after-free and heap-based buffer overflow. However, the existing MTE-based approaches offer probabilistic protection and are vulnerable to brute-force attacks. Moreover, these approaches offer inter-object isolation but are vulnerable to intra-object overflow. Further, adversaries leverage memory confusion to manipulate or leak pointers, leading to arbitrary memory read/write and code execution. In response to the limitation and security, this work introduces a novel usage of MTE, called HeMate, to isolate memory storing different primitive types of data on the heap to enhance memory safety. This approach provides a non-probabilistic constraint on vulnerability exploitation against memory objects with different primitive data types, such as intra-object overflow and use-after-free. We have implemented a HeMate prototype compiler for C programs based on the LLVM framework. Our approach effectively leverages MTE to protect against memory safety vulnerabilities while preserving the functionality of commonly used Linux applications.

A rootkit or an attacker that exploited a single vulnerability in a monolithic OS kernel like Linux could obtain full authority over the system. We introduce SECvma, a new system with Linux kernel protection for Arm-based platforms. SECvma employs a virtualization-based approach to transparently protect the kernel’s code integrity in its lifetime. SECvma proposes a new design that extends current Linux KVM-based confidential virtual machine (CVM) frameworks to provide standalone Linux kernel protection with modest effort while preserving the safety of CVMs. SECvma leverages Arm’s hardware virtualization extensions and addresses their limitations in supporting kernel protection. SECvma incorporates novel optimizations to reduce the overhead from the virtualization-based approach. SECvma significantly enhances Linux’s security while retaining its performance efficiency and standard features, including dynamic kernel module loading and kernel page table isolation (KPTI).

As computations have increasingly shifted to virtual machines (VMs) running on a hypervisor, the security of the hypervisor is of critical concern. Rust has gained significant traction among developers due to its software safety guarantees and performance efficiency. This work explores building on Rust's safety features to construct a secure KVM hypervisor. We retrofit KVM to incorporate a Rust-based core to protect virtual machines. We build on Rust's type and lifetime system in a novel way to secure the core's memory accesses in a concurrent environment. Our resulting KVM implementation, KrustVM, incorporates a data race and deadlock-free core to protect VM confidentiality and integrity against privileged attackers who control the host Linux kernel while preserving KVM's commodity features and performance.

The Android system protects its users' privacy via app permissions, which govern apps' access to sensitive data and resources. However, recent research has reported that, during app virtualization, the current Android permission model fails to prevent illegal permission usage: apps can exploit the User ID shared among co-hosted apps in the same virtualized environment to perform unauthorized actions. To the best of our knowledge, such over-privilege issues have not been thoroughly investigated; neither has a practical defense proposed to address them.

Concurrent systems software is widely-used, complex, and error-prone, posing a significant security risk. We introduce VRM, a new framework that makes it possible for the first time to verify concurrent systems software, such as operating systems and hypervisors, on Arm relaxed memory hardware. VRM defines a set of synchronization and memory access conditions such that a program that satisfies these conditions can be mostly verified on a sequentially consistent hardware model and the proofs will automatically hold on relaxed memory hardware. VRM can be used to verify concurrent kernel code that is not data race free, including code responsible for managing shared page tables in the presence of relaxed MMU hardware. Using VRM, we verify the security guarantees of a retrofitted implementation of the Linux KVM hypervisor on Arm. For multiple versions of KVM, we prove KVM's security properties on a sequentially consistent model, then prove that KVM satisfies VRM's required program conditions such that its security proofs hold on Arm relaxed memory hardware. Our experimental results show that the retrofit and VRM conditions do not adversely affect the scalability of verified KVM, as it performs similar to unmodified KVM when concurrently running many multiprocessor virtual machines with real application workloads on Arm multiprocessor server hardware. Our work is the first machine-checked proof for concurrent systems software on Arm relaxed memory hardware.

Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove security properties of the entire hypervisor by verifying the core alone. To verify the multiprocessor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, while retaining KVM’s functionality and performance. Our work is the first machine-checked security proof for a commodity multiprocessor hypervisor.

Nested virtualization, the ability to run a virtual machine inside another virtual machine, is increasingly important because of the need to deploy virtual machines running software stacks on top of virtualized cloud infrastructure. As ARM servers make inroads in cloud infrastructure deployments, supporting nested virtualization on ARM is a key requirement, which has been met recently with the introduction of nested virtualization support to the ARM architecture. We build the first hypervisor to use ARM nested virtualization support and show that despite similarities between ARM and x86 nested virtualization support, performance on ARM is much worse than on x86. This is due to excessive traps to the hypervisor caused by differences in non-nested virtualization support. To address this problem, we introduce a novel paravirtualization technique to rapidly prototype architectural changes for virtualization and evaluate their performance impact using existing hardware. Using this technique, we propose Nested Virtualization Extensions for ARM (NEVE), a set of simple architectural changes to ARM that can be used by software to coalesce and defer traps by logging the results of hypervisor instructions until the results are actually needed by the hypervisor or virtual machines. We show that NEVE allows hypervisors running real application workloads to provide an order of magnitude better performance than current ARM nested virtualization support and up to three times less overhead than x86 nested virtualization. NEVE will be included in ARMv8.4, the next version of the ARM architecture.

ARM servers are becoming increasingly common, making server technologies such as virtualization for ARM of growing importance. We present the first study of ARM virtualization performance on server hardware, including multi-core measurements of two popular ARM and x86 hypervisors, KVM and Xen. We show how ARM hardware support for virtualization can enable much faster transitions between VMs and the hypervisor, a key hypervisor operation. However, current hypervisor designs, including both Type 1 hypervisors such as Xen and Type 2 hypervisors such as KVM, are not able to leverage this performance benefit for real application workloads. We discuss the reasons why and show that other factors related to hypervisor software design and implementation have a larger role in overall performance. Based on our measurements, we discuss changes to ARM's hardware virtualization support that can potentially bridge the gap to bring its faster VM-to-hypervisor transition mechanism to modern Type 2 hypervisors running real applications. These changes have been incorporated into the latest ARM architecture.