Research: Fraunhofer CPG-inspired precision escalation and summary-aware soundness gates (bounded spike) #436

Classification

• Type: bounded research / architecture-and-correctness spike
• Priority: P2 / backlog; not a production implementation request
• Area: Roslyn → OwnIR → existing ownership/MOS analysis → method summaries → diagnostic verdict/evidence
• External prior art: Fraunhofer-AISEC/cpg (Code Property Graph, Kotlin/Java, Apache-2.0), CPG documentation
• Related, not superseded: Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (IKOS: abstract-state/transfer/fixpoint oracle), Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (OpenTaint: external-method model contract tests), 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 (external heap-effect summaries and typed write targets), P2: Extend MOS/effect summaries to protocol and barrier effects #274 (protocol effect summaries), Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (WALA: demand-driven alias precision), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (OwnIR/ICFG semantic fidelity), Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431 (path feasibility), Research: Graft-inspired derived dependency graph for ownership diagnostic explanations (bounded spike) #435 (Graft: derived evidence graph), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (evidence/completeness), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation testing), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first-divergence instrumentation).

Motivation

S5 ended at STOP-SOUNDNESS without demonstrated incremental yield over C01 on evaluated real projects. Adding a richer graph or stronger solver is not automatically progress. Fraunhofer CPG is worth inspecting for a different question: can Own.NET expose analysis precision and incompleteness as explicit, testable stages, while reusing existing OwnIR/MOS rather than building a CPG?

Relevant CPG prior art to inspect and reproduce precisely (do not assume it maps directly to resource semantics):

1. Alternative DFG construction strategies: baseline DFGPass, ControlFlowSensitiveDFGPass, and PointsToPass. Examine their tradeoffs, contracts, and how a pass advertises actual precision/completeness. In CPG the more precise passes are alternatives, not a mandatory three-pass pipeline.
2. External function DFG summaries: argument/receiver/return flows for opaque calls. Own.NET already has effects and summary work: the question is whether CPG reveals a missing boundary or invariant, not whether to invent another YAML model.
3. MAY/MUST graph traversals, call-context/field sensitivity, bounded traversal: separate a possible graph path from a realizable execution, and a found witness from an exhaustive absence proof.
4. Semantic overlays: separate original source/IR facts from interpreted resource events (Acquire, Borrow, Transfer, Escape, Release) if a minimal read-only projection actually adds value.
5. Correctness cases to inspect: CPG PR #2850 (interprocedural path traversal/recursion), CPG PR #2934 (points-to state copy-on-write and fixed-point concerns), CPG issue #2926 (unknown array indices). Treat these as candidate test ideas, not evidence of Own.NET defects.

Boundary: CPG's DFG is not a .NET ownership/disposal proof, CPG's reported C# support must be qualified against actual buildable frontend coverage, and Neo4j/CPG storage is not needed for this research.

Research question / distinct scope

Can one concrete ownership case currently classified incorrectly or opaquely be improved by budgeted, explicit precision escalation (e.g. baseline fact propagation → targeted call/alias refinement), such that:

• candidate selection and escalation criteria are observable and deterministic;
• UNKNOWN (semantics not modeled) and INCOMPLETE (analysis budget/truncation) cannot silently become PROVEN_SAFE;
• MAY-path existence does not become a claimed executable witness;
• MUST/absence claims include a completeness contract and assumptions;
• no duplicate owner for models (Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394), graph infrastructure (Research: Graft-inspired derived dependency graph for ownership diagnostic explanations (bounded spike) #435), or abstract-state soundness oracle (Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433) is created.

The spike should first inventory existing Own.NET representations and gates. If these properties are already covered, record evidence and close NO-GAP instead of proposing a second implementation.

Bounded experiment

1. Select one adjudicated real Own.NET false positive/false negative, or if unavailable one targeted, independently reviewed adversarial fixture; preserve current baseline output and first divergence.
2. Map one case through existing Roslyn/OwnIR, CFG/ICFG, resource identity, MOS/effect summaries, evidence and diagnostic verdict. Record unknown callees, alias ambiguities, truncation and chosen pass/budget.
3. Inspect the CPG implementation/docs for the five mechanisms above and document exactly which invariant (if any) Own.NET lacks. Do not base the decision on a conceptual diagram alone.
4. Prototype at most one narrow analysis-gate/provenance check or testing-only oracle on current infrastructure. Prefer tests to a new production analysis pass.
5. Adversarial cases: aliasing, using/Dispose, transfer through wrapper, unknown external call, exception edge, recursive/interprocedural traversal, joined branches, and exhausted budget. Source-level semantic mutants (Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405) and state/fixpoint checks (Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433) should challenge any claim of safety.
6. Compare baseline vs experiment on correctness (with adjudicated oracle), false-safe promotions, completeness reporting, diagnostic utility, runtime/memory and first divergence. Do not count more graph edges or warnings as a success.

Acceptance / terminal decisions

• Concrete source references (CPG modules/commits/docs) and Own.NET architecture inventory.
• One reproducible comparison with baseline, evidence/witness and status of every unknown/incomplete case.
• Clear separation of PROVEN_SAFE, WITNESSED_UNSAFE, POTENTIAL_UNSAFE, UNKNOWN, INCOMPLETE as research semantics; do not silently change public diagnostic contracts. A WITNESSED_UNSAFE label requires independently validated executability, not just reachability in a graph.
• Document at least one falsification attempt (mutation, exception path, loop/recursion, summary inconsistency, or budget cutoff).
• Record explicit relationship to Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433/Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: Graft-inspired derived dependency graph for ownership diagnostic explanations (bounded spike) #435 and avoid duplicate implementation work.
• Terminal ruling: ACCEPT-NARROW-FOLLOWUP only if demonstrated net correctness/triage value; otherwise NO-GAP, NO-BENEFIT, or STOP-SOUNDNESS with evidence.

Non-goals

No CPG/Kotlin/JVM dependency in production, no C# frontend port, no Neo4j rollout, no generic graph/query engine, no replacement of OwnIR or Rust/Python core, no wholesale points-to/IFDS rewrite, no unvalidated safe promotions and no expanded detector scope by default.

References

• https://github.com/Fraunhofer-AISEC/cpg
• https://www.codyze.io/CPG/impl/dfg-passes/
• https://www.codyze.io/CPG/specs/dfg-function-summaries/
• https://www.codyze.io/GettingStarted/graph-traversal/
• Rewrite followXUntilHit for correct interprocedural loop detection Fraunhofer-AISEC/cpg#2850
• Share PointsTo state entries between duplicated states Fraunhofer-AISEC/cpg#2934
• PtP: Handling of dynamic array indexes Fraunhofer-AISEC/cpg#2926