💻 computer science

Formal Verification of Secure Encrypted Virtualization

Este artículo presenta un marco formal que abstrae y verifica las garantías de seguridad de AMD Secure Encrypted Virtualization (SEV) para asegurar rigurosamente la confidencialidad, integridad y disponibilidad de los entornos de ejecución de confianza.

Autores originales: Hansika Weerasena, Amitabh Das, Prabhat Mishra

Publicado 2026-06-02

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Hansika Weerasena, Amitabh Das, Prabhat Mishra

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un rascacielos masivo y bullicioso (la Nube) donde cientos de empresas diferentes (Inquilinos) alquilan plantas de oficinas. En un edificio normal, el administrador del edificio (el Hipervisor) tiene una llave maestra que puede abrir cualquier puerta, espiar cualquier caja fuerte y leer cualquier documento en cualquier escritorio. Si el administrador es honesto, todo va bien. Pero, ¿qué pasa si el administrador es un espía o es hackeado? De repente, los secretos de todas las empresas están en riesgo.

Para resolver esto, las empresas comenzaron a construir Habitaciones Seguras dentro del edificio. Estas se llaman Entornos de Ejecución Confiables (TEEs, por sus siglas en inglés). Específicamente, este artículo se centra en una versión de alta tecnología de estas habitaciones llamada AMD SEV (Virtualización con Cifrado Seguro).

Aquí está lo que hicieron los investigadores, explicado de forma sencilla:

1. El Problema: "Confía en mí" no es suficiente

La tecnología AMD SEV es como una oficina súper segura donde las paredes están hechas de un vidrio invisible e irrompible. Incluso el administrador del edificio (el Hipervisor) no puede ver el interior ni tocar nada. El propio hardware de la computadora cifra los datos para que, si alguien intenta robar el disco duro, solo obtenga un montón de información cifrada sin sentido.

Sin embargo, las personas que construyeron estas habitaciones escribieron un manual (la especificación) explicando cómo funcionan. Pero un manual son solo palabras en una página. No demuestra que la habitación sea realmente segura. Podría haber una pequeña grieta en el vidrio, o una puerta secreta que los arquitectos olvidaron mencionar. En el mundo de la seguridad, "creemos que es seguro" no es suficiente; necesitas una prueba matemática.

2. La Solución: El "Plano Matemático"

Los autores de este artículo decidieron dejar de suponer y empezar a demostrar. Construyeron un marco de verificación formal.

Piensa en esto como un arquitecto que no solo dibuja un cuadro del edificio, sino que crea una simulación matemática perfecta de este. Luego, ejecutan una "prueba de estrés digital" en esta simulación para ver si se rompe bajo cualquier ataque posible.

Hicieron esto de dos maneras principales:

Abstracción de Diseño: Tradujeron el complejo y desordenado manual técnico de AMD SEV en un modelo matemático limpio y simplificado. Es como convertir un libro de instrucciones de 500 páginas en un diagrama de flujo claro.
Verificación de Propiedades: Escribieron una lista de "reglas" (propiedades) que la habitación debe seguir para ser considerada segura. Luego, usaron un programa de computadora (llamado Rosette) para comprobar si el modelo matemático alguna vez rompe estas reglas.

3. Las Tres Reglas del Juego (CIA)

Los investigadores comprobaron la seguridad de las habitaciones AMD SEV frente a tres objetivos principales, conocidos como CIA (Confidencialidad, Integridad y Disponibilidad):

Confidencialidad (El "Guardián de Secretos"):
- La Regla: Nadie, ni siquiera el administrador del edificio, debería poder leer lo que sucede dentro de la habitación.
- La Prueba: Simularon a un espía intentando mirar dentro. Comprobaron si el espía podría alguna vez ver la "memoria privada" o los "registros de la CPU" (el cerebro de la computadora) del huésped.
- El Resultado: Verificaron 14 reglas diferentes. Las matemáticas demostraron que, mientras el hardware de AMD funcione según lo diseñado, el espía no puede ver los secretos.
Integridad (El "Sello a Prueba de Manipulación"):
- La Regla: Nadie debería poder cambiar sigilosamente los documentos dentro de la habitación o intercambiarlos por unos falsos.
- La Prueba: Simularon a un saboteador intentando reescribir el código del huésped o engañar al sistema para que piense que una versión antigua y vulnerable del software es la actual.
- El Resultado: Verificaron 7 reglas. Las matemáticas mostraron que el sistema tiene una "tabla de mapa inverso" (como un registro de seguridad estricto) que evita que alguien intercambie páginas o retroceda en el tiempo a un estado inseguro.
Disponibilidad (El "Interruptor de Energía"):
- La Regla: La habitación debe funcionar cuando la necesites, y el administrador del edificio debe poder apagarla si es necesario.
- La Prueba: Comprobaron dos cosas:
  1. ¿Puede el administrador recuperar siempre el control? Sí. Las matemáticas demostraron que el administrador siempre puede pausar o detener al huésped.
  2. ¿Puede el huésped ejecutarse siempre sin que se le agote el tiempo? No. Las matemáticas demostraron que, si el administrador es malicioso, este puede elegir no dejar que el huésped se ejecute nunca. El sistema garantiza que el administrador pueda detenerte, pero no garantiza que el administrador te deje ejecutar. Esta es una limitación conocida de la tecnología.

