Symbolic Validation of SGX enclaves using Guardian
summary
Describes the notion of “orderliness” for Intel SGX enclaves—splitting enclave behavior into entry, secure, ocall, and exit phases with restrictions on access to and sanitisation of untrusted memory—and presents Guardian, an open-source symbolic-execution tool that automatically validates enclaves against those phase-specific policies and searches for common attack primitives. The talk covers how Guardian flags violations that indicate potential memory-corruption or interaction-with-untrusted-code vulnerabilities and reports results from evaluating real enclave samples where it found previously undetected issues.
AI-written summary · about
related talks
15mSecured Routines: Language-based Construction of Trusted Execution Environments
32mSecure Container with SGX: Protecting Secret in Cloud Environment
23mThe Guard's Dilemma: Efficient Code-Reuse Attacks Against Intel SGX
25mTelling Your Secrets without Page Faults...
38mOne Ring -3 To Secure Them All: Computing with Hardware Enclaves
36mAttacking & Defending Kubernetes TEE Enclaves in Critical Infrastructure
32mSecure Container with SGX: Protecting Secret in Cloud Environment
48mSGX Secure Enclaves in Practice: Security and Crypto Review