fold/docs/internal/interprocedural-buffer-threading.md

Interprocedural Buffer-Bound Threading — Research & Implementation Plan

Date: 2026-05-30 | Status: Research complete, implementation pending

Problem

fold misses the decode_base64 buffer overflow because the call chain is: main → validate_auth → decode_base64(basic_auth, decoded[0x100])

The array decoded[0x100] is local to validate_auth. Its 256-byte size must propagate to the output parameter inside decode_base64 for the OOB observer to catch output[output_index++] exceeding 256.

Root Cause (confirmed)

The walker processes functions in declaration order. decode_base64 is defined BEFORE validate_auth, so it's walked first with an empty param_buffer_sizes_ map. Then validate_auth walks, seedParamBufferSizes records param 1 → 256, but it's too late — decode_base64 was already processed.

Declaration order:  decode_base64 → validate_auth → main
Walk order:          decode_base64 (no buffer sizes yet)
                     validate_auth  (seeds param_buffer_sizes_)
                     main           (calls validate_auth)

Research Synthesis

Industry approaches

Tool	Technique	Key insight
Infer/Inferbo	Compositional summaries with symbolic intervals	Summary = {param → interval, ret → (offset, size)}. "Writers only provide intraprocedural analysis; Infer makes it compositional."
FunFrog	Interpolation-based function summarization	Uses Craig interpolation to create over-approximate summaries for BMC
ARCHER	Path-sensitive, interprocedural symbolic analysis	Bounds both variables and memory sizes symbolically across calls
SVF	Value-flow graph with shortcut edges	Summarizes interprocedural value flows with linear complexity

Inferbo's summary format (relevant pattern)

For `char* malloc_wrapper(int n)`:
  summary = { n |-> [s$6, s$7], ret |-> (offset: [0,0], size: [s$6, s$7]) }

This binds the parameter n to the return value's buffer size. In fold's terms: decode_base64 summary would have param_pre[1].kind = "bounds", expr = "arg1_size <= 256".

fold's existing infrastructure

Component	File	What it does
CalleeProperties	cross_tu_cache.hpp:16	Tracks bounds_params per function
param_pre	summary.hpp:18	Per-parameter preconditions (nonnull, nonzero, bounds)
seedParamBufferSizes	oob_access.cpp:1315	Records buffer sizes from call-site array types
param_buffer_sizes_	oob_access.cpp:1358	Per-instance map, keyed on (FunctionDecl*, param_idx)
primeOOBAccessCrossTUCache	oob_access.cpp:1352	Pre-pass that records callee properties
SummaryStore	summary_store.cpp	Shared across TUs, keyed on qualified name

Fix: Pre-Pass Architecture (M effort, ~150 lines)

Step 1: Add a buffer-size pre-pass to the security walker

Before any function is walked, scan all call sites in all function bodies in the TU. For each call like f(decoded) where decoded is ConstantArrayType with known size, record f, param_i → size in a shared (not per-function-walk) map.

Step 2: Add to OOBObserver initialization

Pass the pre-computed buffer size map to the constructor. The OOB observer reads from it instead of (or in addition to) the seedParamBufferSizes runtime seeding.

Step 3: Propagate through summaries

When computing a summary for validate_auth, if it calls decode_base64(basic_auth, decoded) where decoded has known size 256, and decode_base64's summary has a bounds precondition on param 1, then validate_auth's summary should ALSO carry a derived bounds constraint: decoded_size ≥ 256 (already known) → decode_base64_output_bound ≤ 256.

Implementation priority

1. Pre-pass (S, highest ROI): Scan all call sites before walking any function. Populate a shared param_buffer_sizes_ accessible to all per-function OOB observers. This alone would catch decode_base64 because the seed happens before decode_base64 is walked.

2. Summary threading (M): When computing a summary, propagate buffer bounds from callee summaries into the caller's summary as derived constraints.

3. Transitive propagation (M-L): Full interprocedural (cross-TU) buffer size summaries — needed for real-world codebases where callers and callees are in different TUs.

References

• Calcagno et al., "Moving Fast with Software Verification" (NFM 2015) — Infer's compositional analysis design
• "Inferbo: Infer-based buffer overrun analyzer" (Facebook Research, 2017) — interval-based buffer size summaries
• Sery et al., "FunFrog: Bounded Model Checking with Interpolation-Based Function Summarization" (HVC 2012)
• Xie & Aiken, "ARCHER: using symbolic, path-sensitive analysis to detect memory access errors" (ESEC/FSE 2005)
• Biere et al., "Bounded Model Checking" (Advances in Computers, 2003)
• fold's summary infrastructure: src/symbolic/summary_encoder.cpp, include/fold/symbolic/summary.hpp