Initial Evidence and SE Go/No-Go Validation Plan

Date: 2026-09-18

Status: Bounded feasibility demonstration completed; source-grounded commitment validation and added-value comparison remain open

Prospective execution: Disabled

Purpose

Determine whether Structural Explainability (SE), using the finite core of SE-210, can make a defensible contribution to vulnerability-matching analysis before committing to the prospective registered study.

Theory and implementation may be developed together using already-public validation cases and synthetic machinery tests. The prospective study remains unexecuted. This plan does not authorize scanner execution or approve pending execution-route assignments.

The decision concerns methodological feasibility and explanatory value, not the prevalence of defects, discovery of new vulnerabilities, or comparative scanner quality.

Initial Engineering Evidence

The following results were reported by the local repository session. They have not been independently rerun for this document.

Step 1 strengthened the case schema with execution_phase, execution_route, and direction. Validation now checks:

• Exact permitted fields recursively across case tables.
• Permitted routes: full_scanner and matcher_replay.
• Direction agreement with the primary commitment.
• Exact collection-specific execution phases.
• Known, commitment-compatible manipulated and counterpart roles.
• Identical control and variant manipulated roles.
• One-feature PURL changes verified from the actual identifiers.
• Correct transformation operation and before/after values.
• Raw qualifier order for qualifier-order transformations.

Negative tests cover unknown nested fields, invalid or incompatible roles, wrong direction or phase, multiple changed features, incorrect operations, and incorrect before/after values. Documentation now identifies the existing evidence registry and distinguishes commitment direction from control/variant ordering.

Reported verification results:

No prospective scanner execution, adjudication, reliability analysis, or research-question analysis has been started.

A bounded validation-only SE-210 demonstration has been executed using synthetic fixtures.

The listed prospective routes are Grype omitted qualifier: matcher_replay; PURL qualifier order: matcher_replay; and OCI repository location: full_scanner. Recording these assignments does not approve them or authorize execution.

This evidence supports the integrity of case declarations. It does not yet demonstrate scanner reproduction, valid SE positioning, or scientific value.

Existing Public Evidence

Use the existing validation evidence registry as the source of truth for public references, revisions, and hashes. We do not duplicate the registry here.

The initial demonstration uses:

• VAL-GRYPE-OCI-REPOSITORY-URL-001, supported by the already-public Grype issue and merged regression test, to investigate a known failure and its fix.
• The documented Trivy qualifier-applicability validation cases, to check that permitted directional matching is not falsely classified as an identity violation.

Public reports and documented expectations are existing evidence.

The bounded SE-210 analysis has been completed for the supplied candidate formalization. Independent source-grounding of the relevant Grype/VEX matching commitment remains pending.

A known scanner defect, and checker agreement on a supplied formalization, are not by themselves proof that the case is a valid source-grounded SE-210 nonconformance witness.

Boundary and Authorization

The protocol/freeze-policy.md governs permitted pre-registration work. The protocol/snapshots.md governs evidence capture. This plan adds a bounded feasibility decision; it does not replace either document.

• Use only already-public behavior and synthetic machinery controls.
• Do not run prospective cases, including matcher replay of prospective inputs.
• Keep validation evidence and outputs under data/validation/; leave prospective results/ with no prospective observations.
• Exclude these demonstrations from every prospective RQ analysis and count.
• Preserve unsuccessful demonstrations and revisions, not only successes.
• Quarantine previously unknown behavior according to the freeze policy.
• Obtain explicit approval before implementing or running validation execution machinery; approval of this document alone is not that approval.

If feasibility requires investigation of previously unknown empirical outcomes, stop and request editorial clarification. Such work must not be relabeled as already-public validation.

Bounded Demonstration

1. Fix the public target and expectations

Before reproduction, identify the existing case, primary and supporting commitments, public evidence, affected version, corrected version, and chosen execution route. Resolve any source-interpretation uncertainty explicitly.

The OCI content-identity commitment and the tool's VEX applicability rule are distinct. Equal content digests alone do not establish that every VEX statement must apply or suppress a finding.

2. Reproduce the known behavior

Use pinned artifacts and the existing public fixture to reproduce the reported failure and corrected behavior. Capture the commands, inputs, configuration, versions, hashes, raw outputs, and baseline finding required by the snapshot procedure.

Change only the intended transformation within each control/variant pair. Keep other conditions constant when comparing affected and corrected versions; record unavoidable differences as limitations.

Matcher replay supports a claim about the exercised matching path. It does not establish full-scanner behavior. Synthetic vulnerability identifiers must not be represented as public advisory evidence.

3. Establish valid SE-210 positioning

