Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433

Classification

• Type: bounded research / analyzer soundness-infrastructure spike
• Priority: P2 / backlog; not a production-engine rewrite or new diagnostic by default
• Area: existing ownership abstract states and transfers → CFG/fixpoint/merge behavior → result completeness/evidence
• Prior art: NASA-SW-VnV/ikos (NASA IKOS: abstract-interpretation infrastructure and LLVM-based C/C++ analyzer)
• Related, not superseded: Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic source-program mutation harness), Research: COVA-inspired targeted path-condition oracle for ownership soundness (bounded spike) #431 (COVA-inspired path-feasibility oracle), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (Roslyn→OwnIR/ICFG fidelity), Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (opaque call effects), 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), Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (alias precision)

Motivation

S5 ended at STOP-SOUNDNESS, and the evaluated real-project cases did not show meaningful product advantage over C01. More sophisticated warnings are not useful if an internal transfer, join, loop approximation, or incomplete-input path silently loses a feasible ownership state and then reports safety.

IKOS is interesting not as a ready-to-use .NET ownership analyzer, but for several inspectable engineering patterns:

1. Abstract-state semantics separated from checkers. Domain operators and fixpoint machinery need explicit, independently testable contracts.
2. Soundness checker (-a=sound) flags operations that may invalidate the analyzer's assumptions rather than treating every completed scan as a proof.
3. Widening/narrowing and partitioning make the precision-vs-cost tradeoff explicit; maintaining separate outcomes can avoid premature information loss.
4. Result taxonomy: IKOS distinguishes safe/error/unreachable/warning, with warning also covering insufficient information. Its classifications do not magically establish soundness outside stated assumptions.

Relevant IKOS documentation:

• Root README: architecture, result statuses, licensing
• Analyzer docs: soundness checker and numerical domains
• Fixpoint parameters
• Partitioning
• Analysis assumptions

Default decision: do not port IKOS, LLVM IR, numerical domains, APRON, or its engine; Own.NET already has ownership state, CFG/worklist/fixpoint facilities. The first task is to audit whether existing mechanisms preserve their intended semantics.

Research question

Can a small, independent concrete-state oracle and algebraic property tests expose a verified unsoundness defect in Own.NET's abstract-state operations or prevent misleading SAFE/absence claims under incomplete analysis, without building another analyzer?

Keep these distinct:

• Unsoundness: a concretely reachable state/bug is excluded by the abstract result, or an incomplete analysis is treated as complete.
• Imprecision: the abstract result contains extra (possibly infeasible) states; this can cause warnings, but is not itself unsound.
• Oracle limitation: the tiny reference semantics cannot model the relevant C# construct. Report UNMODELED, not PASS.

Bounded work plan

0. Inventory before implementing

• Pin Own.NET revision, engine/mode, concrete implementations of state transfer, join/merge, loop processing, call summaries, escape/alias/Dispose semantics, and status/evidence emission.
• Explicitly inventory whether widening/narrowing or state partitioning actually exist in Own.NET. If absent, do not claim to test them and do not introduce them as prerequisites.
• Write down an initial concretization relation between a deliberately tiny resource-state model and the corresponding Own.NET abstract facts. Identify the assumptions and constructs excluded from that relation.
• Reuse existing fixtures and harnesses from Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405/Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 where possible; no parallel generic testing framework.

1. Independent tiny-state oracle (test-only)

Define a small, reviewable reference machine (separate from production analysis helpers) with finitely many resource identities and path states. Begin with:

• acquire/new obligation; use; release/Dispose; double release/use-after-release;
• alias vs distinct resource identity; transfer/consume vs borrow;
• conditional branch, early return, and cleanup on normal vs exceptional exit where the pinned lowering faithfully exposes it;
• opaque call / unmodeled effect and an explicitly exhausted analysis budget.

For small loop-free or deliberately bounded programs, enumerate concrete successor states and compare with the abstract output at selected program points:

