# 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`