Los puntos clave no están disponibles para este artículo en este momento.
Las tecnologías de Virtualización Encriptada Segura de AMD permiten la computación confidencial al proteger las máquinas virtuales de software altamente privilegiado como los hipervisores. En este trabajo, desarrollamos el primer modelo simbólico integral de la interfaz de software de la última iteración de SEV llamada SEV Paginación Anidada Segura (SEV-SNP). Nuestro modelo abarca la atestación remota, derivación de claves, intercambio de páginas y migración en vivo. Analizamos la seguridad de la interfaz de software de SEV-SNP verificando propiedades críticas de secreto, autenticación, atestación y frescura, y encontramos que la naturaleza independiente de la plataforma de los mensajes intercambiados entre los huéspedes de SNP y el firmware del Procesador Seguro de AMD presenta una debilidad en el diseño. Mostramos múltiples formas de explotar esta debilidad, incluida la compromisión de la integridad del informe de atestación, y sugerimos ligeras modificaciones al diseño que permiten a terceros detectar migraciones de huéspedes a plataformas vulnerables.
Paradžik et al. (Vier,) estudiaron esta cuestión.