Construct the finite instance using the pinned SE-210 definitions. Explain the records, declared identity relation, surfaces, uses, sibling relation, and implemented relation needed for the claimed result.

Justify each mapping with source or implementation evidence. Do not infer an equivalence relation merely because outputs match, or convert directional applicability into symmetric identity.

If the prerequisites cannot be established, retain the operational observation but do not label it a formal witness. Record precisely which prerequisite is missing.

4. Check the formal result independently

For any valid positioned instance, run the literal oracle and optimized checker from the pinned operational-identity verification core. Require agreement and verify the extracted witness against the relevant definition.

Checker agreement establishes correctness for the supplied instance, not the correctness of the domain-to-formal mapping. Review that mapping separately. Do not require the fixed version to pass by changing commitments after seeing its output.

5. Test specificity and explanatory value

Use documented Trivy directional behavior as a permitted-difference control. The audit must not invent symmetric identity or report a violation solely because applicability is directional.

Use synthetic tests to ensure unsupported SE positioning and invalid witness claims are rejected or explicitly qualified.

For the Grype example, compare the ordinary output-difference explanation with the SE explanation. State concretely what SE adds: for example, a justified broken relation, a finite witness, a distinction between source underdetermination and implementation nonconformance, or a repair condition derived from the formal structure. Do not claim an advantage from terminology alone.

Have a second reviewer inspect the sources, mapping, witness prerequisites, and incremental explanation. Preserve disagreement. This focused review does not replace the prospective reliability procedure.

Decision Criteria

Go: All criteria are satisfied. The method is feasible enough to pursue the registered study; future empirical findings remain unknown.

Revise: A bounded implementation or modeling gap prevents evaluation, but the required commitments and SE positioning appear defensible. Preserve the failed attempt, document the revision, and repeat only the public validation demonstration. Do not expand into prospective discovery.

No-go for the current proposal: A valid mapping requires invented identity claims, directional matching must be forced into equivalence, formal witness prerequisites cannot be met, or SE adds only labels to an ordinary differential test. Narrow or stop the proposed formal contribution rather than claim it has been verified.

Decision record and disclosure

Record the decision, date, responsible reviewer(s), repository commit, public case and evidence references, reproduction artifacts, formal checks, limitations, disagreements, and revisions. Keep the record with validation evidence, outside prospective results.

Disclose this method-development work in the Stage 1 submission, including what was inspected and how it informed the design. Do not present known public defects as new discoveries or include validation examples in prospective RQ denominators.

Current conclusion: The bounded SE-210 demonstration has been completed successfully for the supplied candidate formalization.

The feasibility decision is Provisional Go.

The remaining go/no-go work is to independently justify the relevant Grype/VEX commitment and determine whether SE-210 provides analytical surplus beyond a high-rigor conventional conformance audit.

No prospective execution is authorized.

Challenge

The Grype OCI validation case presents a textbook trap for forcing false symmetric identity. The core risk lies in conflating artifact equivalence (an OCI digest match) with rule applicability (a VEX suppression).

OCI content identity is a symmetric relation: if Image A and Image B share a digest, they are the same artifact.

VEX applicability is strictly directional: if the target matches this digest, then apply this vulnerability suppression.

The temptation during the mapping phase is to define the VEX applicability decision itself as the implemented identity relation ($\mathcal{R}_{impl}$).

If we map a directional "applies-to" rule as an equivalence relation, we are structurally asserting that the scanner thinks the VEX document is the image.

This immediately destroys the formal validity of the SE-210 witness. To prevent this, the formal mapping must explicitly isolate the OCI digest as the identity basis ($\tau$) and treat the VEX rule application strictly as a directional operation occurring across an evaluated surface ($d$).

Step 1. Isolate the Finite Domain

Before touching the Python verification checkers, lock down the exact artifacts in VS Code. Do not run a full scanner suite against a live registry.

Pull the exact Grype binary version that exhibited the failure and the subsequent patched version.

Isolate the specific OCI image fixture and the corresponding VEX document that triggers VAL-GRYPE-OCI-REPOSITORY-URL-001.

Store the bounded feasibility artifacts under: data/validation/demo/.

The registered protocol fixture remains separately maintained under: data/validation/fixtures/grype/

After isolating the exact single feature change (the repository_url qualifier), we can run the reproduction to capture the evidence.

A. Acquire the pinned binaries

Open Git Bash terminal (for curl) and run.

mkdir -p ./bin
curl -sSfL https://raw.githubusercontent.com/anchore/grype/main/install.sh | sh -s -- -b ./bin v0.117.0
mv ./bin/grype ./bin/grype-0.117.0

curl -sSfL https://raw.githubusercontent.com/anchore/grype/main/install.sh | sh -s -- -b ./bin v0.118.0
mv ./bin/grype ./bin/grype-0.118.0

