PaperlayerView exact revision on arXiv

Source-linked AI summary

Type-Directed, Secure-by-Construction Enclave Partitioning for LLVM

Wesley B. Nuzzo, Samuel Dodson, Benjamin Houle, Tarakaram Gollamudi, Anitha Gollamudi

arXiv:2609.02048v1cs.CRcs.PL

TL;DR

The paper addresses secure enclave partitioning for low-level LLVM programs, where TEEs alone do not provide information-flow security and manual partitioning is difficult. It develops SIR and SIREN with a type-preserving compilation between them, then evaluates SPLITR’s configurable partitioning trade-offs, including a reduction in OpenSSL transitions from 393 to 187.

  • Problem

    LLVM’s unstructured control flow and arbitrary pointer manipulation complicate information-flow security, while manual enclave partitioning is costly and error-prone.

  • Method

    The paper formalizes SIR and SIREN and compiles SIR programs into type-preserving, enclave-aware SIREN programs using configurable partitioning objectives.

  • Results

    SPLITR produces distinct partitions exposing trade-offs among enclave size, host–enclave transitions, and boundary data movement; OpenSSL transitions decrease from 393 to 187 when optimized for transitions.

  • Takeaways & Limitations

    Type-driven compilation enables secure, flexible enclave partitioning for LLVM programs while supporting systematic exploration of security–performance trade-offs.

  • Takeaways & Limitations

    The translation is not formally shown to preserve semantics, and SPLITR leaves coarse-grained memory safety enforcement to future work.

Abstract

from arXiv · show

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.

1 Introduction

The paper targets secure, flexible enclave partitioning for LLVM, whose low-level features complicate information-flow control and memory safety. It introduces formal calculi, type-preserving compilation, and optimization-based partitioning to address these challenges.

  • Motivation: LLVM’s unstructured control flow and arbitrary pointer arithmetic complicate security enforcement and motivate targeting LLVM IR directly.The goal is automatic placement of sensitive code and data inside enclaves with formal guarantees.
  • Motivation: TEEs isolate code and data from privileged attackers but cannot prevent vulnerable applications from leaking their own secrets.Whole-application enclave placement therefore does not guarantee confidentiality.
  • Challenges: Standard IFC can over-taint LLVM programs, while memory errors such as buffer overflows can expose secrets through public pointers.Meaningful security requires both permissive implicit-flow tracking and protection against memory violations across security boundaries.
  • Challenges: Manual enclave partitioning is costly and error-prone, and prior automated approaches do not target LLVM-like languages with formal security guarantees.TEE constraints and host–enclave transitions also create practical partitioning challenges.
  • Approach: SIR, SIREN, and type-preserving compilation provide formal security against progressively stronger low-level attackers while automating enclave-aware partitioning.SIR combines information-flow policies with security-aware coarse-grained memory safety; SIREN models enclave isolation.
  • Evaluation: SPLITR evaluates thirteen applications and exposes trade-offs among enclave size, host–enclave transitions, and boundary data movement through multiple objectives.Constraint-generation optimizations mitigate the cost of solving the partitioning problem.

2 Overview

The overview presents SIR’s low-level security mechanisms, SIREN’s enclave isolation model, and type-driven partitioning with configurable objectives. Evaluation shows that these objectives produce concrete trade-offs in enclave size and transition counts.

  • SIR: SIR represents LLVM instructions and security policies while supporting declassification, security-aware memory safety, and low-level pointer arithmetic.Its memory model partitions stack and heap locations into security-indexed regions.
  • SIR: SIR’s gep aborts when pointer arithmetic crosses security boundaries, preventing a known route for exposing secrets through public pointers.Arithmetic may still overflow within a single security region.
  • SIR: SIR tracks branch-induced taints and safely removes them at postdominator-indexed control-flow points, reducing over-tainting.The approach avoids complex continuations and abstract-interpretation-based influence regions.
  • Security Guarantees: SIR guarantees noninterference without declassification and gradual release when information is explicitly declassified.Gradual release is more permissive than noninterference and makes the HOTP example secure.
  • SIREN: SIREN models enclave memory and transitions, enforcing that enclave memory is accessible only to code executing within the same enclave.Its type system guarantees noninterference against an attacker observing all host memory.
  • Partitioning: SPLITR uses type-driven compilation and four objectives to trade off transitions, enclave code size, their combination, and boundary data movement.For HOTP, minTCB yields 635 enclave instructions and 53 transitions, whereas minimizing transitions yields 733 instructions and 1 transition.
  • Evaluation: For OpenSSL, minimizing transitions reduces their number from 393 to 187, while some benchmarks show little optimization freedom.OpenSSL contains 425,953 LLVM IR instructions.

