Biblio

One of the essential features of confidential computing is the ability to attest to an application remotely. Remote attestation ensures that the right code is running in the correct environment. We need to ensure that all components that an adversary might use to impact the integrity, confidentiality, and consistency of an application are attested. Which components need to be attested is defined with the help of a policy. Verification of the policy is performed with the help of an attestation engine. Since remote attestation bootstraps the trust in remote applications, any vulnerability in the attestation mechanism can therefore impact the security of an application. Moreover, mistakes in the attestation policy can result in data, code, and secrets being vulnerable. Our work focuses on 1) how we can verify the attestation mechanisms and 2) how to verify the policy to ensure that data, code, and secrets are always protected.

With a broad spectrum of technologies for the protection of personal data, it is important to be able to reliably compare these technologies to choose the most suitable one for a given problem. Although technologies like Homomorphic Encryption have matured over decades, Confidential Computing is still in its infancy with not only informal but also incomplete and even conflicting definitions by the Confidential Computing Consortium (CCC). In this work, we present key issues in definitions and comparison among existing technologies by CCC. We also provide recommendations to achieve clarity and precision in the definitions as well as fair and scientific comparison among existing technologies. We emphasize on the need of formal definitions of the terms and pose it as an open challenge to the community.

In August 2020, Intel asked the research community for feedback on the newly offered architecture extensions, called Intel Trust Domain Extensions (TDX), which give more control to Trust Domains (TDs) over processor resources. One of the key features of these extensions is the remote attestation mechanism, which provides a unified report verification mechanism for TDX and its predecessor Software Guard Extensions (SGX). Based on our experience and intuition, we respond to the request for feedback by formally specifying the attestation mechanism in the TDX using ProVerif's specification language. Although the TDX technology seems very promising, the process of formal specification reveals a number of subtle discrepancies in Intel's specifications that could potentially lead to design and implementation flaws. After resolving these discrepancies, we also present fully automated proofs that our specification of TD attestation preserves the confidentiality of the secret and authentication of the report by considering the state-of-the-art Dolev-Yao adversary in the symbolic model using ProVerif. We have submitted the draft to Intel, and Intel is in the process of making the changes.

Trust is of paramount concern for tenants to deploy their security-sensitive services in the cloud. The integrity of virtual machines (VMs) in which these services are deployed needs to be ensured even in the presence of powerful adversaries with administrative access to the cloud. Traditional approaches for solving this challenge leverage trusted computing techniques, e.g., vTPM, or hardware CPU extensions, e.g., AMD SEV. But, they are vulnerable to powerful adversaries, or they provide only load time (not runtime) integrity measurements of VMs. We propose TRIGLAV, a protocol allowing tenants to establish and maintain trust in VM runtime integrity of software and its configuration. TRIGLAV is transparent to the VM configuration and setup. It performs an implicit attestation of VMs during a secure login and binds the VM integrity state with the secure connection. Our prototype's evaluation shows that TRIGLAV is practical and incurs low performance overhead (\textbackslashtextless 6%).

Intel has recently offered third-party attestation services, called Data Center Attestation Primitives (DCAP), for a data center to create its own attestation infrastructure. These services address the availability concerns and improve the performance as compared to the remote attestation based on Enhanced Privacy ID (EPID). Practical developments, such as Hyperledger Avalon, have already planned to support DCAP in their roadmap. However, the lack of formal proof for DCAP leads to security concerns. To fill this gap, we propose an automated, rigorous, and sound formal approach to specify and verify the remote at-testation based on Intel SGX DCAP under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. In the proposed approach, the data center configuration and operational policies are specified to generate the symbolic model, and security goals are specified as security properties to produce verification results. The evaluation of non-Quoting Verification Enclave-based DCAP indicates that the confidentiality of secrets and integrity of data is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX DCAP during formal specification.

Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX attestation during formal specification.

