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

CRII：SaTC：使用可信执行环境执行表达性安全策略

• 批准号: 2348304
• 负责人: Anitha Gollamudi
• 金额: $ 17.5万
• 依托单位: University of Massachusetts Lowell
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-04-15 至 2026-03-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2348304&HistoricalAwards=false
• 关键词: CRII; SaTC; Enforcing; Expressive; Security

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.

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