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

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

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.