The pinned binary files are retained locally and excluded from version control because of their size. Their versions, acquisition procedure, and cryptographic hashes are recorded so that the environment can be reconstructed independently.

B. Create the bounded synthetic inputs

Create a minimal CycloneDX JSON SBOM representing the bare-digest description and a minimal OpenVEX document representing the repository-scoped description. This simulates the bare digest OCI image parsed by the Docker daemon, injecting a dummy vulnerability (CVE-2024-0001) to test the suppression.

SBOM: data/validation/demo/demo-synthetic-sbom.json

VEX: data/validation/demo/demo-synthetic-variant.vex.json

These are synthetic feasibility fixtures. They are not prospective research evidence and do not independently reproduce historical scanner behavior.

C. Run the Replay and Capture Diffs

Execute both binaries using the synthetic files and capture the JSON output.

(Note: Standalone historical binaries like v0.117.0 may exhibit offline database schema or compatibility limits when queried directly via CLI without an initialized local database cache; in such instances, the upstream PR #3659 regression test logic serves as the definitive empirical record).

mkdir -p ./data/validation/outputs/

# Run 0.117.0 (The VEX match fails; the vulnerability appears in the output)
./bin/grype-0.117.0 sbom:./data/validation/demo/demo-synthetic-sbom.json \
  --vex ./data/validation/demo/demo-synthetic-variant.vex.json \
  -o json > ./data/validation/outputs/demo-grype-0.117.0-output.json

# Run 0.118.0 (The VEX match succeeds; the vulnerability is suppressed)
./bin/grype-0.118.0 sbom:./data/validation/demo/demo-synthetic-sbom.json \
  --vex ./data/validation/demo/demo-synthetic-variant.vex.json \
  -o json > ./data/validation/outputs/demo-grype-0.118.0-output.json

D. Run the bounded SE-210 demonstration

Run (from the root project directory):

uv run python data/validation/demo/run_se210_grype.py

Step 2. Compare SE-210 to Audit

Step 1: Establish the Conventional Audit Baseline

The Action: Read the public issue description (VE-GRYPE-ISSUE-3657) and the merged fix in PR #3659.

The Output: Write down the conventional explanation of the defect:

Grype failed to suppress the vulnerability because its string-parsing logic split the PURL incorrectly when a repository_url qualifier was present, causing the internal VEX matcher to look for a non-existent product key instead of matching the underlying OCI digest.

This is accurate, human-readable, and tells you what went wrong. It is an observational prose summary, not a mathematical proof object. It cannot be programmatically checked by an independent script.

Step 2: Build the Finite SE-210 Instance

Next, take that same case and use SE-210:

1. Define the Domain ($R$): Create a finite domain of records representing the test case (e.g., $r_0$ for the control bare-digest PURL, $r_1$ for the variant repository-scoped PURL).
2. Define the Candidate Declared Regime ($\tau$): Model the content-preserving transformation as $\mathsf{PRS}$ with respect to OCI content identity. This is the candidate formalization being evaluated; it does not independently establish that VEX applicability must preserve the same operational treatment.
3. Define the Operational Surface ($d$): Map Grype's string-parsing behavior as an operational surface whose use ($U_d$) determines vulnerability suppression.
4. Feed it to the Checkers: Format this instance so it can be consumed by the Python verification code (oracle.py and fast.py) from the se-verification-operational-identity project.

uv run python data/validation/demo/run_se210_grype.py

Step 3: Extract and Inspect the Formal Witness

Run the script to see what the machine outputs.

The Output: Both independent checkers evaluate the supplied SE-210 instance and return the same finite divergence witness:

Verdict.FAIL | Witness: ('r0', 'r1')

The witness establishes divergence relative to the supplied formalization. Its interpretation as an external Grype nonconformance remains contingent on independent source-grounding of the relevant commitment.

Ask the Core Question: Look at what the checker produced. Did the formal machinery just print out what you already knew from Step 1, or did it mathematically isolate a structural flaw?

Step 4: Compare the Answers Side-by-Side

Evaluate the two outputs against each other to judge if the formal witness is "sharper":

Interpretability: Is the prose description easier to understand? (Usually yes for humans).

Machine Checkability: Once the externally justified formalization is fixed, can an independent checker mechanically verify that the supplied relations and operational signatures produce the claimed SE-210 witness? The bounded demonstration shows that both independent SE-210 implementations produce the same result.

Classifying the Break: Does SE-210 produce a materially better analytical product from the same evidence than a high-rigor source-grounded conformance audit? That question remains part of the added-value evaluation and must not be answered in SE-210's favor merely because the result is expressed formally.