Formal Abstractions for Attested Execution Secure Processors

By Rafael Pass, Elaine Shi, Florian Tramèr. 2017

133 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Hardware and Architecture

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

1. Florian Tramèr
2. Dawn Song
3. Dan Boneh
4. Yang Zhang
5. Mario Fritz
6. Michael Backes
7. Nicholas Carlini
8. Nicolas Papernot

In Hardware and Architecture

1. Dan Boneh
2. Dawn Song
3. Florian Tramèr
4. Raymond Cheng
5. Nicholas Hynes
6. Ari Juels
7. Warren He
8. Mario Fritz

Citations in the corpus

• Slalom: Fast, Verifiable and Private Execution of Neural Networks in Trusted Hardware (2018, methodology): “While SGX covers many software and hardware attack vectors, there is a large and prominent class of side-channel attacks that it explicitly does not address (Costan & Devadas, 2016; Tramèr et al., 2017).”
• Ekiden: A Platform for Confidentiality-Preserving, Trustworthy, and Performant Smart Contracts (2018, positive): “To formally model attested execution on trusted hardware, we adopt the ideal functionality Gatt defined in [70].”
• IRON: Functional Encryption using Intel SGX (2017, methodology): “A detailed comparison of these systems to Intel SGX is covered in [20].”
• A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “model the cryptography of this scheme, and refer the reader to [54] for a formal treatment of this subject.”
• Sealed-Glass Proofs: Using Transparent Enclaves to Prove and Sell Knowledge (2017, methodology): “[32] (in the GUC framework) and the model of Barbosa et al.”
• Tesseract: Real-Time Cryptocurrency Exchange using Trusted Hardware (2017, background): “Pass, Shi, and Tramèr give a formal modeling of trusted hardware and remote attestation [68].”
• MLCapsule: Guarded Offline Deployment of Machine Learning as a Service (2018, background): “Pass, Shi, and Tramèr [37] proposed an abstraction of attested execution in the universal composability (UC) model.”
• Secure Multiparty Computation from SGX (2017, background): “In recent independent work Pass, Shi and Tramer [36] formalize attestation guarantees offered by trusted hardware in the Universal Composability setting, and consider the feasibility of achieving UC-secure MPC starting from a hardware assumption formalized in very much the same style as we model SGX”
• ROTE: Rollback Protection for Trusted Execution (2017, background): “Several recently proposed SGX systems [39, 40, 41, 13, 42, 43, 44, 45] consider an adversary model with an untrusted OS.”