Formal Security Analysis of the AMD SEV-SNP Software Interface

• URL: http://arxiv.org/abs/2403.10296v4
• Date: Thu, 17 Oct 2024 11:25:46 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:
• 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 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.

Related papers

• The Impact of SBOM Generators on Vulnerability Assessment in Python: A Comparison and a Novel Approach [56.4040698609393]
  Software Bill of Materials (SBOM) has been promoted as a tool to increase transparency and verifiability in software composition. Current SBOM generation tools often suffer from inaccuracies in identifying components and dependencies. We propose PIP-sbom, a novel pip-inspired solution that addresses their shortcomings.
  arXiv  Detail & Related papers  (2024-09-10T10:12:37Z)
• SETC: A Vulnerability Telemetry Collection Framework [0.0]
  This paper introduces the Security Exploit Telemetry Collection (SETC) framework. SETC generates reproducible vulnerability exploit data at scale for robust defensive security research. This research enables scalable exploit data generation to drive innovations in threat modeling, detection methods, analysis techniques, and strategies.
  arXiv  Detail & Related papers  (2024-06-10T00:13:35Z)
• Securing Federated Learning with Control-Flow Attestation: A Novel Framework for Enhanced Integrity and Resilience against Adversarial Attacks [2.28438857884398]
  Federated Learning (FL) as a distributed machine learning paradigm has introduced new cybersecurity challenges. This study proposes an innovative security framework inspired by Control-Flow (CFA) mechanisms, traditionally used in cybersecurity. We authenticate and verify the integrity of model updates across the network, effectively mitigating risks associated with model poisoning and adversarial interference.
  arXiv  Detail & Related papers  (2024-03-15T04:03:34Z)
• 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)
• SISSA: Real-time Monitoring of Hardware Functional Safety and Cybersecurity with In-vehicle SOME/IP Ethernet Traffic [49.549771439609046]
  We propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security. Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication. Extensive experimental results show the effectiveness and efficiency of SISSA.
  arXiv  Detail & Related papers  (2024-02-21T03:31:40Z)
• 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)
• DASICS: Enhancing Memory Protection with Dynamic Compartmentalization [7.802648283305372]
  We present the DASICS (Dynamic in-Address-Space Isolation by Code Segments) secure processor design. It offers dynamic and flexible security protection across multiple privilege levels, addressing data flow protection, control flow protection, and secure system calls. We have implemented hardware FPGA prototypes and software QEMU simulator prototypes based on DASICS, along with necessary modifications to system software for adaptability.
  arXiv  Detail & Related papers  (2023-10-10T09:05:29Z)
• 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)

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.