4. Las "Actualizaciones" que Probaron

El artículo no solo analizó la versión básica de AMD SEV. También probaron dos actualizaciones más nuevas y fuertes:

SEV-ES: Añade una capa de protección para el "cerebro" de la computadora (los registros de la CPU). Antes, el administrador podía ver qué estaba pensando la computadora cuando se pausaba. Ahora, incluso los pensamientos están cifrados.
SEV-SNP: Añade un sistema de "notario" para las páginas de memoria. Asegura que una página de memoria pertenezca a la persona correcta y no haya sido intercambiada o manipulada.

5. El Veredicto

Los investigadores construyeron con éxito un gemelo digital del sistema AMD SEV y lo sometieron a una serie de 23 pruebas de seguridad diferentes.

Confidencialidad: Pasó todas las pruebas.
Integridad: Pasó todas las pruebas.
Disponibilidad: Pasó la prueba del control del administrador, pero identificó correctamente que el huésped no puede forzar al administrador a dejarlo ejecutar (lo cual es una característica de diseño, no un error).

En Resumen

Este artículo es como un equipo de ingenieros forenses que tomaron una caja fuerte de alta tecnología, construyeron un modelo matemático perfecto de ella y demostraron al mundo que, según las leyes de la matemática, la caja fuerte no puede ser abierta por el administrador del edificio. No se limitaron a decir: "Parece segura". Dijeron: "Hemos calculado cada posible forma de romperla y hemos demostrado que no se puede romper".

Esto otorga a los usuarios de la nube un nivel mucho mayor de confianza en que sus datos están seguros, incluso si el propio software del proveedor de la nube es hackeado.

Resumen Técnico: Verificación Formal de la Virtualización Segura Cifrada

Declaración del Problema

Los entornos modernos de computación en la nube albergan inquilinos mutuamente desconfiados en una infraestructura física compartida, lo que crea riesgos significativos para los ataques entre inquilinos y basados en el hipervisor. Aunque los Entornos de Ejecución Confiables (TEE), particularmente los TEE basados en máquinas virtuales (VM) como AMD Secure Encrypted Virtualization (SEV), ofrecen aislamiento asistido por hardware para proteger la confidencialidad e integridad del código y los datos, su documentación arquitectónica carece frecuentemente de garantías de seguridad formales. La complejidad de estos diseños y el potencial de fallos sutiles de implementación requieren una verificación formal rigurosa para asegurar que las VMs huéspedes permanezcan confidenciales y sin modificaciones durante todo su ciclo de vida, incluso ante un hipervisor malicioso o software de sistema comprometido. Los esfuerzos de verificación existentes para otros TEE (por ejemplo, Intel SGX, ARM TrustZone) no son directamente aplicables a los TEE basados en VM debido a diferencias fundamentales en los modelos de confianza, mecanismos de ejecución e interacciones del sistema.

Metodología

Los autores proponen un marco de verificación formal que utiliza la abstracción a nivel de diseño y de propiedad para modelar y verificar las VMs confidenciales de AMD SEV. La metodología procede de la siguiente manera:

Estrategia de Abstracción:
- Abstracción basada en el diseño: Captura todos los comportamientos definidos arquitectónicamente y las transiciones de estado de la especificación de SEV para formar un modelo operativo base.
- Abstracción basada en propiedades: Simplifica el sistema centráéndose únicamente en los componentes y comportamientos relevantes para propiedades de seguridad específicas (Confidencialidad, Integridad, Disponibilidad).
Modelado Formal:
- La arquitectura AMD SEV (incluyendo SEV-base, SEV-ES y SEV-SNP) se modela utilizando el lenguaje Rosette, un lenguaje de programación asistido por un solucionador (solver-aided).
- El modelo incorpora variables simbólicas, aserciones y funciones asistidas por un solucionador para representar estructuras de datos con estado (por ejemplo, la Tabla de Contexto del Huésped, la Tabla ASID, la Tabla de Mapeo Inverso) y funciones de la Interfaz Binaria de Aplicación (ABI) (por ejemplo, LAUNCH_START, ACTIVATE, DECOMMISSION).
- El modelo de amenazas asume un adversario privilegiado (hipervisor) capaz de pausar, terminar y manipular estados del sistema, pero restringido por mecanismos de aislamiento forzados por el hardware.
Definición de Propiedades y Verificación:
- El marco define modelos formales para la Confidencialidad (prevenir la observación no autorizada de memoria/registros), la Integridad (prevenir la modificación o repetición no autorizada de datos/estado) y la Disponibilidad (asegurar la vitalidad tanto para el host como para el huésped).
- La verificación se realiza utilizando el motor de ejecución simbólica de Rosette junto con el solucionador SMT Z3. El sistema explora rutas de ejecución para validar restricciones y buscar contraejemplos.

