SE Verification: Vulnerability Matching - Feasibility Part 2

Project

Repository: structural-explainability/se-verification-vulnerability-matching

The project is an exploratory MSR 2027 Registered Report study applying the SE-210 Operational Identity framework to security-relevant identity semantics in software vulnerability matching.

The contribution under evaluation is identity conformance, not scanner disagreement.

Before SE-210 audits an implementation, the method must establish whether the governing semantic rule belongs within SE-210’s jurisdiction.

Prospective execution remains disabled.

Part 1 Result

A bounded feasibility demonstration has been completed using the public Grype OCI repository_url case.

The demonstration models two records:

r0: bare-digest OCI PURL;
r1: the same digest with a repository_url qualifier.

For the supplied candidate SE-210 formalization:

r0 has operational signature SUPPRESSED;
r1 has operational signature NOT_SUPPRESSED;
both the literal oracle and optimized SE-210 checker return:

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

This establishes checker agreement and demonstrates that the case can be represented in the finite SE-210 machinery under the supplied candidate formalization.

Two limits on that result now govern everything downstream.

Directional, not symmetric. The Part 1 formalization used a symmetric content-preservation relation. The governing VEX product-matching commitment (OpenVEX / go-vex PurlMatches) is directional: the more general identifier matches the more specific one, and the specific side may add qualifiers. So (r0, r1) is a machinery witness for the supplied model, not yet the correctly structured semantic witness for the Grype defect.

Coverage lifting may be faithful but structurally limited.

A directional coverage predicate can be lifted into a binary classification over a finite identifier domain: { covered, not-covered }.

That lifting does not automatically preserve the semantics of the directional commitment, for two reasons.

First, an unlabeled two-block partition does not record which block means covered and which means not-covered; the opposite predicate yields the identical partition.

Any faithful lifting must make that role explicit.

Second, two distinct two-block partitions are never in a refinement relation: neither refines the other, so they are either equal or incomparable.

Incomparability is reachable, so the encoding is not lattice-trivial; but for two-block partitions it coincides with the two covered sets being non-nested, which a labeled set comparison already expresses.

Proper refinement structure, that is, the sub-/super-sibling cases that exceed that set comparison, is unreachable below three blocks.

The feasibility question is therefore whether a lifted representation exercises SE-210's refinement structure in a way that adds information beyond the labeled predicate comparison already available to a conventional audit.

Consequently, the Grype case does not currently demonstrate partition-native Layer-2 surplus.

The Grype case is retained as a Layer-1 translation and boundary case. A second structural case is required to determine whether SE-210's partition machinery contributes genuine Layer-2 value.

The current feasibility decision remains Provisional Go.

Grype Case: Assigned Role

The Grype repository_url case is retained as a Layer-1 / boundary case, with three explicit jobs:

exercise the translation discipline - direction, general/specific roles, qualifier semantics, identity dimension;
exercise the admissibility check that rejects the symmetric-content model as INVALID;
serve as a boundary case for surplus - a case used to determine whether lifting a directional predicate into SE-210 adds genuine structural information or merely restates the conventional predicate comparison.

The Grype case must not be credited with Layer-2 surplus unless that surplus is demonstrated independently of the translation discipline itself.

Part 2: Source-Ground and Orient the Commitment

First action (before any modeling): pin the concrete case. Read Grype issue #3657 directly and the PR #3659 diff, and record from the diff which candidate identifiers Grype now generates. The release note alone is insufficient; the issue body and diff are the authoritative source for orientation and for whether the defect is a matching direction failure or an identifier-set completeness gap.

Do not infer the commitment from the SE-210 result. Investigate and record evidence from:

