Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431

Classification

• Type: bounded research / independent soundness-test oracle spike
• Priority: P2 / backlog; not a production solver or warning-suppression feature by default
• Area: C# source/Roslyn → OwnIR path and resource facts → ownership verdict/evidence → independent test adjudication
• Prior art: secure-software-engineering/COVA (Java/Android constraint analysis using Soot/VASCO/Z3; not a .NET component)
• Related, not superseded: Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation harness), Research: evaluate Tabby-style stateful path pruning for bounded ownership diagnostics #424 (Tabby stateful path pruning, explicitly not a feasibility solver), Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (method-effect contract tests), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (OwnIR/ICFG fidelity audit), Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (alias precision), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (evidence/completeness), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first-divergence tracing), Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (canonical call facts)

Motivation

S5 ended at STOP-SOUNDNESS and did not establish meaningful product advantage over C01 on the evaluated cases. Adding an ever larger path-sensitive production engine is not the default next step; we first need independently reproducible ways to challenge the existing verdicts and the conditions under which a claimed ownership violation could execute.

COVA's useful idea is selective path conditions associated with relevant values/events, rather than treating every syntactic CFG path as executable or solving the entire program. Its implementation includes:

• ConstraintAnalysis: interprocedural forward analysis of constraints;
• ConstraintFactory: predicates on branch edges, associated with tracked values;
• Abstraction: constraints + taint state, with alternative contexts joined using OR;
• ConstraintZ3 / SMTSolverZ3: formula combination and satisfiability checks.

The transfer to Own.NET is the testing strategy, not Android taint analysis, Soot/Jimple, VASCO, or a new global solver.

Safety lesson from COVA source

In the inspected version, SMTSolverZ3.isSatisfiable() returns false for Z3 UNKNOWN, and ConstraintZ3.simplify() can then rewrite the condition to FALSE. This is a possible unsound loss of a feasible path if UNKNOWN is reached; source-backed concern, not a reproduced end-to-end COVA exploit.

• SMTSolverZ3.java
• ConstraintZ3.java

Design invariant: SAT, UNSAT and UNKNOWN are distinct. Timeout, unsupported expressions, incomplete path encoding, solver error, or missing call facts must not become proof of UNSAT or of ownership safety.

Research question

Can a narrowly targeted, independent path-condition checker expose one concrete, independently adjudicated Own.NET soundness/precision error or improve the auditability of an existing finding, beyond what #405/#424/#430 already provide, at modest complexity and cost?

Distinguish three outcomes:

1. Soundness bug found: a known feasible bug path is missing, or a safe verdict depends on a wrongly excluded path.
2. Precision/evidence improvement: an existing warning relies on a demonstrably infeasible path; do not equate this with a soundness fix.
3. No incremental value / inconclusive: existing analysis already handles it, or semantic facts necessary for the solver were lost before reaching the checker.

Bounded investigation

0. Preregister and map existing infrastructure (no code yet)

• Pin Own.NET commit, active Python/Rust engine modes, Roslyn/OwnIR representation, exact commands and runtime.
• Read and cross-reference Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405, Research: evaluate Tabby-style stateful path pruning for bounded ownership diagnostics #424, Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425, Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 and Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430. Inventory whether an existing checker, fixture runner or condition abstraction can already answer the chosen question.
• Pin a COVA commit/paper and document verified implementation facts vs design ideas; its Android benchmark results do not establish .NET ownership accuracy.
• State the suspected defect/benefit and independently review expected C# behavior before looking at Own.NET output.

1. Small C# corpus (target 8–12 reviewed cases)

Prefer existing #405/#430 cases; compile and pin each fixture. Include paired positive/negative/adversarial controls covering:

• Infeasible branch conjunction: x > 0 && x <= 0 cannot both be true on the same unchanged integer value; e.g. apparent missing cleanup that would require this contradictory path.
• Feasible leak/use-after-release control: a reachable missing Dispose / wrong-instance release must not disappear merely because one neighboring path is impossible.
• Guards and early returns; conditionally executed cleanup; source-level using / try/finally and exceptional exits.
• A changed variable or alias between predicates (to catch invalid reuse of stale conditions); at least one helper call/returned condition if existing OwnIR facts permit it.
• An opaque/virtual/unresolved method and one deliberately incomplete/lost predicate.
• Integer overflow/checked semantics or another precise C# semantic boundary, where relevant.

