💻 computer science

Formal Verification of Secure Encrypted Virtualization

This paper presents a formal framework that abstracts and verifies the security guarantees of AMD Secure Encrypted Virtualization (SEV) to rigorously ensure the confidentiality, integrity, and availability of trusted execution environments.

Original authors: Hansika Weerasena, Amitabh Das, Prabhat Mishra

Published 2026-06-02

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Hansika Weerasena, Amitabh Das, Prabhat Mishra

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a massive, bustling skyscraper (the Cloud) where hundreds of different companies (Tenants) rent office floors. In a normal building, the building manager (the Hypervisor) has a master key that can open any door, peek into any safe, and read any document on any desk. If the manager is honest, everyone is fine. But what if the manager is a spy, or gets hacked? Suddenly, every company's secrets are at risk.

To solve this, companies started building Secure Rooms inside the building. These are called Trusted Execution Environments (TEEs). Specifically, this paper focuses on a high-tech version of these rooms called AMD SEV (Secure Encrypted Virtualization).

Here is what the researchers did, explained simply:

1. The Problem: "Trust Me" isn't enough

The AMD SEV technology is like a super-secure office where the walls are made of invisible, unbreakable glass. Even the building manager (the Hypervisor) cannot see inside or touch anything. The computer hardware itself encrypts the data so that if anyone tries to steal the hard drive, they just get a pile of scrambled gibberish.

However, the people who built these rooms wrote a manual (the specification) explaining how they work. But a manual is just words on a page. It doesn't prove the room is actually secure. There might be a tiny crack in the glass, or a secret door the architects forgot to mention. In the world of security, "we think it's safe" isn't good enough; you need mathematical proof.

2. The Solution: The "Mathematical Blueprint"

The authors of this paper decided to stop guessing and start proving. They built a formal verification framework.

Think of this like an architect who doesn't just draw a picture of the building but creates a perfect, mathematical simulation of it. They then run a "digital stress test" on this simulation to see if it breaks under any possible attack.

They did this in two main ways:

Design Abstraction: They translated the complex, messy technical manual of AMD SEV into a clean, simplified mathematical model. It's like turning a 500-page instruction book into a clear flowchart.
Property Checking: They wrote a list of "rules" (properties) that the room must follow to be considered safe. Then, they used a computer program (called Rosette) to check if the mathematical model ever breaks these rules.

3. The Three Rules of the Game (CIA)

The researchers checked the security of the AMD SEV rooms against three main goals, known as CIA:

Confidentiality (The "Secret Keeper"):
- The Rule: No one, not even the building manager, should be able to read what's happening inside the room.
- The Test: They simulated a spy trying to peek inside. They checked if the spy could ever see the "private memory" or the "CPU registers" (the brain of the computer) of the guest.
- The Result: They verified 14 different rules. The math proved that as long as the AMD hardware works as designed, the spy cannot see the secrets.
Integrity (The "Tamper-Proof Seal"):
- The Rule: No one should be able to sneakily change the documents inside the room or swap them for fake ones.
- The Test: They simulated a saboteur trying to rewrite the guest's code or trick the system into thinking an old, vulnerable version of the software is the current one.
- The Result: They verified 7 rules. The math showed that the system has a "reverse map table" (like a strict security log) that prevents anyone from swapping pages or rolling back time to an insecure state.
Availability (The "Power Switch"):
- The Rule: The room should work when you need it, and the building manager should be able to turn it off if they need to.
- The Test: They checked two things:
  1. Can the manager always get control back? Yes. The math proved the manager can always pause or stop the guest.
  2. Can the guest always run without being starved of time? No. The math proved that if the manager is malicious, they can choose to never let the guest run. The system guarantees the manager can stop you, but it doesn't guarantee the manager will let you run. This is a known limitation of the technology.

4. The "Upgrades" They Tested

The paper didn't just look at the basic version of AMD SEV. They also tested two newer, stronger upgrades:

SEV-ES: This adds a layer of protection for the "brain" of the computer (the CPU registers). Before, the manager could see what the computer was thinking when it paused. Now, even the thoughts are encrypted.
SEV-SNP: This adds a "notary" system for the memory pages. It ensures that a page of memory belongs to the right person and hasn't been swapped out or tampered with.

5. The Verdict

The researchers successfully built a digital twin of the AMD SEV system and ran it through a gauntlet of 23 different security tests.

Confidentiality: Passed all tests.
Integrity: Passed all tests.
Availability: Passed the test for the manager's control, but correctly identified that the guest cannot force the manager to let it run (which is a design feature, not a bug).

In a Nutshell

This paper is like a team of forensic engineers who took a high-tech safe, built a perfect mathematical model of it, and proved to the world that, according to the laws of math, the safe cannot be opened by the building manager. They didn't just say, "It looks secure." They said, "We have calculated every possible way to break it, and we proved it cannot be broken."

This gives cloud users a much higher level of confidence that their data is safe, even if the cloud provider's own software gets hacked.

Technical Summary: Formal Verification of Secure Encrypted Virtualization