3 SIR: The Source Language

SIR is an LLVM-based source calculus that combines security-labeled typing, permissive control-flow tracking, and coarse-grained memory isolation to protect low-level programs. Its semantics and theorems address pointer-based leakage, implicit flows, and controlled declassification.

  • SIR language and memory model: SIR associates explicit security labels with data types and partitions memory into security-level regions.Its LLVM-like model includes functions, blocks, arithmetic, gep, loads, stores, branches, calls, returns, and phi instructions.
  • Security-aware memory safety: SIR prevents cross-security pointer aliasing by allocating objects according to security levels and restricting pointer-valued loads to their source region.These invariants address pointer/integer confusion that can otherwise launder secrets through apparently public pointers.
  • Security-aware memory safety: The gep semantics abort when pointer arithmetic crosses security-region boundaries, while loads and stores restrict dereferences to the same region.This coarse-grained protection does not prevent buffer overflows within a single security region.
  • Permissive control-flow typing: Block-indexed program-counter labels let control-flow taint be discharged at immediate postdominators, making implicit-flow tracking more permissive.The mechanism refines the standard flows-to relation and avoids rejecting some public effects after secret-dependent branches.
  • Security guarantees: Well-typed SIR programs without declassification satisfy noninterference against a bottom-level attacker, while programs with declassification satisfy gradual release.Gradual release permits controlled information release according to declassification policies.

4 SIREN: SIR + ENclaves

SIREN extends SIR with enclave-aware memory, control-flow, and transition abstractions that model TEE isolation and support security against stronger attackers.

  • Enclave abstractions: SIREN adds seven enclave-specific instructions, including preserve and ocall, to model enclave management and host–enclave transitions.preserve and ocall capture transition requirements not modeled in prior work.
  • Enclave abstractions: Execution modes distinguish host mode from specific enclaves, with transitions occurring only through eenter, eexit, ocall, and oret.ecreate initializes an enclave and ekill terminates it.
  • Well-formedness: SIREN requires single-entry, single-exit enclave regions and variable dominance so enclave-local values cross boundaries only through explicit preserve operations.Variable dominance propagates preserved values to enclave entries for uses after exit.
  • Memory isolation: SIREN restricts memory access so enclave locations are accessible only from the same enclave, while host memory remains accessible from enclave code.The load premise permits a pointer’s mode to be either host mode or the current enclave mode.
  • Security guarantees: SIREN’s type system guarantees noninterference against both ⊥-attackers and e-attackers for non-declassifying, well-typed programs under a well-formed specification.The e-attacker can observe arbitrary host memory, making it stronger than the language-level attacker.

5 Translation

The translation compiles well-typed SIR programs into well-typed SIREN programs by solving mode constraints and inserting structured host–enclave transitions.

  • Constraint generation: A well-typed SIR program is translated into a mode-annotated SIREN− program that generates constraints for enclave placement.The constraints assign modes to pointers, blocks, instructions, and functions.
  • Transition insertion: The second phase inserts eenter and eexit instructions after splitting blocks by execution mode, then rewrites control flow with preserve operations for well-structured boundaries.A shared mode-exit block provides a consistent host continuation after enclave execution.
  • Constraint generation: Secret-context instructions and accesses to private pointers are constrained to execute inside an enclave, while pointer and function modes must remain consistent.Calls either remain standard calls within one mode or become ocalls from enclave to host.
  • Constraint generation: Conditional-branch constraints conservatively require source and successor blocks to share a mode, preventing undesirable multiple enclave entry points.Memory-access rules likewise require pointer modes to match instruction execution modes.
  • Correctness: The translation is type preserving: translating a well-typed SIR configuration yields a well-typed SIREN configuration and therefore inherits the stated security guarantees.Formal semantic preservation is not established; evaluation supplies empirical evidence instead.

6 Implementation