For each case record independent source-level expected behavior, resulting OwnIR facts, the target diagnostic/path, relevant assumptions and the first semantic boundary at which a fact is unavailable. Do not use Own.NET's own findings as the oracle.

2. Optional disposable targeted oracle (only if the preregistered cases justify it)

Build a test-only, isolated checker over one selected finding/path, not all reachable program states:

• Extract only available, trustworthy branch conditions and relevant symbolic values from the pinned facts. Avoid inventing constraints for omitted operations.
• Preserve resource/receiver identity, assignment/alias invalidation and supported C# integer semantics; explicitly mark unsupported constructs.
• Use an SMT solver only if genuinely necessary; a tiny manually audited path-condition checker can be the baseline. Do not select Z3 merely to claim sophistication.
• Return a structured status: UNSAT (proven infeasible under complete, faithful encoding), SAT (satisfies the model, not necessarily executable), UNKNOWN/INCOMPLETE, with constraints, assumptions, unsupported facts, solver version, time/cost and source evidence.
• Budget queries and memory. If any critical predicate/effect was omitted, classify INCOMPLETE, even if the remaining formula is UNSAT unless that proof is independently valid despite the omission.
• Attempt replay or independent validation of a SAT witness when practical; do not advertise it as a real bug merely because an SMT model exists.

Hard prohibition: do not automatically suppress production findings, introduce new Safe decisions, or convert UNKNOWN to UNSAT. No new production schema, general symbolic executor, or solver dependency in this issue.

3. Explicit adversarial solver tests

Exercise SAT, UNSAT, UNKNOWN, forced timeout/budget exhaustion, unsupported operations, incomplete branch facts, stale-value conditions, incorrect call/alias summaries and solver exceptions. Assert that every unproven outcome preserves the existing conservative behavior and is clearly reported.

If an optional implementation cannot preserve this contract, STOP rather than making a flaky checker authoritative.

4. Compare against baseline and disposition

Report per case:

• independently adjudicated ground truth and supporting code;
• baseline Own.NET result and evidence;
• extracted predicates, checker result, assumptions and completeness;
• attributable FP/FN/unknown differences (if any), first divergence, runtime/queries/memory;
• which results depend on Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382/Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 or other upstream representation/model work;
• whether the result is an actual detector-quality change, or only improved explanation.

Do not manufacture aggregate recall/precision metrics from a tiny handpicked sample or count a plausible SMT model as an independently confirmed TP.

Acceptance / kill criteria

• Source-backed COVA note with exact version, key transferable pattern, limitations, and the UNKNOWN handling hazard.
• Clear non-overlap map to Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405/Research: evaluate Tabby-style stateful path pruning for bounded ownership diagnostics #424/Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430; use existing fixtures/infrastructure wherever possible.
• 8–12 independently reviewed C# cases or a justified early STOP after inventory if no distinguishable seam exists.
• Each case has source-level oracle, pinned commands, OwnIR/CFG evidence, and reproducible baseline.
• If a checker is built: explicit SAT / UNSAT / UNKNOWN / INCOMPLETE contract, timeouts and adversarial negative controls; no production verdict changes.
• At least one genuinely incremental confirmed gap/evidence benefit or an explicit evidence-backed NO-GO; report lost TPs and uncertainty, not just removed warnings.
• Final disposition STOP / RESEARCH ONLY / FOLLOW-UP CANDIDATE; implementation follow-up only for a confirmed, product-relevant gain with a bounded cause and regression controls.

Stop conditions

STOP if all benefit is already obtained from #405/#424/#430; conditions cannot be faithfully extracted from current OwnIR; apparent improvement requires treating solver uncertainty as infeasibility; meaningful results depend on a general concolic engine/global solver/large new IR; or runtime and maintenance costs dominate a measured gain.

Non-goals

• No COVA/Java/Soot/VASCO port.
• No Android/privacy taint analysis or generic C# symbolic execution platform.
• No automatic SMT-based filtering of production warnings or newly asserted soundness.
• No second mutation generator (Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405), alternate method-effect models (Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425), or parallel evidence/completeness system (Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426).
• No re-opening the frozen Post-cutover: summary-backed lifecycle release reachability (generalize the landed #293/#302 predicates) #304 lifecycle work through this research spike.

Desired deliverable: a short evidence-backed GO/NO-GO report and, only if justified, a follow-up with a minimal independently verified counterexample. The primary objective is to find analyzer blind spots, not to decorate warnings with equations.