Users of online services such as messaging, code hosting and collaborative document editing expect the services to uphold the integrity of their data. Despite providers' best efforts, data corruption still occurs, but at present service integrity violations are excluded from SLAs. For providers to include such violations as part of SLAs, the competing requirements of clients and providers must be satisfied. Clients need the ability to independently identify and prove service integrity violations to claim compensation. At the same time, providers must be able to refute spurious claims. We describe LibSEAL, a SEcure Audit Library for Internet services that creates a non-repudiable audit log of service operations and checks invariants to discover violations of service integrity. LibSEAL is a drop-in replacement for TLS libraries used by services, and thus observes and logs all service requests and responses. It runs inside a trusted execution environment, such as Intel SGX, to protect the integrity of the audit log. Logs are stored using an embedded relational database, permitting service invariant violations to be discovered using simple SQL queries. We evaluate LibSEAL with three popular online services (Git, ownCloud and Dropbox) and demonstrate that it is effective in discovering integrity violations, while reducing throughput by at most 14%.

Third-party storage services pose the risk of integrity and confidentiality violations as the current storage policy enforcement mechanisms are spread across many layers in the system stack. To mitigate these security vulnerabilities, we present the design and implementation of Pesos, a Policy Enhanced Secure Object Store (Pesos) for untrusted third-party storage providers. Pesos allows clients to specify per-object security policies, concisely and separately from the storage stack, and enforces these policies by securely mediating the I/O in the persistence layer through a single unified enforcement layer. More broadly, Pesos exposes a rich set of storage policies ensuring the integrity, confidentiality, and access accounting for data storage through a declarative policy language. Pesos enforces these policies on untrusted commodity platforms by leveraging a combination of two trusted computing technologies: Intel SGX for trusted execution environment (TEE) and Kinetic Open Storage for trusted storage. We have implemented Pesos as a fully-functional storage system supporting many useful end-to-end storage features, and a range of effective performance optimizations. We evaluated Pesos using a range of micro-benchmarks, and real-world use cases. Our evaluation shows that Pesos incurs reasonable performance overheads for the enforcement of policies while keeping the trusted computing base (TCB) small.

Memory-safety violations are the primary cause of security and reliability issues in software systems written in unsafe languages. Given the limited adoption of decades-long research in software-based memory safety approaches, as an alternative, Intel released Memory Protection Extensions (MPX)–-a hardware-assisted technique to achieve memory safety. In this work, we perform an exhaustive study of Intel MPX architecture along three dimensions: (a) performance overheads, (b) security guarantees, and (c) usability issues. We present the first detailed root cause analysis of problems in the Intel MPX architecture through a cross-layer dissection of the entire system stack, involving the hardware, operating system, compilers, and applications. To put our findings into perspective, we also present an in-depth comparison of Intel MPX with three prominent types of software-based memory safety approaches. Lastly, based on our investigation, we propose directions for potential changes to the Intel MPX architecture to aid the design space exploration of future hardware extensions for memory safety. A complete version of this work appears in the 2018 proceedings of the ACM on Measurement and Analysis of Computing Systems.

Content-based routing (CBR) is a powerful model that supports scalable asynchronous communication among large sets of geographically distributed nodes. Yet, preserving privacy represents a major limitation for the wide adoption of CBR, notably when the routers are located in public clouds. Indeed, a CBR router must see the content of the messages sent by data producers, as well as the filters (or subscriptions) registered by data consumers. This represents a major deterrent for companies for which data is a key asset, as for instance in the case of financial markets or to conduct sensitive business-to-business transactions. While there exists some techniques for privacy-preserving computation, they are either prohibitively slow or too limited to be usable in real systems. In this paper, we follow a different strategy by taking advantage of trusted hardware extensions that have just been introduced in off-the-shelf processors and provide a trusted execution environment. We exploit Intel's new software guard extensions (SGX) to implement a CBR engine in a secure enclave. Thanks to the hardware-based trusted execution environment (TEE), the compute-intensive CBR operations can operate on decrypted data shielded by the enclave and leverage efficient matching algorithms. Extensive experimental evaluation shows that SGX adds only limited overhead to insecure plaintext matching outside secure enclaves while providing much better performance and more powerful filtering capabilities than alternative software-only solutions. To the best of our knowledge, this work is the first to demonstrate the practical benefits of SGX for privacy-preserving CBR.