Research: SPDS field-stack reachability for ownership aliasing (bounded spike) #438

Classification

• Type: bounded research / field-sensitive reachability and soundness spike
• Priority: P2 / backlog; not a production SPDS port or automatic solver rollout
• Area: Roslyn → OwnIR → resource identity / field-sensitive aliases → interprocedural ownership and disposal diagnostics
• Source: CodeShield-Security/SPDS (Java, EPL-2.0; legacy Boomerang 3.0–3.1.2, explicitly unmaintained)
• Current upstream: secure-software-engineering/Boomerang (Boomerang 3.2+), SparseBoomerang (research extension)
• Related Own.NET: Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (WALA-inspired demand-driven alias precision), Research: Heros-inspired IFDS/IDE feasibility for interprocedural ownership facts (bounded spike) #434 (Heros IFDS/IDE feasibility), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (SootUp / OwnIR / ICFG semantic fidelity), Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (canonical first-party calls), Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394/Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395 (opaque effects / heap-write targets), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutants), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (completeness and evidence), Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431 (path-condition oracle), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first-divergence instrumentation)
• Default: research only; reuse cases/artifacts from Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429. No new generalized alias-analysis platform.

Motivation and distinct question

SPDS (Späth, Ali, Bodden, POPL 2019) uses a call PDS to track call/return matching and a field PDS to track field-store/load matching. Each is a separate pushdown reachability problem; their synchronization provides context-, field-, and flow-sensitive may-flow information, without fixing field-access paths to a constant depth k.

This is interesting specifically for aliases of resources stored in nested and/or recursive heap structures (including resources transferred through wrapper objects across method boundaries). Existing ownership rules need to know whether a release, use, borrow, or escape applies to the same resource. But SPDS does not provide C# lifetime semantics or prove that Dispose() has happened: it supplies underlying flow/alias information that a separate ownership/typestate model can consume.

Important precision boundary: satisfying call-stack and field-stack reachability independently does not necessarily imply that both can be satisfied on the same concrete data-flow path. Exact interleaved two-stack reachability is undecidable in general. SPDS deliberately computes a sound over-approximation, and corner cases may yield spurious may-flow. Do not report a reachable graph path as an executable ownership witness or an unreachability result as safe without complete assumptions/model.

Incremental question, distinct from #429: Does unbounded-depth field-path matching (or the SPDS field-stack idea) improve a confirmed Own.NET diagnostic over the cheapest existing field/alias abstraction after the source→OwnIR fidelity and summary/model checks? Is that benefit obtainable with a small on-demand field-path experiment rather than a full synchronized-PDS engine?

If no verified field-depth-related discrepancy survives preliminary triage, stop early; #429 remains the broad alias-precision owner.

Scope / bounded research plan

0. Pin sources and adjudicate an actual gap

• Pin exact commits/tags of the legacy SPDS, current Boomerang, optional SparseBoomerang, paper, and the tested Own.NET snapshot. Inspect actual SynchronizedPDS, WPDS, boomerangPDS, idealPDS modules instead of reasoning only from README diagrams.
• Reuse Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429's real-OSS / reviewed minimized cases and its baseline. Select at least one independently verified FP/FN plausibly caused by field-path depth or field-sensitive aliasing, not just missing local alias facts or failed call summaries.
• Trace the first divergence through Roslyn/OwnIR, receiver/argument identity, field stores/loads, arrays/containers, alias joins, ICFG calls/returns, and release/use transfer. Verify that necessary semantics exist in OwnIR. If absent, classify as lowering/representation gap (Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382/Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395) and STOP this solver experiment.
• Disqualify purely unknown external effects (Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394), incorrect test oracles, and unrelated false positives. Record both the source-level expectation and current tool output before experimentation.

1. Write down the two-stack abstraction and its limits (no code first)

• Model call PDS transitions (push call-site / pop return-site) and field PDS transitions (push/pop on field store/load) as conceptual analysis operations, not runtime C# stacks.
• Contrast: current Own.NET resource identity, k-limited access paths if applicable, access graphs / field summaries, and SPDS field-stack reachability.
• Specify a narrow query, e.g. “can release at site B may-alias the allocation/resource used at site A through next.value and wrapper calls?” Distinguish may-alias, must-alias, definitely disjoint, unknown.
• Explain the two-path false-positive case: call-valid path differs from field-valid path. Create an adversarial negative control to ensure independent reachability is not promoted to a single realizable witness.
• Detail heap abstractions, allocation sites, unknown receiver types, dynamic/virtual dispatch, recursion, ref/out, field overwrites, arrays, delegates, exception edges and incomplete calls. Mark unsupported features explicitly; no fabricated exactness.

