Moat: Verifying Confidentiality of Enclave Programs

By Rohit Sinha, Sriram K. Rajamani, Sanjit A. Seshia, Kapil Vaswani. 2015

118 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Information Systems, 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 Information Systems

In Signal Processing

Citations in the corpus

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.”
CacheZoom: How SGX Amplifies The Power of Cache Attacks (2017, unknown): “Symmetric keys can be generated at runtime from a secure random entropy (using RDRAND instruction) and/or transferred through a public secure channel without the attacker knowledge.”
AsyncShock: Exploiting Synchronisation Bugs in Intel SGX Enclaves (2016, background): “Moat [24] makes a first step towards the verification of SGX enclaves.”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “Similar to Sanctum, we use a formal model of the SGX instruction set, following the approach of Moat [63], which models the SGX platform at the level of abstraction presented in the Intel Programmer Reference manual [30].”
A design and verification methodology for secure isolated regions (2016, methodology): “This is accomplished with either a whole-program analysis of UH, which is hard to scale for machine code, or fine-grained annotations which specify locations with secrets, which is cumbersome for machine code [40].”
A compiler and verifier for page access oblivious computation (2017, background): “Our formal model of an active adversary’s operations is similar to Moat [19] — we only extend Moat’s adversary with observations of page-level accesses.”
Inferring Fine-grained Control Flow Inside SGX Enclaves with Branch Shadowing (2016, methodology): “[54, 53] develop tools to verify the confidentiality of enclave programs.”
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].”
SGX-Shield: Enabling Address Space Layout Randomization for SGX Programs (2017, background): “To handle this problem, Moat [56] suggests a new programming model that checks services related to the security of the SGX program (e.”
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.”