arXiv subjects

Ante Derek

Publications and source records attributed to Ante Derek.

2 recordsLinked to original sources

arXiv2024

Formal Security Analysis of the AMD SEV-SNP Software Interface

AMD Secure Encrypted Virtualization technologies enable confidential computing by protecting virtual machines from highly privileged software such as hypervisors. In this work, we develop the first, comprehensive symbolic model of the software interface of the latest SEV iteration called SEV Secure Nested Paging (SEV-SNP). Our model covers remote attestation, key derivation, page swap and live migration. We analyze the security of the software interface of SEV-SNP and formally prove that most critical secrecy, authentication, attestation and freshness properties do indeed hold in the model. Furthermore, we find that the platform-agnostic nature of messages exchanged between SNP guests and the AMD Secure Processor firmware presents a potential weakness in the design. We show how this weakness leads to formal attacks on multiple security properties, including the partial compromise of attestation report integrity, and discuss possible impacts and mitigations.

cs.CR↗

arXiv2023

Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves

We propose a protocol that explores a synergy between two TEE implementations: it brings SGX-like remote attestation to SEV VMs. We use the notion of a \emph{trusted guest owner}, implemented as an SGX enclave, to deploy, attest, and provision a SEV VM. This machine can, in turn, rely on the trusted owner to generate SGX-like attestation proofs on its behalf. Our protocol combines the application portability of SEV with the flexible remote attestation of SGX. We formalise our protocol and prove that it achieves the intended guarantees using the Tamarin prover. Moreover, we develop an implementation for our trusted guest owner together with example SEV machines, and put those together to demonstrate how our protocol can be used in practice; we use this implementation to evaluate our protocol in the context of creating \emph{accountable machine-learning models}. We also discuss how our protocol can be extended to provide a simple remote attestation mechanism for a heterogeneous infrastructure of trusted components.

cs.CR↗