面向LLVM的类型驱动、构造安全的飞地分区

中文摘要 AI 辅助

可信执行环境（TEE）通过飞地提供硬件支持的隔离，可独立于软件抽象保护代码与数据，但仅靠TEE无法实施信息流安全。这一问题在类似LLVM的低级语言中更为严重，这类语言允许无限制的指针操作和非结构化控制流。此外，有效使用TEE通常需要手动将应用划分为飞地和非飞地组件，该过程劳动密集、易出错且缺乏细粒度控制。我们通过三步方法解决这些挑战：首先，我们形式化SIR，一种基于LLVM IR的飞地无关演算，配备新型宽松类型系统，可抵御低级攻击者的安全；为获得有意义的保证，SIR将信息流控制与感知安全的粗粒度内存安全相结合。其次，我们将SIR扩展为SIREN，一种飞地感知演算，可抵御能观察任意非飞地内存的更强攻击者的非干扰。第三，我们开发从SIR到SIREN的类型驱动、类型保留编译，可自动生成安全的飞地感知程序，消除手动分区，同时为主机-飞地边界提供细粒度控制。我们在13个微基准和实际工作负载（包括SGXGauge中的应用）上实现并评估SPLITR，在Intel SGX硬件上进行测试。SPLITR可扩展至OpenSSL（425953条LLVM IR指令），支持多个目标，这些目标会在飞地TCB大小、主机-飞地转换和边界数据移动之间产生权衡。对于OpenSSL，针对转换进行优化可将转换次数从393减少到187。运行时开销在短运行工作负载中主要由固定飞地成本主导，而长运行应用能更好地分摊这些成本，接近原生性能。

英文摘要

Trusted Execution Environments (TEEs) provide hardware-supported isolation through enclaves that protect code and data independently of software abstractions. However, TEEs alone cannot enforce information-flow security. This problem is further aggravated in LLVM-like low-level languages that allow unrestricted pointer manipulation and unstructured control flow. Moreover, using TEEs effectively typically requires manually partitioning applications into enclave and non-enclave components, a process that is labor-intensive, error-prone, and lacks fine-grained control. We address these challenges with a three-step approach. First, we formalize SIR, an enclave-oblivious calculus based on LLVM IR, equipped with a novel permissive type system that enforces security against low-level attackers. To obtain meaningful guarantees, SIR combines information-flow control with security-aware coarse-grained memory safety. Second, we extend SIR to SIREN, an enclave-aware calculus that enforces noninterference against stronger attackers capable of observing arbitrary non-enclave memory. Third, we develop a type-driven, type-preserving compilation from SIR to SIREN that automatically produces secure enclave-aware programs, eliminating manual partitioning while providing fine-grained control over host-enclave boundaries. We implement and evaluate SPLITR on thirteen microbenchmarks and real-world workloads, including applications from SGXGauge, on Intel SGX hardware. SPLITR scales to OpenSSL (425,953 LLVM IR instructions) and supports multiple objectives that expose trade-offs among enclave TCB size, host-enclave transitions, and boundary data movement. For OpenSSL, optimizing for transitions reduces them from 393 to 187. Runtime overhead is dominated by fixed enclave costs for short-running workloads, whereas long-running applications better amortize these costs and approach native performance.

发表机构

• University of Massachusetts Lowell（马萨诸塞大学洛厄尔分校）

机构由 AI 辅助整理，请以论文原文为准。