Paul Butcher 9693273fc5 Merge branch 'butcher-main-patch-67112' into 'main'
Update following review comments

See merge request eng/das/fuzz/research/erts_2026!1
2025-12-02 15:52:09 +00:00
2025-12-02 13:35:30 +00:00
2025-12-02 13:35:30 +00:00
2025-12-02 15:10:28 +00:00

ERTS 2026: Memory Safety Research for Embedded Real-Time Systems

Research artifacts for the 2026 Embedded Real-Time Systems Conference paper on fuzz testing effectiveness in memory-safe verification environments and AddressSanitizer limitations.

Overview

This repository contains two complementary research components:

  1. Benchmarks: A suite of memory safety vulnerability tests designed to evaluate fuzzer effectiveness when starting from Ada entry points
  2. ASan Blindspot Fuzzer: An automated tool that discovers AddressSanitizer evasion patterns across different memory regions

Together, these tools provide empirical data on:

  • The effectiveness of fuzz testing for finding vulnerabilities in mixed Ada/C codebases
  • Systematic limitations of AddressSanitizer's redzone-based approach
  • The comparative advantages of capability-based memory protection (CHERI)

Note: Replication of exact results requires access to the GNAT Pro Dynamic Analysis Suite and applicable GNAT Pro compilation toolchains from AdaCore. A partical reproduction should also be feasible by compiling and executing the benchmarks directly on the target hardware, and not using the Adaptive fuzzer.

Repository Structure

erts_2026/
├── benchmarks/              # Fuzzing benchmark suite (13 test variants)
│   ├── src/                 # Ada and C source files with deliberate vulnerabilities
│   └── README.md            # Detailed benchmark documentation
│
├── asan_blindspot_fuzzer/   # Automated ASan evasion discovery tool
│   ├── asan_evasion_fuzzer.c    # Main fuzzer implementation
│   ├── example_results/     # Pre-generated evasion examples (18 patterns)
│   └── README.md            # Complete fuzzer documentation
│
└── mutation_stats_util/     # Ada utility for tracking fuzzing statistics
    └── (Not configured for this study)

Component 1: Benchmarks

Purpose: Evaluate whether fuzzers can discover memory safety vulnerabilities when fuzzing Ada interfaces that call into unsafe C code. The tests performed utilise the AdaCore GNATfuzz Adaptive fuzzing engine.

Key Features

  • 13 Test Variants across 7 vulnerability categories
  • Mixed Ada/C Architecture: Ada entry points with C vulnerability implementations
  • Complexity Spectrum: From simple off-by-one errors to complex multi-condition bugs
  • Sanitizer Compatibility: Designed to test with ASAN, MSAN, UBSan

Vulnerability Categories

Category Variants Example Test
Stack buffer overflow 3 simple_stack_overflow(), process_user_config()
Heap buffer overflow 2 simple_heap_buffer_overflow(), write_cache_entry()
Double free 2 cleanup_resource_handle(), Double_Free_Fuzz()
Use after free 2 handle_session_data(), Use_After_Free_Fuzz()
Array in struct 2 simple_struct_array_access(), Record_Array_Access()
Out of bounds pointer arithmetic 1 test_out_of_bounds_arithmetic()
ASan overflow evading 1 test_asan_evade()

Quick Start

For a detailed explanation of how to use the GNATfuzz Adaptive engine see: https://docs.adacore.com/live/wave/gnatdas/html/gnatdas_ug/gnatfuzz/gnatfuzz_part.html#gnatfuzz-adaptive-on-target-fuzzing-experimental

cd benchmarks

# Example:

# *** Step 1 *** Set up the build environment and configure the fuzzer

# tell GNATfuzz to generate code for Adaptive fuzzing
export GNATFUZZ_ADAPTIVE=1

# ensures the GNATfuzz runtime is built the specified target
export GNATFUZZ_RT_Externally_Built=false

# configure the Adaptive engine fuzzer
export GNATFUZZ_ADAPTIVE_ENGINE_COVERAGE=1
export GNATFUZZ_ADAPTIVE_ENGINE_TIMEOUT=1
export GNATFUZZ_ADAPTIVE_ENGINE_MAX_CRASH=1
export GNATFUZZ_ADAPTIVE_ENGINE_SEED=1

# *** Step 2 ***  Generate the Adaptive engine fuzz harness
gnatfuzz analyze -P benchmarks.gpr

# where <id> should be selected from the generated obj/gnatfuzz/analyze.json
gnatfuzz generate -P benchmarks.gpr --analysis=obj/gnatfuzz/analyze.json --subprogram-id=<id> -o generated_harness


