0d63dbbd7e
- SafetyObserver::seedInterproceduralContext() called before function walks - OOBObserver override scans all call sites for ConstantArrayType args - Seeds param_buffer_sizes_ from any caller, regardless of decl order - Research doc covers Inferbo/ARCHER/FunFrog approaches and fold's infrastructure
106 lines
5 KiB
Markdown
106 lines
5 KiB
Markdown
# 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`
|