Automatically Generating Secure Wrappers for SGX Enclaves from Separation Logic Specifications
No abstract available.
Related papers
- Automatic enforcement of expressive security policies using enclaves OOPSLA 2016
- SGXElide: enabling enclave code secrecy via self-modification CGO 2018
- Cerisier: A Program Logic for Attestation in a Capability Machine PLDI 2026
- Securing Interruptible Enclaved Execution on Small Microprocessors TOPLAS 2021
- HasTEE: Programming Trusted Execution Environments with Haskell Haskell 2023
- SecCSL: Security Concurrent Separation Logic CAV 2019
- Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation PLDI 2023
- A design and verification methodology for secure isolated regions PLDI 2016