Securing Access to Untrusted Services From TEEs with GateKeeper
Meni Orenbach, Bar Raveh, Alon Berkenstadt, Yan Michalevsky, Shachar, Itzhaky, Mark Silberstein

TL;DR
GateKeeper is a framework that leverages formal models and testing to automatically generate runtime validators and vulnerability checkers, enhancing security for applications in TEEs against untrusted external services.
Contribution
It introduces a novel approach to model untrusted services using testing suites, enabling automatic generation of security validators and vulnerability checkers without requiring formal methods expertise.
Findings
Successfully protected Memcached and SQLite with negligible overheads.
Generated vulnerability checker detected novel vulnerabilities.
Developed comprehensive models of POSIX file system and OS primitives.
Abstract
Applications running in Trusted Execution Environments (TEEs) commonly use untrusted external services such as host File System. Adversaries may maliciously alter the normal service behavior to trigger subtle application bugs that would have never occurred under correct service operation, causing data leaks and integrity violations. Unfortunately, existing manual protections are incomplete and ad-hoc, whereas formally-verified ones require special expertise. We introduce GateKeeper, a framework to develop mitigations and vulnerability checkers for such attacks by leveraging lightweight formal models of untrusted services. With the attack seen as a violation of a services' functional correctness, GateKeeper takes a novel approach to develop a comprehensive model of a service without requiring formal methods expertise. We harness available testing suites routinely used in service…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Cloud Data Security Solutions · Distributed systems and fault tolerance