Contribuciones Clave

El artículo realiza las siguientes contribuciones específicas:

Modelo Formal Exhaustivo: Un modelo formal que define los límites de seguridad de las VMs confidenciales, considerando explícitamente adversarios con acceso a vectores de ataque avanzados.
Definiciones Formales de CIA: Modelado formal de las nociones de Confidencialidad, Integridad y Disponibilidad (CIA) específicamente adaptadas para TEE basados en VM.
Implementación de AMD SEV: Un modelo formal detallado de la arquitectura AMD SEV (cubriendo SEV-base, SEV-ES y SEV-SNP) desarrollado en Rosette, incluyendo estructuras de datos con estado y transiciones de ciclo de vida.
Análisis Comparativo: Una evaluación crítica de las medidas de seguridad de AMD SEV en comparación con otros TEE basados en VM como Intel TDX, destacando divergencias arquitectónicas en la raíz de confianza, atestación y gestión de claves.
Resultados de Verificación Formal: Verificación exitosa de AMD SEV frente a 23 propiedades de seguridad derivadas de las nociones de seguridad CIA.

Resultados Experimentales

Los autores implementaron el modelo y verificaron 23 propiedades en un entorno de CPU Apple M2 (16 GB de RAM):

Confidencialidad: Se verificaron 14 propiedades ( $CP_1$ – $CP_{14}$ ). Estas cubren la ejecución del cifrado de memoria, el aislamiento de ASID, el cifrado del estado de los registros (SEV-ES) y la validación de páginas (SEV-SNP). Todas las propiedades pasaron.
Integridad: Se verificaron 7 propiedades ( $IP_1$ – $IP_7$ ). Estas aseguran transiciones de estado de ciclo de vida válidas, atomicidad, prevención de ataques de reversión (rollback) y el manejo correcto de secretos durante la migración. Todas las propiedades pasaron.
Disponibilidad: Se modelaron 2 propiedades ( $AP_1$ $A P_{1}$ – $AP_2$ $A P_{2}$ ).
- $AP_1$ (Vitalidad del lado del Host): Verificada. El modelo confirma que el hipervisor siempre puede recuperar el control.
- $AP_2$ (Vitalidad del lado del Huésped): No Verificada. El modelo confirma que la vitalidad del lado del huésped (garantizar el progreso frente a un hipervisor malicioso) no puede garantizarse en las tecnologías SEV actuales, ya que el hipervisor retiene el control de la planificación (scheduling).

Métricas de Verificación:

Tiempo de verificación de propiedades de confidencialidad: ~20.52 segundos.
Tiempo de verificación de propiedades de integridad: ~12.45 segundos.
Tiempo de verificación de propiedades de disponibilidad: ~3.67 segundos.

Significación y Reivindicaciones

El artículo afirma proporcionar una base rigurosa para definir y verificar atributos de seguridad clave para salvaguardar los entornos de ejecución. Al establecer definiciones formales de CIA en el contexto de los TEE basados en VM y verificar con éxito la arquitectura AMD SEV, el trabajo demuestra que los métodos formales pueden aplicarse eficazmente a sistemas complejos diseñados conjuntamente por hardware y software.

Los autores sostienen que su enfoque ofrece la mayor garantía de que la arquitectura aplica correctamente las promesas de aislamiento y protección, abordando una brecha crítica donde los métodos basados en simulación fallan al no cubrir los casos límite (edge cases). El trabajo destaca que, si bien AMD SEV proporciona fuertes garantías de confidencialidad e integridad (verificadas por el modelo), inherentemente carece de garantías de disponibilidad para el huésped frente a un hipervisor malicioso. El artículo concluye que este marco formal allana el camino para futuras investigaciones en la seguridad de los entornos de virtualización TEE y ofrece una solución escalable para validar la postura de seguridad de los servicios en la nube.