• Every modeled reachable concrete successor must be represented by (i.e., belong to the concretization of) the abstract state.
• Transfer: abstraction of concrete post-states is covered by abstract transfer of the pre-state.
• Join: each input's concretization is included in the joined state's concretization; join should be monotone/idempotent where the selected domain promises that law.
• Bottom/top and ordering properties are tested only when the implementation exposes corresponding semantics.
• For loops, a bounded explorer is not a proof about unbounded executions; test only sound local invariants of any actual approximation/widening operator, or mark loops out of scope.

Crucially, the oracle must not call Own.NET's transfer/join functions to compute the expected result. Hand-review its semantics against source-level C# behavior. Enumerating bounded executions can find counterexamples but cannot establish global analyzer soundness.

2. Adversarial soundness and completion cases

Include a small matrix of reviewed positive and negative tests:

• branch merge with cleanup on one path only;
• guarded Dispose plus early return or thrown exception;
• two aliases to one resource vs two distinct resource instances;
• consuming callee vs borrowed callee; unknown/virtual/unresolved target;
• missing/unsupported OwnIR fact or call effect, partial CFG/call frontier, interrupted/budget-exceeded analysis;
• path partitioning by return value only if an existing mechanism can represent it.

Safety invariant: an UNKNOWN, unsupported effect, skipped path, incomplete CFG, timeout, or budget cutoff must not silently become a proven SAFE or a complete absence claim. Evaluate this against existing result semantics: do not redefine all clean diagnostics as a global proof obligation without first documenting current contracts.

Capture first divergence (concrete states → lowered facts → transfer/join/fixpoint → checker/result), not just a mismatch count.

3. Mutation-test the analyzer operations (distinct from #405)

If feasible, deliberately inject a few test-only broken variants:

• join drops an incoming path;
• release is applied to the wrong alias/identity;
• unknown effect is treated as no-op;
• exceptional/early-return edge is discarded;
• actual loop approximation fails to over-approximate.

The oracle/property suite should fail on each applicable, valid mutant. Record mutants not generated or not applicable. This is operator-level fault injection, not #405's mutations to user C# source.

4. Optional partitioning micro-comparison, only after an observed gap

On 2–4 reviewed cases, compare current state merging with a test-only limited partition keyed by a return outcome or relevant guard, if current abstractions can support it cheaply. Record changed classifications, any lost states, time/memory growth, and whether this genuinely fixes an adjudicated problem.

Do not generalize from a synthetic precision win to real-project utility; no default production partitioning.

Deliverables / acceptance criteria

• Pinned IKOS source/documentation note, explicitly separating transferable patterns from LLVM/C++-specific implementation and assumptions.
• Inventory of actual Own.NET domain operators, convergence behavior, completeness contract and gaps; no invented widening/partitioning capabilities.
• Independently reviewed, minimal concrete semantics and small deterministic oracle corpus, with assumptions documented.
• Per-case trace showing concrete reachable states vs abstract coverage; PASS / UNSOUND-COUNTEREXAMPLE / INCOMPLETE / UNMODELED / INFRA-ERROR kept distinct.
• At least 3 applicable injected operator faults demonstrably caught, or an explicit explanation of why such injection is not viable; do not inflate a score with inapplicable mutants.
• At least one adversarial case verifying that unsupported/unknown/incomplete work is not represented as a proven safe result.
• Reproduction instructions, pinned revision/commands, tiny fixtures, machine-readable results and a short human audit report.
• End with CONFIRMED UNSOUNDNESS → narrow fix issue, RESEARCH-ONLY (useful checks but no new bug), or STOP (overlap, inadequate oracle, or unjustified cost). No broad soundness claim based on finite tests.

Stop and safety gates

Stop after the bounded corpus and a handful of operator mutations. Do not add a new solver, numerical domain, global abstract interpreter, always-on CI mutation stage, or rewrite of diagnostics in this ticket.

Any proposed production SAFE upgrade or warning suppression must be reviewed in its own issue, with a documented semantic model and adversarial tests. A bounded reference oracle is evidence about its modeled subset only. IKOS itself has stated analysis assumptions; importing its vocabulary without equivalent contracts would recreate the same soundness problem.

IKOS uses the NASA Open Source Agreement 1.3 (NOSA): study ideas/docs initially, do not copy code without a separate license review.