the Package URL OCI definition;
PURL qualifier semantics, especially repository_url;
the Grype issue documenting the failure (#3657);
Grype PR #3659 implementing the fix;
Grype v0.118.0 release documentation;
relevant OpenVEX / go-vex product-matching semantics (PurlMatches, Component.Matches, Product.Matches).

The critical questions are:

What exact product-matching relation governs the Grype case?
Which identifier is the more general product identifier, which is the more specific identifier, and which side carries the repository_url qualifier?
Under that documented direction, should the applicable VEX product match the identifier generated from the scanned OCI image - or is the defect that the scanned side failed to generate a qualified candidate identifier at all (an identifier-set completeness gap rather than a matching-direction gap)?

Note the completeness reading explicitly. If the VEX product carried repository_url and the scanned identifier did not, strict PurlMatches makes the non-match correct, and the nonconformance relocates to Grype's generated candidate set G: G should have contained a repository_url-qualified identifier for the scanned image. Establish which of these the sources actually support.

The answer must come from the OpenVEX/go-vex matching contract and the concrete Grype issue and fix, not from content identity alone.

The commitment must be narrowly worded.

We must not claim that:

every pair of OCI PURLs sharing a digest is operationally equivalent;
repository_url can never affect identity;
OCI content identity automatically determines VEX applicability.

If the sources justify the narrower Grype-specific invariant, we add a source-grounded commitment to contracts/commitments.toml and corresponding provenance records to contracts/sources.toml.

Translation-Validity Question

Part 2 must also begin formalizing the translation layer between external domain semantics and SE-210.

The desired long-term pipeline is:

external source
--> declared commitment
--> declarative translation manifest
--> translation validation
    --> ADMISSIBLE
    --> UNDERDETERMINED
    --> UNSUPPORTED
    --> INVALID

ADMISSIBLE only
--> SE-210 instance
--> oracle + optimized checker
--> PASS / FAIL + witness

The translation layer should eventually enforce rules such as:

every SE-210 relation must cite an external commitment;
the commitment must govern the same identity dimension being modeled;
directional applicability must not be promoted to symmetric identity without independent justification;
when a commitment is directional, the translation must explicitly record source role, target role, general/specific orientation, and allowed qualifier extension;
observed scanner output must not be used to choose the relation against which that output is tested;
content, package, locator, platform, and vulnerability-applicability identities must remain distinguishable;
ambiguous source semantics should produce UNDERDETERMINED, not an invented PASS or FAIL.

Jurisdiction Classifier

SOURCE SEMANTICS
↓
TRANSLATION CLASSIFIER

Can this commitment be represented faithfully as an SE-210
operational-identity relation?

        ├── YES
        │    ↓
        │   SE-210 partition audit
        │
        ├── DERIVABLE
        │      ↓
        │   justified, semantics-preserving lifting
        │      ↓
        │   SE-210 audit
        │
        └── NO
            ↓
           outside SE-210 scope
           use native directional/predicate conformance

Verdict Taxonomy (Two-Stage)

Verdicts are split so that "the implementation failed" is never conflated with "we could not validly construct the model." The three model-construction failures are kept distinct because they sit at different points in the pipeline.

TRANSLATION VERDICT              (Layer 1: can we validly build the instance?)
  ADMISSIBLE                     translation cites a commitment, dimension,
                                 direction, and roles that check out
  UNDERDETERMINED                the source standard does not fix the commitment
  UNSUPPORTED                    the commitment cannot be expressed in SE-210
  INVALID                        the translation is provably wrong
                                 (e.g. directional modeled as symmetric)

CONFORMANCE VERDICT              (Layer 2: given an admissible model, conform?)
  PASS
  FAIL + witness
  NOT_EVALUATED                  emitted whenever TRANSLATION != ADMISSIBLE

Gating: the conformance stage runs only on ADMISSIBLE. Everything else yields NOT_EVALUATED, with the translation verdict carrying the finding.

Under Part 1's symmetric-content model, the Grype case is: TRANSLATION: INVALID (directional relation modeled as symmetric), CONFORMANCE: NOT_EVALUATED.

Second Structural Case (Required GO Gate)

Because the Grype case does not yet demonstrate partition-native Layer-2 surplus, a second structural case is required, not optional, before a full GO.

Committed case family: alias / merge / split over a single artifact, realized via multiple SBOM generators or an SPDX <-> CycloneDX round-trip.

Rationale: a merge/split is definitionally a partition phenomenon -

Declared:        A == B,  B != C
Implemented:     A == C,  B separate

This configuration is intrinsically relational rather than a single covered/not-covered predicate.

With multiple identity bases over one finite record set (content / package / locator / document-local / vulnerability-applicability), the SE-210 refinement structure has an opportunity to distinguish merges, splits, and incomparable classifications that are not naturally represented by one Boolean predicate.

Whether that produces genuine analytical surplus is the purpose of the test.

Purpose of the second case: test whether SE-210's native partition machinery provides genuine Layer-2 analytical surplus once translation is admissible.

Added-Value Test

After source-grounding and orienting the commitment, analyze the same case using the strongest reasonable conventional source-grounded conformance audit.

Then answer:

Does SE-210 produce a materially better analytical product from the same evidence add after the conventional audit has already reached its strongest defensible conclusion?

Two guards on this test:

The baseline auditor performs an implicit semantic translation (reads the standard, identifies direction and roles, checks the implementation). Credit them with it. The fair Layer-1 comparison is whether making translation explicit and machine-checkable exposes mapping errors that stay implicit - not whether SE-210 caught an error our own initial formalization introduced.
A symmetric SE-210 witness over a directional external commitment is not analytical surplus. It is a translation error and must be rejected.

Candidate forms of genuine surplus:

a mechanically derivable finite witness;
formal classification of the broken identity relation;
faithful formalization of one-way applicability without collapsing it into symmetric identity;
explicit rejection of an unsupported mapping;
distinction between implementation nonconformance and source underdetermination;
a repair condition derived from the formal structure;
a reusable declarative translation artifact.

Feasibility Decision

The go/no-go has an explicit ceiling per case:

Grype case alone yields at most a translation-discipline GO. It can support a methods contribution through explicit, auditable, two-stage translation and conformance, and it can demonstrate an important framework boundary. It does not by itself establish partition-native analytical surplus.

Full GO requires the second structural case to demonstrate that the partition-based SE-210 analysis yields a defensible structural result that is not reducible to the same labeled predicate comparison supplied by the conventional baseline.

If the second case also reduces to predicates, that is a strong, honest bounding result: the contribution is the translation discipline and the verdict taxonomy, and the program is scoped to co-reference/identity cases rather than arbitrary applicability. Still publishable; a smaller and different claim, and one that must not be freezing-time surprise.

Do not freeze the Registered Report design until the second case has been run.

Broader Feasibility Direction

If Part 2 succeeds, promising future prospective test families include:

SPDX <---> CycloneDX representation changes;
SPDX --> CycloneDX --> SPDX round-trip identity preservation;
multiple SBOM generators applied to the same artifact;
PURL qualifier transformations;
identifier-strength changes such as PURL, hash, CPE, or combinations;
SBOM-to-VEX identity propagation;
alias/merge/split cases;
intentionally lossy representation changes.

CISA provides a baseline mapping of component attributes between SPDX 3.0 and CycloneDX, making cross-format identity preservation a particularly promising future test family.

The long-term best-case contribution is a reusable conformance method for identity-sensitive software-supply-chain transformations.

Best Case Adopted Workflow May Be 2 Layers

LAYER 1 - TRANSLATION VALIDITY

What does the external standard actually require?

Can that rule be represented faithfully in SE-210?

Are direction, roles, and identity dimension preserved?

LAYER 2 - CONFORMANCE

Given an admissible translation, does the implementation behave consistently with that rule?

Producing something like:

TRANSLATION: ADMISSIBLE

Commitment:
OpenVEX qualifier-subset matching

Relation:
directional applicability

General identifier:
<established from source commitment>

Specific identifier:
<established from source commitment>

Result:
FAIL

Witness:
(...)

Example Verdict Meanings

INVALID: You tried to treat applicability as identity.

UNSUPPORTED: This rule is not expressible by this framework.

FAIL: The translation is valid and the implementation actually violates it.

Possible Workflow if Feasibility is Shown

SBOM / VEX / package metadata
↓
source-grounded identity / applicability commitments
↓
declarative SE translation manifest
↓
TRANSLATION VALIDATION
  - identity dimension
  - direction
  - roles
  - allowed transformations
  - source provenance
↓
ADMISSIBLE
UNDERDETERMINED
UNSUPPORTED
INVALID
↓
SE-210 Operational Identity finite conformance audit
[ADMISSIBLE translations only]
↓
PASS
or
FAIL + finite witness
↓
CI / scanner testing / standards conformance

Or

software-supply-chain representation
↓
externally grounded semantic rule
↓
reviewable translation
↓
translation validation
↓
formal conformance audit
↓
actionable result

That is, scanner vendors, SBOM/VEX processors, CI systems, or standards test suites could declare the identity/applicability rules they claim to implement, then automatically test whether their software preserves those rules across legitimate representation changes.