Formal Security Analysis of the AMD SEV-SNP Software Interface
- URL: http://arxiv.org/abs/2403.10296v3
- Date: Tue, 23 Jul 2024 12:56:18 GMT
- Title: Formal Security Analysis of the AMD SEV-SNP Software Interface
- Authors: Petar Paradžik, Ante Derek, Marko Horvat,
- Abstract summary: AMD Secure Encrypted technologies enable confidential computing by protecting virtual machines from highly privileged software such as hypervisors.
We develop the first, comprehensive symbolic model of the software interface of the latest SEV iteration called SEV Secure Nested Paging (SEV-SNP)
- Score: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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 by verifying critical secrecy, authentication, attestation and freshness properties, and find that the platform-agnostic nature of messages exchanged between SNP guests and the AMD Secure Processor firmware presents a weakness of the design. We show multiple ways of exploiting this weakness, including the compromise of attestation report integrity, and suggest slight modifications to the design which let third parties detect guest migrations to vulnerable platforms
Related papers
- WeSee: Using Malicious #VC Interrupts to Break AMD SEV-SNP [2.8436446946726557]
AMD SEV-SNP offers VM-level trusted execution environments (TEEs) to protect sensitive cloud workloads.
WeSee attack injects malicious #VC into a victim VM's CPU to compromise the security guarantees of AMD SEV-SNP.
Case-studies demonstrate that WeSee can leak sensitive VM information (kTLS keys for NGINX), corrupt kernel data (firewall rules), and inject arbitrary code.
arXiv Detail & Related papers (2024-04-04T15:30:13Z) - Trustworthy confidential virtual machines for the masses [1.6503985024334136]
We present Revelio, an approach that allows confidential virtual machine (VM)-based workloads to be designed and deployed in a way that disallows tampering even by the service providers.
We focus on web-facing workloads, protect them leveraging SEV-SNP, and enable end-users to remotely attest them seamlessly each time a new web session is established.
arXiv Detail & Related papers (2024-02-23T11:54:07Z) - HOACS: Homomorphic Obfuscation Assisted Concealing of Secrets to Thwart Trojan Attacks in COTS Processor [0.6874745415692134]
We propose a software-oriented countermeasure to ensure the confidentiality of secret assets against hardware Trojans.
The proposed solution does not require any supply chain entity to be trusted and does not require analysis or modification of the IC design.
We have implemented the proposed solution to protect the secret key within the Advanced Encryption Standard (AES) program and presented a detailed security analysis.
arXiv Detail & Related papers (2024-02-15T04:33:30Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs)
TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks.
We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
arXiv Detail & Related papers (2024-01-17T00:56:23Z) - The Security and Privacy of Mobile Edge Computing: An Artificial Intelligence Perspective [64.36680481458868]
Mobile Edge Computing (MEC) is a new computing paradigm that enables cloud computing and information technology (IT) services to be delivered at the network's edge.
This paper provides a survey of security and privacy in MEC from the perspective of Artificial Intelligence (AI)
We focus on new security and privacy issues, as well as potential solutions from the viewpoints of AI.
arXiv Detail & Related papers (2024-01-03T07:47:22Z) - Tamper-Evident Pairing [55.2480439325792]
Tamper-Evident Pairing (TEP) is an improvement of the Push-Button configuration (PBC) standard.
TEP relies on the Tamper-Evident Announcement (TEA), which guarantees that an adversary can neither tamper a transmitted message without being detected, nor hide the fact that the message has been sent.
This paper provides a comprehensive overview of the TEP protocol, including all information needed to understand how it works.
arXiv Detail & Related papers (2023-11-24T18:54:00Z) - Establishing Dynamic Secure Sessions for ECQV Implicit Certificates in Embedded Systems [0.0]
We present a design that utilizes the Station to Station (STS) protocol with implicit certificates.
We show that with a slight computational increase of 20% compared to a static ECDSA key derivation, we are able to mitigate many session-related security vulnerabilities.
arXiv Detail & Related papers (2023-11-19T22:40:21Z) - Putting a Padlock on Lambda -- Integrating vTPMs into AWS Firecracker [49.1574468325115]
Software services place implicit trust in the cloud provider, without an explicit trust relationship.
There is currently no cloud provider that exposes Trusted Platform Module capabilities.
We improve trust by integrating a virtual TPM device into the Firecracker, originally developed by Amazon Web Services.
arXiv Detail & Related papers (2023-10-05T13:13:55Z) - SyzTrust: State-aware Fuzzing on Trusted OS Designed for IoT Devices [67.65883495888258]
We present SyzTrust, the first state-aware fuzzing framework for vetting the security of resource-limited Trusted OSes.
SyzTrust adopts a hardware-assisted framework to enable fuzzing Trusted OSes directly on IoT devices.
We evaluate SyzTrust on Trusted OSes from three major vendors: Samsung, Tsinglink Cloud, and Ali Cloud.
arXiv Detail & Related papers (2023-09-26T08:11:38Z) - Smart Home, security concerns of IoT [91.3755431537592]
The IoT (Internet of Things) has become widely popular in the domestic environments.
People are renewing their homes into smart homes; however, the privacy concerns of owning many Internet connected devices with always-on environmental sensors remain insufficiently addressed.
Default and weak passwords, cheap materials and hardware, and unencrypted communication are identified as the principal threats and vulnerabilities of IoT devices.
arXiv Detail & Related papers (2020-07-06T10:36:11Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.