A Formal Foundation for Secure Remote Execution of Enclaves

By Pramod Subramanyan, Rohit Sinha, Ilia A. Lebedev, Srini Devadas, Sanjit A. Seshia. 2017

151 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Hardware and Architecture, Privacy & Security, Signal Processing

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

In Hardware and Architecture

In Privacy & Security

In Signal Processing

Citations in the corpus

Advances and Open Problems in Federated Learning (2019, background): “In particular, when the verifier knows (or can reproduce) which binary should run in the secure enclaves, TEEs will be able to provide a notion of integrity (the code execution cannot be affected, except by the inputs), and an attestation (the TEE can prove that a specific binary is executing and wh”
Robust Aggregation for Federated Learning (2019, background): “, secure enclaves [81] in conjunction with our approach could guarantee Byzantine robustness in federated learning.”
Slalom: Fast, Verifiable and Private Execution of Neural Networks in Trusted Hardware (2018, background): “We refer the interested reader to (Pass et al., 2017; Fisch et al., 2017; Subramanyan et al., 2017) for different attempts at such formalisms.”
Keystone: an open framework for architecting trusted execution environments (2020, background): “A careful and ground-up design with verified components [43, 55, 69] may provide stronger guarantees and Keystone can help explore designs which combine these with hardware protection [41, 85].”
DAWG: A Defense Against Cache Timing Attacks in Speculative Execution Processors (2018, result): “Figure 11 illustrates DAWG’s non-interference property, which can be proven in a manner similar to the proof for the Sanctum processor’s cache partitioning scheme [50].”
HardFails: Insights into Software-Exploitable Hardware Bugs (2019, methodology): “A formal veriﬁcation methodology for SGX and Sanctum en-claves under a limited adversary was introduced in [67].”