2. Conditional micro-experiment only if the gap is real

Build one small, test-only on-demand query experiment over existing OwnIR/ICFG facts, preferring the cheapest counterfactual first:

1. Existing Own.NET baseline.
2. A bounded field-path / selective field-sensitive alternative; quantify where k loses or merges relevant resource identities.
3. Only if (2) demonstrably fails for the eligible case, prototype field-stack reachability inspired by SPDS, with existing call-context facts and explicit over-approximation. No Java/JVM runtime dependency.
4. Optional: test whether SparseBoomerang's type-aware vs alias-aware sparsification idea lowers exploration cost; do not promise its published speedups for Own.NET.

Reuse ~8–12 reviewed positive, negative, and adversarial C# fixtures, including:

• definite alias vs separate instances of the same disposable type;
• holder.child.resource, field overwrite, branch join, and aliased receiver;
• recursive Node.Next chains at increasing depth (especially beyond any proposed k);
• direct wrapper method vs two callers / mismatched return context;
• guarded Dispose, use-after-dispose, double-release and transfer/escape;
• a crossed call/field path that is accepted by both projections separately but has no jointly valid execution path;
• a deliberately missing edge/model and forced analysis budget exhaustion;
• an exceptional/virtual call case, only where faithfully lowered.

Independently adjudicate actual C# behavior; a compiler success or the prototype's verdict alone is not an oracle.

3. Correctness, budgets, and comparison

• Separate may-flow reachability, possible violation, validated witness, bounded complete negative, UNKNOWN, INCOMPLETE, and UNSUPPORTED. Do not silently change public diagnostic statuses.
• Never turn may-alias into must-alias, a failed search into PROVEN_SAFE, or crossed projections into a concrete witness. Keep existing confirmed positives under adverse budget/summary settings.
• Compare per case: source/oracle, current Own.NET output, experimental output, first divergence, changed FP/FN, explanatory value, visited states, maximum field/context depth, time and memory (if measured).
• Measure costs only on pinned inputs; include at least one real-OSS slice if an eligible gap exists. No synthetic pooled “precision” percentages from tiny curated sets.

Acceptance / stop gates

• Version-pinned primary-source note: SPDS vs current Boomerang vs SparseBoomerang, and precise sound over-approximation boundary.
• Explicit difference / overlap with Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 and Research: Heros-inspired IFDS/IDE feasibility for interprocedural ownership facts (bounded spike) #434, and a source→OwnIR feasibility audit before proposing a solver.
• One independently confirmed field-depth / field-sensitive ownership discrepancy, or documented STOP-NO-ELIGIBLE-GAP.
• Reviewed source-level positive/negative/crossed-path corpus and baseline with exact commands and artifacts if the gap exists.
• Conditional smallest-possible comparative experiment with deliberate missing-edge and truncation controls; unknown is never “safe”.
• Per-case correctness and cost comparison; clear GO / NO-GO / RESEARCH ONLY ruling.
• On GO only, create a separate narrowly scoped implementation issue with proven marginal benefit; otherwise close research with evidence.

Non-goals

No adoption of unmaintained CodeShield SPDS as a dependency, no Java/Soot/JVM integration, no port of Boomerang/IDEal/SparseBoomerang, no generic dual-PDS solver, no wholesale OwnIR / Python / Rust core rewrite, no new call graph framework, no default CI gate, no diagnostic promotion on graph reachability alone, no duplication of #429's broad alias work or #434's IFDS formulation.

Primary references

• Legacy repo: https://github.com/CodeShield-Security/SPDS
• Current Boomerang: https://github.com/secure-software-engineering/Boomerang
• SparseBoomerang (ICST 2023 research extension): https://github.com/secure-software-engineering/SparseBoomerang
• Späth, Ali, Bodden, Context-, Flow-, and Field-Sensitive Data-Flow Analysis Using Synchronized Pushdown Systems, POPL 2019: https://doi.org/10.1145/3290361 (preprint: https://johspaeth.github.io/publications/boomerangPDS.pdf)
• Independent SPDS implementation/contract: https://zju-pl.github.io/lotus/cfl/interleaved_dyck/spds.html

Decision criterion: demonstrate a real ownership correctness gain from deeper field-flow tracking, not just a more elaborate reachability engine.