A Framework for Automatic Leveraging of Trusted Execution Environments
Abstract
Trusted execution environments (TEEs), such as enclaves based on Intel s SGX hardware, offer a promising approach to improve the sec urity of computing platforms. However, leveraging such trusted enclave platforms with verifiable guarantees of security remains a ch allenging task. As each TEE exposes its capabilities via its API, only newly written applications can leverage the TEE s capabilitie s; existing applications must be manually rewritten. Worse yet, such rewriting will happen repeatedly as TEEs gain new capabilities. Not only do these repeated rewrites cost substantial developer efforts, each rewrite is yet another opportunity to introduce securi ty loopholes that will cost even more to repair later on.This proposal seeks to address this need through a program synthesis-driven approach to the design and deployment of software on TEEs. We argue that point-wise solutions (e.g., a standalone compiler) that ta rgets a specific TEE is simply non-scalable, as the rapid development of TEEs and ever-changing application security requirements wi ll quickly render such technology obsolete. Instead, we will develop a parameterizable code deployment framework called SecuriLift. Given an application to be deployed, its security specifications, and the target TEE, SecuriLift automatically extracts high-level f unctional model of the TEE, infers the semantics of the input application, and generates a hardened application that leverages the T EE while satisfying the user-provided security specification.The architecture of SecuriLift will consist of the following key compon ents:- We will develop a new program summary language called PSec to describe the semantics of input applications. Our language will nd P with security-related constructs, such as state machines to be executed on the TEE, security labels for variables, etc.- We wil l automatically extract formal models of TEEs that are built using the Keystone framework. Such models will be expressed using an ex tended Trusted Abstract Platform model. To extract PSec program summaries and TEE models, we will leverage technology developed in t he PI s group called verified lifting. Verified lifting uses a combination of formal methods and oracle-guided program synthesis tec hniques to automatically infer summaries. The technique was originally developed to infer summaries from source code and is now depl oyed at Adobe and Intel.- Once models and summaries are inferred, we will develop efficient strategies for compiling PSec programs t o leverage the target, given the provided security specification. We will use a combination of syntax and synthesis-driven technique s for this task, based on the PI s prior work on program partitioning and code generation.We will evaluate our approach on publicly available enclave platforms in collaboration with our industry partners. All tools developed will be released as open-source. The co n of trusted enclave platforms, although the chosen domain will provide a suitable focus to direct and demonstrate the research.This proposed project will develop fundamentally new techniques and tools for high-assurance software on trusted computing platforms. It will develop new ways of lifting models and code of platform implementations and legacy software, novel oracle- and syntax-guided s ynthesis methods for lifting and verification, and efficient co iques will be implemented in open-source tools applied to industrial-scale open-source TEEs. The proposed languages, synthesis metho ds, and tools will both create new fundamental science and also significantly increase the level of assurance in the security and co rrectness of trusted enclave
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 20, 2021
- Source ID
- N000142112724
Entities
People
- Alvin Cheung
Organizations
- Office of Naval Research
- United States Navy
- University of California Regents