Agenda

27 Set 2023 09:15

A Formal Analysis of AMD SEV-SNP

Aula C, edificio ZETA - Campus Scientifico via Torino

Speaker: Petar Paradzik, University of Zagreb

Abstract:
AMD Secure Encrypted Virtualization (AMD SEV) is a family of x86-64 technologies used for confidential computing and available for Epyc brand of microprocessors. AMD SEV technologies are designed to isolate virtual machines (VMs) from a hypervisor. Over the years AMD has introduced several generations of x86-64 technologies starting with SEV, which introduced hardware-accelerated main memory encryption, followed by SEV-ES (Encrypted State), which provided additional protections for a virtual machine's register state, and most recently SEV-SNP (Secure Nested Paging) which adds strong memory integrity protection and more. SEV-SNP, like its predecessors, is implemented as firmware running on an AMD Secure Processor (ASP) --- an isolated ARM core that runs independently of the main x86-64 cores. The firmware application binary interface (ABI) which SEV-SNP provides to a hypervisor for managing guest VMs has been officially specified and is available.  In addition, the SEV-SNP firmware was recently released as open-source.

In this lecture I will discuss how we used the Tamarin prover tool to formally verify the firmware ABI specification of AMD SEV-SNP with respect to desirable security properties under the specified threat model.                                                     

Bio Sketch:
I received my bachelor's degree in Mathematics and my master's degree in Computer Science and Mathematics at the Faculty of Science, Department of Mathematics in Zagreb. I spent several years in industry, mainly as an embedded software developer. Currently, I am a PhD student and teaching assistant at the Faculty of Electrical Engineering and Computing in Zagreb. My research area is formal analysis of security protocols.

Lingua

L'evento si terrà in inglese

Organizzatore

Stefano Calzavara

Cerca in agenda