# *** Step 3 *** Instrument the source code for coverage guidance grey box fuzzing 

# For CHERI fuzzing on Arm Morello, CheriBSD set <target> to "morello-freebsd,15", for x86 Linux host fuzzing drop the --target switch
gnatcov instrument -P generated_harness/fuzz_testing/fuzz_test/adaptive_engine.gpr --level=stmt --target=<target>

# *** Step 4 *** Build the Adaptive engine
# For CHERI fuzzing on Arm Morello, CheriBSD set <target> to "morello-freebsd,15", for x86 Linux host fuzzing drop the --target switch
# To include Address Sanitizer instrumentation add -fsanitize=address
gprbuild --target=<target> -P generated_harness/fuzz_testing/fuzz_test/adaptive_engine.gpr -j$(nproc --all) --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts.gpr

# *** Step 5 *** Execute the Adaptive engine fuzzing campaign
# The resulting artifacts will be located under ./obj/gnatfuzz/harness/fuzz_testing/build/gnatfuzz-test_harness.adaptive. For fuzzing on CHERI, send the executable to a physical Arm Morello running CheriBSD.
./gnatfuzz-test_harness.adaptive

Full Benchmarks Documentation

Component 2: ASan Blindspot Fuzzer

Purpose: Automatically discover buffer overflow patterns that evade AddressSanitizer detection but would be caught by capability-based memory protection.

Key Features

  • Automated Discovery: Generates, compiles, and tests thousands of overflow scenarios
  • Cross-Memory Coverage: Tests heap, stack, global variables, and struct padding
  • Verification Built-in: Confirms both corruption AND ASan evasion
  • Ready-to-Use Examples: Pre-generated evasion tests included

Research Findings

The fuzzer discovered 18 distinct ASan evasion patterns:

Memory Type Evasions Found Redzone Size Detection Advantage
Heap (malloc) 5 ~32 bytes CHERI would catch
Global/Static 5 64 bytes (fixed) CHERI would catch
Stack locals 3 16 bytes CHERI would catch
Struct padding 5 N/A (intra-object) Both miss (needs sub-object bounds)

Key Insight: ASan's redzone architecture has predictable blind spots that can be systematically exploited. Overflows of specific sizes (16, 32, 64 bytes) reliably jump redzones across all memory regions.

Quick Start

cd asan_blindspot_fuzzer

# Run the fuzzer (takes a few minutes depending on the hardware architecture)
gcc -Wall -Wextra asan_evasion_fuzzer.c -o asan_evasion_fuzzer
./asan_evasion_fuzzer

# Test a discovered evasion
gcc -fsanitize=address results/asan_evasion_heap_buf1_ovf31_into_buf2.c -o test
./test
echo $?  # Returns 42 = successful evasion (corruption without ASan detection)

Full ASan Fuzzer Documentation

Research Methodology

Benchmarks Study Design

  1. Define vulnerability patterns across common memory safety bug classes
  2. Implement as Ada entry points calling C vulnerable code
  3. Apply and evaluate a novel lightweight cross-target fuzzing solution (GNATfuzz Adaptive Engine)
  4. Measure discovery rates across different sanitizer configurations
  5. Analyze results for fuzzer effectiveness and sanitizer coverage

ASan Limitation Study Design

  1. Systematically generate overflow scenarios with varying sizes and layouts
  2. Compile with ASan and execute each test
  3. Detect successful evasions: corruption occurs but ASan doesn't trigger
  4. Classify patterns by memory region and overflow distance
  5. Document implications for security tool selection

Research Context

This work supports the following research questions:

  1. RQ1: Can fuzzers effectively discover vulnerabilities in memory-safe languages that interface with unsafe code?
  2. RQ2: What types of vulnerabilities are most/least discoverable via fuzzing?
  3. RQ3: What are the systematic limitations of AddressSanitizer?
  4. RQ4: How do different memory protection approaches compare (ASan vs CHERI)?

Requirements

For Benchmarks

  • Ada Compiler: GNAT (FSF or AdaCore)
  • C Compiler: GCC or Clang with sanitizer support
  • Optional: GNATfuzz Adaptive engine from the GNAT Pro Dynamic Analysis Suite

For ASan Fuzzer

  • C Compiler: GCC or Clang with -fsanitize=address support

Citation

If you use these research artifacts in your work, please cite:

[Paper details to be added upon publication]
2026 Embedded Real-Time Systems Conference

License

Copyright (C) 2025, AdaCore
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception

Contact

For questions about these research artifacts, please contact the authors through the conference submission system or AdaCore's research team.

Description
No description provided
Readme 69 KiB
Languages
C 89.2%
Ada 10.8%