Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425

Classification

• Type: bounded research / analyzer test-infrastructure spike
• Priority: P2 / backlog; no production implementation by default
• Area: external/opaque method effects → OwnIR/MOS and heap-effect summaries → diagnostic evidence
• External inspiration: seqra/opentaint, especially its dataflow-approximation workflow and rule-test workflow
• Related, not superseded: Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 (trusted external heap-effect summaries), P2: Extend MOS/effect summaries to protocol and barrier effects #274 (protocol/barrier effect summaries), Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (canonical first-party call facts), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation harness), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first-divergence instrumentation)

Motivation

OpenTaint's useful architectural lesson is not “port an IFDS taint engine into Own.NET.” It separates:

1. the deterministic analyzer,
2. reusable, explicit rules/models for unknown library behavior,
3. independently runnable positive/negative tests for each model,
4. escalation when a faithful model still fails because the engine cannot express or propagate the effect.

Own.NET already has MOS/effect-summary work, adversarial fixtures, and a semantic-mutation pilot (#405). But there is still an engineering question: how do we qualify a specific human- or agent-authored model of an opaque method before anyone relies on it to suppress or emit an ownership/lifetime finding?

A “model test passed” badge cannot constitute a soundness proof. In particular, trusting an over-broad harmless / no-write summary can silently hide real bugs.

Distinct scope

This issue is model-validation infrastructure and failure classification, not implementation of new summary semantics.

• Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 owns whether/how curated BCL and annotation summaries may be loaded and trusted; do not implement its table or flip H1 policy here.
• P2: Extend MOS/effect summaries to protocol and barrier effects #274 owns new protocol/barrier effect vocabulary; no new effects here.
• Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 owns missing first-party call facts; a model test must not paper over facts the frontend discarded.
• Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 owns semantic mutant generation/scoring; reuse its cases if available, but do not build another mutation generator.
• P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 owns Python/Rust first-divergence traces; reuse if useful, do not redesign tracing here.

Pilot research question

Can one small, reviewable contract-test workflow distinguish:

• valid model, correctly propagated;
• incorrect/over-broad model;
• incorrect/under-specified model;
• representation/dispatch gap (input call or identity never reaches the core);
• engine limitation (valid representable effect does not propagate);
• unknown/unresolved;
• test/oracle error;

without weakening the current fail-closed/unknown policy?

Bounded experiment

1. Inventory before coding. Identify the current summary schema/loaders and 1–2 concrete model candidates already relevant to an existing issue. Start with a simple effect that existing semantics can express. Use Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 as a motivating candidate, not evidence that arbitrary logging is harmless.
2. Pin contract and provenance. For each candidate record exact assembly/package and method signature (including overload/generics where relevant), model version, source evidence/assumptions, which receiver/argument/resource is affected, and a trust level (derived / curated-external / annotation / unknown). These are research metadata until an existing production contract supports them.
3. Write paired tests. At minimum, one positive, one negative, and one adversarial near-neighbor per modeled effect. Exercise receiver vs argument identity, aliases, indirect writes, a guarded effect, and unknown/virtual dispatch where semantically applicable. Compile all C# cases and inspect lowered facts; reject cases the frontend cannot represent rather than counting them as engine passes/fails.
4. Independent adjudication. State expected behavior from C#/.NET/library semantics before running Own.NET. Tests created by an LLM must be reviewed independently. A test proving that a model agrees with itself is not validation.
5. Run existing pipeline. Prefer a lightweight standalone fixture runner over schema/engine changes. Record baseline → explicit candidate model → observed findings and evidence, with reproducible command and pinned toolchain/commit. Unknown cases must stay unknown under the existing policy.
6. Diagnose failures at the correct boundary. Separate model mistake, parser/Roslyn lowering loss, wrong binding/dispatch, engine transfer/summary failure, bad oracle, and inconclusive. Retain a minimal repro; if a faithful model cannot pass, do not broaden it just to turn the test green.

A useful first experiment may legitimately conclude that #382 or #394 must land before the intended case is expressible. That is a documented blocker, not permission to patch those issues through this spike.

Deliverables / acceptance

• Short source-backed note on OpenTaint's actual approximation/rule-test workflow, including its limits: taint propagation is not an ownership proof; IFDS is not automatically soundness.
• Inventory mapping current Own.NET summary facilities and related issues (P2: Extend MOS/effect summaries to protocol and barrier effects #274, 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, Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405) to one feasible model-validation seam.
• 1–2 narrowly scoped model candidates with pinned provenance and an explicit unknown/trust policy, or an early NO-GO if no meaningful candidate is expressible.
• For any runnable candidate, independently reviewed compiling positive/negative/adversarial controls; expected source-level effect recorded before execution.
• Reproducible report that distinguishes model error / representational gap / engine gap / oracle invalid / unknown, with baseline and candidate diagnostics, rather than treating any green run as a proof.
• If an engine gap is found, a minimized repro and a separate follow-up issue; no silent model broadening and no hidden diagnostic suppression.
• Final GO / NO-GO based on incremental coverage or earlier detection of a model error at modest maintenance cost. If value duplicates Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394/Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 or requires a new general analysis engine, STOP.

Explicit non-goals

• No Java/Kotlin/OpenTaint engine port, new IFDS implementation, or generalized taint-analysis subsystem.
• No AI-authored summaries auto-promoted to trusted production facts.
• No new soundness claims merely because fixture tests pass.
• No automatic false-positive suppression or weakening of Unknown.
• No generic model DSL, marketplace, dependency crawler, or whole-OSS benchmark in this pilot.
• No requirement to introduce concolic execution or mutation testing; those are separate experimental techniques.

Desired outcome: a cheap, falsifiable way to determine whether reusable method-effect knowledge is actually trustworthy enough to consider for an existing Own.NET rule, while making engine limitations visible instead of hiding them inside “fixed” models.