A design and verification methodology for secure isolated regions

By Rohit Sinha, Manuel Costa, Akash Lal, Nuno P. Lopes, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani. 2016

71 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, 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 Computer Networks and Communications

In Signal Processing

Citations in the corpus

EnclaveDB: A Secure Database Using SGX (2018, background): “Recent research has shown that it is possible to automatically enforce and verify confidentiality for reasonably sized applications at low runtime overheads [21].”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “While techniques for verifying security properties of enclave programs [62, 63] have been developed, they rely on models of the underlying enclave platform.”
A compiler and verifier for page access oblivious computation (2017, methodology): “Moat [19] and SlashConf [18] verify the enclave binaries to prove an absence of explicit leaks; side channels are out of their scope.”
T-SGX: Eradicating Controlled-Channel Attacks Against Enclave Programs (2017, background): “Moat [56] and CONFIDENTIAL [55] design verification methodologies for enclave programs to check whether they are secure.”
Komodo: Using verification to disentangle secure-enclave hardware from software (2017, background): “Work complementary to ours provides security guarantees for SGX enclaves [33, 80, 81], and could be adapted for Komodo.”
SGX-Shield: Enabling Address Space Layout Randomization for SGX Programs (2017, background): “[55] introduce a runtime library that offers an interface to securely communicate with the external party of the enclave.”
Oblivious Multi-Party Machine Learning on Trusted Processors (2016, background): “We assume that all parties agree on the machine learning code that gets access to their datasets, after inspecting the code or using automated verification [60] to ascertain its trustworthiness.”
Keystone: an open framework for architecting trusted execution environments (2020, background): “The enclave can defend itself against explicit or implicit information leakage via the SM or the edge call API with known defenses [83, 84].”