CRII: SaTC: Enforcing Expressive Security Policies using Trusted Execution Environments

安全硬件体系结构(如Intel SGX和ARM TrustZone)的最新进展为构建在密码、信用卡等敏感数据上运行的安全关键型应用程序提供了巨大潜力。它们支持Enclave-安全内存区域，使使用敏感数据的应用程序部分能够隔离执行。Enclaves可以强制实施各种安全策略，例如在使用后始终擦除敏感数据。然而，使用Enclaves需要更多的编程专业知识，这限制了它们的广泛采用。这项工作通过自动将应用程序的安全关键部分放置在飞地内来推进构建安全系统的最先进技术，从而减少了程序员的挑战。我们将实施这一系统，以支持经常跨多个平台分布应用处理的现代应用平台，例如，在自动柜员机(ATM)上运行的应用，以及ATM连接到的云中的数据中心服务器上运行的应用。该项目包括对本科生和研究生的教育和指导。基于语言的安全机制--例如用于信息流控制的安全类型系统--可以在应用程序级别表达和执行安全要求。然而，由基于语言的安全机制强制执行的安全保证在不受语言级抽象约束的强大的低级攻击者的存在下崩溃，例如，能够注入任意代码来提取机密的攻击者。可信执行环境(TEE)--例如Intel SGX、AMD SEV、ARM TrustZone和Sanctom--为隔离执行和远程代码证明提供强大的架构保护机制。为此，它们提供了隔离的内存区域，称为Enclaves，即使在特权内核级攻击者在场的情况下也能提供机密性。我们的工作旨在使用安全的TEE飞地来实施富有表现力的安全策略。首先，我们建议为LLVM中间表示构建一个编译器，它可以自动推断Enclave区域并针对强大的攻击者实施特定于应用程序的安全。然后，推断的飞地区域将被转换为机器特定的TEE指令。我们计划支持多个后端(例如，Intel SGX和ARM TrustZone)。其次，我们建议构建DFLATE，这是一个具有分布式飞地的系统，提供关于可表达的安全规范的健壮的机密性和完整性保证。值得注意的是，DFLATE支持涉及主体组的安全策略(例如，读取机密需要Alice和Bob的许可)。我们提出了一种新的方法来使用先进的加密技术，如门限加密和环签名来实施这样的组级策略。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Recent advances in secure hardware architectures—such as the Intel SGX and ARM TrustZone—offer a great potential to build security-critical applications operating on sensitive data such as passwords, credit cards, etc. They support enclaves — secure memory regions that enable isolated execution of those parts of the applications that use the sensitive data. Enclaves can enforce a variety of security policies such as always erasing sensitive data after use. However, using enclaves requires greater programming expertise and this limits their wide-spread adoption. This effort advances the state-of-the-art for building secure systems by automatically placing the security-critical parts of an application inside enclaves, reducing the challenges for the programmer. We will implement this system to support modern application platforms that often distribute application processing across multiple platforms, for example, an application that runs on an Automatic Teller Machine (ATM) and also on data center servers in the cloud to which the ATM is connected. This project includes education and mentorship of undergraduate and graduate students. Language-based security mechanisms—such as the security type systems for information-flow control— can express and enforce security requirements at the application-level. However, the security guarantees enforced by the language-based security mechanisms break down in the presence of powerfullow-level attackers that are not bound by the language-level abstractions, for example, attackers that are capable of injecting arbitrary code to extract secrets. Trusted Execution Environments (TEEs)—such as Intel SGX, AMD SEV, ARM TrustZone, and Sanctum — offer strong architectural protection mechanisms for isolated execution and remote code attestation. To this end, they provide isolated regions of memory, referred to as enclaves, that offer confidentiality even in the presence of a privileged kernel-level attacker. Our work aims to enforce expressive security policies using secure TEE enclaves. First, we propose to build a compiler for LLVM intermediate representation that automatically infers enclave regions and enforces application-specific security against powerful attackers. The inferred enclave regions will then be translated to machine-specific TEE instructions. We plan to support multiple backends (e.g., Intel SGX and ARM TrustZone). Second, we propose to build DFLATE, a system with distributed enclaves that offers robust confidentiality and integrity guarantees with respect to an expressive security specification. Notably, DFLATE supports security policies that involves principal groups (e.g., reading a secret requires the permission of both Alice and Bob). We propose a novel approach to use advanced cryptographic techniques such as threshold encryption and ring signatures to implement such group-level policies.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.