Inferno infers security policies from sparse annotations, while SPLITR type-preservingly partitions annotated LLVM IR into host and enclave components. The implementation supports multiple placement objectives and handles enclave boundaries under SGX constraints, with limitations for outlining, marshalling, and unsupported memory-safety enforcement.

  • Inferno: Inferno propagates a small set of seed annotations according to SIR typing rules to infer a complete security policy.Developers mark where secrets enter the program rather than manually annotating every instruction.
  • Inferno: OpenSSL’s approximately 400k instructions are annotated in under 10 minutes, with at most one manual annotation per distinct confidentiality level.Many benchmarks require only a single annotation specifying the initial security context.
  • SPLITR: SPLITR partitions annotated LLVM IR into OpenEnclave host and enclave components using per-instruction placement constraints and max-flow min-cut.The solver models instructions as nodes, with weighted edges encoding placement and transition costs.
  • SPLITR: SPLITR supports minTCB, minT, minT+TCB, and mindata objectives targeting TCB size, transitions, combined costs, and boundary data movement.These objectives provide control over distinct enclave-placement trade-offs.
  • SPLITR: SPLITR targets a single enclave and uses host pinning plus marshalled ocalls for host-only operations that cannot execute inside SGX enclaves.Flat known-size buffers are deep-copied, while nested pointers are avoided across the boundary by co-locating code with data.
  • Limitations: Unsupported outlining or boundary marshalling can force enclosing functions into the enclave, and SPLITR does not enforce coarse-grained memory safety.Unsupported LLVM instruction classes are treated permissively, while multiple-enclave partitioning remains future work.

7 Evaluation

The evaluation spans diverse workloads and shows that partitioning objectives expose trade-offs among transitions, enclave size, data movement, and runtime. Slowdowns vary widely: fixed enclave costs dominate short workloads, while objective choice and boundary constraints matter for larger or I/O-heavy applications.

  • Benchmarks and Experimental Setup: Thirteen workloads span cryptographic, data-processing, machine-learning, and systems applications, ranging from small kernels to OpenSSL’s 425,953 LLVM IR instructions.LZAV has 1,455 instructions with 89.48% labeled private, whereas OpenSSL has 425,953 instructions with 0.16% labeled private.
  • Impact of Optimization Objectives: MinT generally produces the fewest enclave–host transitions, whereas minTCB may add transitions to move more code outside the enclave.The difference is especially pronounced for larger applications with substantial public code surrounding small private cores.
  • Impact of Optimization Objectives: MinTCB generally favors smaller enclaves, minT may retain public code to avoid crossings, and minT+TCB typically lies between these extremes.Mindata instead favors placements that reduce boundary data movement.
  • Runtime: OpenSSL’s adjusted slowdown ranges from 0.88× under minT to 1.74× under mindata, while short-running workloads incur approximately 39–42× slowdown.BFS incurs approximately 2× overhead, whereas BTree, Memcached, and SVM Predict remain close to native performance.
  • Runtime: Svm_scale incurs a 120× slowdown when computation is separated from host-pinned logging, because heavy enclave–host data marshalling follows the I/O boundary.Mindata co-locates svm_scale with logging on the host, minimizing boundary data transfer and substantially reducing the slowdown.

8 Related Work

The related-work landscape covers low-level information-flow control, automatic partitioning, and secure computation, but the paper distinguishes its LLVM-focused combination of formal guarantees, enclave partitioning, and optimization trade-offs.

  • IFC for Low-level Languages: Prior low-level IFC approaches address implicit-flow tracking through mechanisms such as dynamic pc stacks, linear continuations, or abstract interpretation.The paper positions its approach around unstructured control flow and permissive tracking in low-level languages.
  • IFC for Low-level Languages: Existing systems for higher-level languages or Android and Haskell do not provide the paper’s combination of automatic low-level partitioning, formal noninterference, and enclave inference.The cited comparison includes systems lacking fine-grained IFC, automatic enclave porting, or formal guarantees for LLVM-like programs.
  • Automatic Partitioning: Privtrans and PtrSplit automate privilege partitioning, whereas this work targets noninterference against low-level attackers and fine-grained host–enclave partitioning under unsafe memory.The distinction is the security property and LLVM-level enclave setting rather than privilege separation alone.
  • Secure Computation: Viaduct uses constraint optimization to minimize cryptographic-mechanism costs, while this work uses optimization to minimize enclave-usage costs.The systems differ in both target technology and the cost optimized.
Loading 2609.02048v1…