Source-linked AI summary
FRESCO: Complete and Scalable Temporal Safety for CHERI Application Processors
Merve Gülmez, Nils Jordan, Jialun Zhang, Hossam ElAtali, Gang Tan, N. Asokan, Thomas Nyman
TL;DR
Prior CHERI temporal-safety designs protect heap allocations but leave stack use-after-return and scalability gaps. FRESCO colors stack capabilities by function activation and uses Color Saver plus segmented provenance namespaces to provide complete, scalable temporal safety. It prevents reported stack and heap temporal-safety exploits with approximately 4% geometric-mean SPEC CPU runtime overhead.
Problem
Prior CHERI temporal-safety schemes leave stack use-after-return unprotected and face finite provenance-ID scalability limits.
Method
FRESCO tracks stack-frame provenance by coloring the stack pointer, selectively instruments functions with Color Saver, and partitions memory into independent color segments.
Results
FRESCO systematically prevents use-after-return, use-after-free, and double-free conditions across Juliet tests and real-world CVEs, with approximately 4% geometric-mean SPEC CPU runtime overhead.
Takeaways & Limitations
Color segmentation lets stack and heap temporal-safety enforcement coexist while scaling colored capabilities beyond a single bounded namespace.
Takeaways & Limitations
FRESCO does not address intra-frame use-after-scope, and transient-execution attacks and side channels remain out of scope.
Abstract
from arXiv · showhide
CHERI provides hardware-enforced spatial memory safety. While prior work extends it with heap temporal safety, stack use-after-return remains unaddressed. Existing defenses fall short: compiler analysis reliably catches only references that escape as function return values, while dynamic sanitizers impose overheads that preclude production deployment. We present FRESCO, built on the principle that a stack capability must not outlive the frame that created it. FRESCO "colors" the stack pointer with per-invocation provenance identifiers; every capability derived from it inherits that lifetime and is hardware-invalidated the moment the function exits, regardless of how or where it escaped. Because stack frames retire orders of magnitude more frequently than heap allocations, FRESCO manages the resulting color pressure through: 1) Color Saver, a static capability-aware escape analysis that confines coloring to functions needing it, and whose core algorithm we mechanically verify in Rocq, and 2) capability-color segmentation, which partitions memory into disjoint segments, each with an independent color namespace. Color segmentation lets stack and heap temporal safety coexist on one system, making FRESCO the first hardware/software co-design to provide complete and scalable temporal safety for CHERI application processors. We realize FRESCO on the CHERI-RISC-V QEMU full-system emulator and the out-of-order CHERI-Toooba FPGA softcore, with software support in the CHERI-enabled Clang/LLVM compiler and CheriBSD OS. FRESCO systematically prevents use-after-return, use-after-free, and double-free across the NIST Juliet Test Suite and CVEs, with only a small run-time overhead in SPEC CPU (4% g.m.), SQLite, and PostgreSQL (10-14%).
1 Introduction
Prior CHERI temporal-safety extensions protect heap allocations but leave stack use-after-return unmitigated. FRESCO introduces stack coloring and scales it with Color Saver and capability-color segmentation to provide complete temporal safety for CHERI application processors.
- Motivation: Prior CHERI extensions address heap temporal safety but leave stack use-after-return unmitigated.Compiler escape analysis reliably catches only references returned from functions, while other escapes require dynamic sanitizers.
- Stack coloring: FRESCO colors the stack pointer with a per-frame provenance identifier so escaped capabilities can be retracted when the frame returns.This deterministically protects against use-after-return regardless of how references escape.
- Scalability: Color Saver confines coloring to functions needing it using capability-aware escape analysis and prevents stale capability reads from reused stack memory.The basic escape classifier is mechanically verified in Rocq.
- Scalability: Capability-color segmentation partitions provenance identifiers into independent namespaces, allowing stack and heap temporal-safety enforcement to coexist.This addresses the much higher retirement frequency of stack frames compared with heap allocations.
- Implementation and evaluation: FRESCO combines stack coloring with a color-segmented heap allocator and implements the design across CHERI-RISC-V, CHERI-Toooba, Clang/LLVM, and CheriBSD.The evaluation reports systematic prevention of use-after-return, use-after-free, and double-free conditions in Juliet tests and real-world cases.
2 Background
CHERI provides capability-based spatial memory safety, while prior temporal-safety extensions primarily target heap use-after-free and use-after-reallocation. PICASSO improves heap temporal safety with colored capabilities but remains limited by missing stack protection and a finite provenance-ID space.
- CHERI: CHERI uses hardware-supported capabilities to enforce spatial safety for C and C++ pointers.Capabilities encode permissions and are protected by validity tags that hardware-aware instructions preserve or invalidate when tampered with.
- Prior work: Cornucopia quarantines freed heap memory and performs revocation sweeps, but quarantine delays reuse and increases memory overhead.Its threshold trades mitigation completeness for performance because revoke-on-free is prohibitively expensive.
- Prior work: PICASSO uses colored capabilities to decouple provenance validity from capability validity and reduce revocation-sweep frequency for heap allocations.It caches recently accessed provenance-validity words to keep checks off the critical CPU path.
- Temporal-safety gaps: Prior CHERI temporal-safety designs mitigate heap use-after-free and use-after-reallocation vulnerabilities but do not enforce stack use-after-return safety.Stack use-after-return remains a distinct gap in application processors.
- Temporal-safety gaps: PICASSO’s 21-bit provenance identifiers provide just over two million concurrently distinguishable allocations per process, leaving a finite color-space ceiling.The remaining gaps include absent stack enforcement and bounded scalability.
3 Problem Statement
FRESCO targets complete temporal safety for heap and stack objects, scalability beyond a fixed provenance-ID ceiling, and bounded revocation cost. Its guarantees rely on trusted compiler and allocator behavior, CHERI spatial safety, and a defined adversary model, while excluding several classes of attacks and finer-grained lifetime violations.
- Goals: FRESCO’s goals are deterministic protection against heap use-after-free and stack use-after-return, without weakening guarantees across allocation classes.This closes the stack temporal-safety gap in prior CHERI designs.
- Goals: FRESCO requires simultaneously live colored objects to be bounded by available memory rather than provenance-ID bits.Long-running and allocation-heavy workloads should remain deployable without widening the capability field.
- Goals: Revocation should be infrequent, avoid dependence on one global identifier pool, and cost proportionally to live state reclaimed.The target excludes costs driven by cumulative allocation history or identifier-space fragmentation.
- System and adversary model: The model trusts the compiler to instrument stack prologues and epilogues and trusts the allocator to maintain valid bounds and reject malformed frees.The adversary can influence calls, returns, allocation, and deallocation through program defects but cannot forge capabilities or tamper with trusted components.
- Scope: Protection tracks heap provenance per allocation and stack provenance per function activation, independently of reference escape route.Intra-frame use-after-scope is not addressed because allocations within one active frame share provenance.
- Scope: Transient-execution attacks and side channels are excluded, although provenance checks occur before instruction commit.Uninitialized reads of stale capabilities are in scope, while other uninitialized allocation reads are out of scope.
4 System Design
FRESCO combines stack coloring, Color Saver, and capability-color segmentation to invalidate capabilities tied to retired stack frames while scaling provenance namespaces. Its compiler, runtime, allocator, and hardware components coordinate per-segment validity checks for stack and heap temporal safety.
- Stack Coloring: On function entry, stack coloring assigns the stack pointer a fresh color that derived capabilities inherit throughout the activation.This associates capabilities with the provenance of the frame holding their referenced allocation.
- Stack Coloring: On function return, FRESCO invalidates the frame’s color in the provenance-validity structure, causing later dereferences through escaped capabilities to trap.The mechanism retracts every dangling capability tied to the inactive frame.
- Addressing Color Churn.: Capability-color segmentation gives each disjoint virtual-memory segment its own provenance-ID namespace, preventing colors in different segments from aliasing.A segment resolver selects the appropriate per-segment provenance-validity table using the capability address.
- Addressing Color Churn.: Color Saver classifies stack allocations using capability-flow facts and removes unnecessary initialization clears while retaining stale-read prevention.The compiler architecture inserts initial clears, performs analysis after optimization, annotates IR, and then instruments selected functions.
- Color-segmented allocator: The color-segmented allocator separates heap regions by segment and uses per-segment tables and bitmaps for allocation, reclamation, and revocation.Stack and heap draw from disjoint segments, while asynchronous sweeps reclaim colors after revocation completes.
- FRESCO’s runtime architecture: FRESCO’s runtime architecture applies hardware provenance-validity checks to colored accesses and integrates stack management, heap allocation, and kernel revocation.The system is implemented for CHERI-RISC-V in QEMU and CHERI-Toooba with Clang/LLVM and CheriBSD support.
5 Color Saver Analysis
Color Saver combines capability-aware escape analysis with stale-read prevention to reduce unnecessary stack coloring while preserving temporal-safety guarantees.
- Escape analysis: The escape analysis traces capability flows backward from possible function-lifetime escapes through returns, globals, unresolved calls, copies, loads, stores, and calls.It summarizes capability-relevant LLVM instructions and propagates possible flows through both direct and memory paths.
- Escape analysis: A function is colored only when a capability pointing to its frame may escape; otherwise, coloring prologue and epilogue instrumentation can be omitted.The classifier is conservative and may color a function unnecessarily.
- Stale-read prevention: Stale-read analysis zeroes stack storage that could hold capabilities, preventing stale capabilities from being recovered after reuse.The analysis removes clears rendered redundant by the program’s own stores.
- Stale-read prevention: Selected locals include capability-carrying types or recursively capability-containing aggregates, tag-granule-sized variables, variable-length arrays, and integers cast to capabilities.Parameters and C++ reference-type variables are excluded.
- Stale-read prevention: The analysis treats unresolved memory operations conservatively by recording possible reads for every tag granule and no definite overwrite.Initial clears are inserted at variable definitions before initialization or use.
6 FRESCO Implementation
FRESCO implements stack coloring, Color Saver, segmented provenance tracking, and runtime support across CHERI hardware, compiler, and OS components. Its stack runtime switches to fresh segments when color epochs reach a threshold, while heap management assigns and revokes per-segment colors.
- Implementation platforms: FRESCO is implemented in CHERI-RISC-V QEMU and CHERI-Toooba, with compiler extensions in CHERI-enabled Clang/LLVM and runtime support in CheriBSD.The implementation includes stack coloring, Color Saver, libfresco, segment-aware MRS, allocator, and revocation.
- Capability-color segmentation: Per-segment PVTs let identical color values remain distinct across memory segments through address-based namespace selection.Configurable segment size and count are programmed through three process-level CSRs; the per-segment slice size is tied to otype width.
- Compiler integration: Color Saver runs after LLVM optimization and before instruction selection, using capability types, call attributes, and stack-object lifetime markers.The escape classifier selects functions requiring stack-coloring instrumentation, while stale-read analysis rewrites IR with validity-tag clears.
- Stack coloring instrumentation: Phase A reads the caller’s color, increments k, checks threshold K, and either recolors csp or switches to a fresh segment before frame allocation.Phase B records and later restores the caller’s color after frame allocation and callee-save spills.
- Stack segment nesting: When stack coloring exhausts a segment’s 221 encoded color values, libfresco saves execution state, installs a return trampoline, and switches to a fresh segment.Returning from the triggering function restores the previous segment; exhausted segments can be replaced without a fixed bound from nesting depth or per-segment color space.
- Heap segment management: The allocator assigns every allocation a unique color from its selected segment or a global fallback namespace, and free retracts the capability before memory reuse.MRS selects segments based on color and memory availability, while revocation reclaims colors asynchronously when reuse is unavailable or the free segment pool is low.
7 Evaluation
FRESCO is evaluated for temporal-safety coverage, color-management effectiveness, hardware cost, and application performance. It detects all evaluated Juliet violations and real-world cases while keeping overhead moderate across processor and workload evaluations.
- Security Evaluation: FRESCO detects all 1,214 vulnerable Juliet cases with zero false positives across double-free, use-after-free, and returned-stack-address tests.The evaluation covers CWE-415, CWE-416, and CWE-562 in Juliet Test Suite 1.3.
- Security Evaluation: FRESCO detects every reproduced real-world stack and heap temporal-safety violation, including a complete JavaScriptCore dangling-stack-pointer exploit chain.The cases include CVEs, GitHub issues, OSS-Fuzz reports, and the Microsoft CHERI ISA proof of concept.
- Color Saver Analysis: Color Saver reduces required segments by an order of magnitude and limits SPEC CPU2006 binary growth to 2.0% with stale-read clearing.Full coloring grows binaries by 26.5%, Color Saver by 1.4%, and the complete configuration by 2.0%.
- Performance Evaluation: FRESCO adds approximately 5% logic, 6.40% registers, and 8% memory to CHERI-Toooba, while full coloring incurs 12.9% geometric-mean cycle overhead.Excluding the limits outlier, full-coloring overhead is 7.0% geometric mean; each colored call costs 15–25 cycles.
- Performance Evaluation: FRESCO incurs approximately 4% geometric-mean runtime overhead and 18% memory overhead in SPEC, while closing the stack use-after-return gap relative to PICASSO.The SPEC runtime overhead is below Cornucopia’s approximately 11% and PICASSO’s approximately 5%.
- Performance Evaluation: FRESCO’s complete configuration incurs approximately 10% SQLite runtime overhead and degrades PostgreSQL TPS by 13.8%, while remaining below or comparable to Cornucopia across three workloads.The complete configuration’s SQLite memory overhead is approximately 90%; PostgreSQL comparisons are 13.8% for FRESCO, 6.2% for PICASSO, and 23.1% for Cornucopia.
8 Related Work
Prior CHERI temporal-safety work leaves stack use-after-return incompletely addressed or relies on costly runtime tracking. Related designs differ in restrictions, version capacity, metadata placement, and quarantine behavior.
- Prior CHERI Defenses: Prior CHERI temporal-safety designs primarily mitigate heap use-after-free or reallocation and leave stack use-after-return unaddressed.The paper identifies stack temporal safety as an effectiveness gap in prior work.
- Compiler and Dynamic Analysis: Compiler escape analysis reliably catches direct returned stack references, but indirect escapes through heap or global objects require dynamic analysis.Dynamic sanitizers track pointer propagation at runtime, but their per-store bookkeeping precludes production deployment.
- Embedded CHERI CPUs: CHERIoT restricts stack-storable capabilities so stack references cannot reach heap or global memory, but this restriction is non-conformant with C and its code compatibility is unclear.A stack pointer can still outlive its allocation through direct return or storage via a pointer to a higher frame.
- Memory Versioning: Memory-versioning schemes close reallocation gaps by matching allocation and pointer versions, but constrained tag widths require version recycling and permit collisions.Arm Memory Tagging Extension exposes 4-bit tags, or 16 versions, illustrating the capacity constraint described.
- Colored and ID-Based Capabilities: CHERI-D enables immediate heap reuse with architecturally tracked IDs, trading PICASSO’s global color ceiling for a per-slot limit of 254 reallocations before quarantine.CHERI-D stores an 8-bit ID with object data or in a per-page ID table.
9 Discussion and Future Work
FRESCO addresses memory-safety completeness and scalability by replacing fragmentation-sensitive provenance-ID management with bitmap allocation while acknowledging a use-after-scope boundary.
- Partial memory safety leaves individually exploitable residual gaps when one allocation class remains unprotected.
- FRESCO does not address intra-frame use-after-scope because per-activation coloring cannot distinguish allocations within a live frame.Per-scope coloring could address this at greater color pressure, but scope boundaries lack a runtime manifestation without compiler-generated instrumentation.
- Bitmap-based provenance ID allocation: PICASSO’s unr allocator incurs significant memory and runtime costs during bulk reclamation because fragmented IDs require structural rebuilding.Bulk freeing may require either modifying affected nodes individually or discarding and rebuilding the structure wholesale.
- Bitmap-based provenance ID allocation: FRESCO’s flat bitmap has constant footprint, avoids dynamic allocation and system calls, and supports efficient bulk bit manipulation.For a 2^21-identifier namespace, the bitmap footprint is n = 256 KiB regardless of allocation pattern, fragmentation, or revocation count.
A.2 Benchmark comparison against unr
The bitmap allocator matches unr when benchmarks do not trigger revocation and reduces both cycle and memory overhead on omnetpp, the revoking benchmark.
- The evaluation compares PICASSO with bitmap and original unr allocators on unmodified SPEC CPU2006 INT benchmarks using the train input set.
- 23% lower cycle overhead on omnetpp is achieved by the bitmap allocator relative to PICASSO’s unr allocator.The seven benchmarks without revocation perform equivalently within measurement noise.
- 1.01x memory usage for the bitmap allocator contrasts with unr’s 1.80x peak on omnetpp.The bitmap allocator maintains a constant approximately 256 KiB footprint irrespective of workload characteristics.
B Escape Analysis
FRESCO’s escape analysis tracks capability reachability through LLVM values, memory access paths, calls, and returns to identify functions whose stack frames can escape.
- The analysis represents capability-carrying LLVM values and extracts facts for copies, loads, stores, parameters, calls, returns, and retained or observed values.These facts support propagation of capability reachability through LLVM IR and interprocedural flows.
- A frame escapes when a capability pointing into it remains reachable after its activation returns through persistent memory or a returned value.The analysis performs separate Retain and Return searches from escape endpoints to frame origins.
- Access paths record memory edges crossed to reach a capability, using L for cell contents and R for values supplied to stores.Paths are words over {L, R} of length at most five, with the empty path representing the capability itself.
- Propagation relations distinguish ordinary reachability from derived reachability that may be followed backward through value definitions.Every Derived fact has a corresponding Used fact.
- Call, copy, load, and store rules propagate Used and Derived facts across arguments, returns, SSA copies, and abstract memory edges.
- The Rocq theorem establishes no false negatives for the basic algorithm on a normalized abstract machine when a returned activation retains reachable stack allocations.Under complete input facts, the rules derive UnsafeFunction for the affected function.
- Production analysis adds function summaries, shared-value propagation, and other refinements around the mechanically verified basic rules.
C Stale-Read Analysis Facts and Rules
The stale-read analysis decides which compiler-inserted clearing stores to retain by propagating possible tag observation and non-stack origins through address copies and known calls.
- A candidate is a compiler-inserted clearing store whose roots represent storage protected against stale capabilities.One candidate may have multiple roots after optimization.
- NonStackOrigin propagates through address copies to identify values originating from parameters, globals, constants, or function values.
- The analysis propagates MayObserveTag backward and forward across address copies, conservatively treating them as possible aliases.
- Known callees transmit possible tag observation from formal parameters to matching actual arguments.
- The analysis retains a clear when any candidate root may reach a tag sink or when incomplete information requires conservative retention.It also retains clears for roots not proven to be source-owned stack storage.
E Supplementary Evaluation
The supplementary evaluation reports FRESCO’s stack-coloring overhead, colored-binary code sizes, and SQLite benchmark phases, alongside gRPC latency and SQLite benchmark figures.
- 15–25 cycles is the fixed cost per colored call reported for FRESCO stack coloring on MiBench.
- Figure 10 presents gRPC QPS latency percentiles.
- Table 4 reports .text-byte code sizes for colored SPEC CPU2006 binaries.
- Figure 11 presents SQLite Speedtest1 benchmark results.
- Table 5 describes SQLite Speedtest1 phases and their overhead compared with baseline.