Problem Statement

Modern cloud computing environments host mutually untrusted tenants on shared physical infrastructure, creating significant risks for cross-tenant and hypervisor-based attacks. While Trusted Execution Environments (TEEs), particularly VM-based TEEs like AMD Secure Encrypted Virtualization (SEV), offer hardware-assisted isolation to protect code and data confidentiality and integrity, their architectural documentation often lacks formal security guarantees. The complexity of these designs and the potential for subtle implementation flaws necessitate rigorous formal verification to ensure that guest VMs remain confidential and unmodified throughout their lifecycle, even in the presence of a malicious hypervisor or compromised system software. Existing verification efforts for other TEEs (e.g., Intel SGX, ARM TrustZone) are not directly applicable to VM-based TEEs due to fundamental architectural differences in trust models, enforcement mechanisms, and system interactions.

Methodology

The authors propose a formal verification framework that utilizes design-level and property-level abstraction to model and verify AMD SEV confidential VMs. The methodology proceeds as follows:

Abstraction Strategy:
- Design-based Abstraction: Captures all architecturally defined behaviors and state transitions from the SEV specification to form a baseline operational model.
- Property-based Abstraction: Simplifies the system by focusing only on components and behaviors relevant to specific security properties (Confidentiality, Integrity, Availability).
Formal Modeling:
- The AMD SEV architecture (including SEV-base, SEV-ES, and SEV-SNP) is modeled using the Rosette language, a solver-aided programming language.
- The model incorporates symbolic variables, assertions, and solver-aided functions to represent stateful data structures (e.g., Guest Context Table, ASID Table, Reverse Map Table) and Application Binary Interface (ABI) functions (e.g., LAUNCH_START, ACTIVATE, DECOMMISSION).
- The threat model assumes a privileged adversary (hypervisor) capable of pausing, terminating, and manipulating system states, but constrained by hardware-enforced isolation mechanisms.
Property Definition and Verification:
- The framework defines formal models for Confidentiality (preventing unauthorized observation of memory/registers), Integrity (preventing unauthorized modification or replay of data/state), and Availability (ensuring liveness for both host and guest).
- Verification is performed using Rosette's symbolic execution engine coupled with the Z3 SMT solver. The system explores execution paths to validate constraints and check for counterexamples.

Key Contributions

The paper makes the following specific contributions:

Comprehensive Formal Model: A formal model defining the security boundaries of confidential VMs, explicitly considering adversaries with access to advanced attack vectors.
Formal CIA Definitions: Formal modeling of Confidentiality, Integrity, and Availability notions specifically tailored for VM-based TEEs.
AMD SEV Implementation: A detailed formal model of the AMD SEV architecture (covering SEV-base, SEV-ES, and SEV-SNP) developed in Rosette, including stateful data structures and lifecycle transitions.
Comparative Analysis: A critical evaluation of AMD SEV security measures compared to other VM-based TEEs like Intel TDX, highlighting architectural divergences in root of trust, attestation, and key management.
Formal Verification Results: Successful formal verification of AMD SEV against 23 security properties derived from CIA security notions.

Experimental Results

The authors implemented the model and verified 23 properties on an Apple M2 CPU environment (16 GB RAM):

Confidentiality: 14 properties ( $CP_1$ – $CP_{14}$ ) were verified. These cover memory encryption enforcement, ASID isolation, register state encryption (SEV-ES), and page validation (SEV-SNP). All properties passed.
Integrity: 7 properties ( $IP_1$ – $IP_7$ ) were verified. These ensure valid lifecycle state transitions, atomicity, prevention of rollback attacks, and correct handling of secrets during migration. All properties passed.
Availability: 2 properties ( $AP_1$ $A P_{1}$ – $AP_2$ $A P_{2}$ ) were modeled.
- $AP_1$ (Host-side liveness): Verified. The model confirms the hypervisor can always regain control.
- $AP_2$ (Guest-side liveness): Not Verified. The model confirms that guest-side liveness (guaranteeing progress against a malicious hypervisor) cannot be guaranteed in current SEV technologies, as the hypervisor retains scheduling control.

Verification Metrics:

Confidentiality properties: ~20.52 seconds verification time.
Integrity properties: ~12.45 seconds verification time.
Availability properties: ~3.67 seconds verification time.

Significance and Claims

The paper claims to provide a rigorous foundation for defining and verifying key security attributes for safeguarding execution environments. By establishing formal definitions for CIA in the context of VM-based TEEs and successfully verifying the AMD SEV architecture, the work demonstrates that formal methods can be effectively applied to complex, hardware-software co-designed systems.

The authors assert that their approach offers the strongest assurance that the architecture correctly enforces isolation and protection guarantees, addressing a critical gap where simulation-based methods fail to cover edge cases. The work highlights that while AMD SEV provides strong confidentiality and integrity guarantees (verified by the model), it inherently lacks guarantees for guest-side availability against a malicious hypervisor. The paper concludes that this formal framework paves the way for future research in securing virtualized TEE environments and offers a scalable solution for validating the security posture of cloud services.