Understanding SE-210 and Structural Explainability in Vulnerability Matching

For those new to Software Engineering, Software Bill of Materials (SBOMs), and Structural Explainability (SE), this guide begins with the basics and introduces the SE-210 Operational Identity framework, Operational Identity: A Finite Audit of Declared and Implemented Rules of Sameness, which provides the formal foundation for this research.

Introduction and Background

Modern software isn't written in a vacuum; it is assembled from thousands of pre-compiled components, open-source packages, and container images.

A CVE (Common Vulnerabilities and Exposures) is a publicly known cybersecurity flaw that has been cataloged and given a unique identification number. Managed by the MITRE Corporation and funded by the US Department of Homeland Security, the CVE program acts as a universal dictionary for software vulnerabilities. This ensures that security professionals, software vendors, and scanning tools (like Grype and Trivy) are all talking about the same security flaw when they use its ID.

The SBOM (Software Bill of Materials): An SBOM is the formal ingredients list for a software package. It lists every component, library, and container image inside a deployment.

Vulnerability Matching & VEX: When a security flaw (like a CVE) is discovered, vulnerability scanners (like Grype or Trivy) inspect the SBOM to see if an affected package is present. A VEX (Vulnerability Exploitability Exchange) statement is a companion document that says: "Yes, the vulnerable code is present, but it is not exploitable in this specific context (e.g., it's patched or disabled)."

A PURL is a standardized, URL-compatible string format designed to universally identify and locate software components (such as libraries, container images, or modules) across different package ecosystems (e.g., npm, PyPI, Maven, OCI) so that tools can reference them unambiguously regardless of where or how they are packaged.

Motivation: The Problem with Conventional Auditing

When a scanner fails, such as failing to recognize that a VEX statement applies to a container image because of a minor URL string variation, auditors typically write a human-readable bug report:

The tool failed because its string parser split the URL incorrectly when a repository_url qualifier was present.

While accurate, this prose summary is not machine-checkable. It requires a human expert to read, interpret, and manually verify.

Enter SE-210: Operational Identity

The SE-210 Operational Identity framework provides a formal way to represent declared and implemented rules of sameness over a finite record domain.

Mathematically, a rule of sameness can be represented as a partition of that domain: records that are considered the same under the rule belong to the same group, while records considered different belong to separate groups.

Rather than asking whether two representations appear similar, SE-210 models these identity relations explicitly and checks whether observed operational behavior is consistent with the supplied rules.

If the operational behavior splits records that the declared rule requires to remain together, SE-210 can extract a finite divergence witness identifying the inconsistency.

Initial Feasibility

We want to design a formal study to see how SE-210 can help. Before proposing the detailed protocol, we want some initial indication of feasibility.

Plain Language Feasibility

Before using this method in a larger study, we ran a small feasibility test based on a publicly documented Grype vulnerability-matching problem.

The test used two descriptions of the same container image. Both descriptions included the same SHA-256 digest, which identifies the underlying container contents. One description used only the digest. The other also included a repository_url qualifier describing where the image came from.

In the historical Grype case, that extra repository information affected whether a VEX statement was matched and whether a vulnerability was suppressed.

For the feasibility test, we represented the two descriptions as two records:

• r0: the container identified by its digest alone;
• r1: the same digest plus a repository_url.

We then supplied the SE-210 Operational Identity framework with a candidate rule saying that adding the repository location does not change the underlying container content.

The two description records were given different observed security outcomes:

• r0: vulnerability suppressed;
• r1: vulnerability not suppressed.

SE-210 was then run using the two provided independent implementations: a direct mathematical oracle and a faster optimized checker.

Both produced the same result:

The supplied rule says the two descriptions preserve the same underlying identity, but the modeled security behavior treats them differently.

Both implementations identified the same pair, (r0, r1), as the finite example showing that divergence.

This was an important first result because it demonstrated that the Grype case can be represented in the SE-210 framework and that the two independent implementations agree on the result.

It does not yet prove that Grype violated an external VEX requirement. The remaining question is whether the relevant standards, Grype documentation, or other source-grounded evidence actually require the two descriptions to receive the same vulnerability-matching treatment.

So the feasibility result is a provisional go: the method works technically on this kind of case, but the external rule of sameness still has to be justified before the example can be called a confirmed nonconformance witness.

Evaluating the Grype Case

In SE-210, the finite domain $R$ consists of records ($r$), discrete, atomic entities (such as package references, image descriptors, or SBOM entries) whose identity lineage and operational behavior are tracked across system surfaces.

In our Grype case (DEMO-VAL-GRYPE-OCI-REPOSITORY-URL-001), we examined two records from this domain:

• $r_0$: A bare-digest OCI image PURL (pkg:oci/debian@sha256:...), representing the control record (the baseline OCI reference that successfully applied the VEX suppression under normal scanner execution).
• $r_1$: A repository-scoped OCI image PURL with a query qualifier (?repository_url=...), representing the variant record (the modified locator reference that failed to match due to parser divergence).

The two fixture records preserve the same OCI content digest: adding the repository_url qualifier does not alter the referenced content digest.

For the bounded SE-210 demonstration, we therefore test a candidate formalization in which the transformation is classified as $\mathsf{PRS}$ with respect to content identity.

Under that supplied formalization, the operational signatures differ:

• $r_0$: SUPPRESSED
• $r_1$: NOT_SUPPRESSED

The dual-checker run consequently returns a divergence witness $(r_0, r_1)$.

This establishes that SE-210 detects the inconsistency implied by the candidate formalization. It does not yet establish that Grype or the applicable VEX semantics require suppression to be invariant under this transformation. That external commitment must be established separately.

The Risk of a Contrived Mapping

The danger is forcing directional logic into a symmetric equivalence.

• Symmetric Identity ($A \equiv B$): Two records refer to the exact same artifact.
• Directional Applicability ($A \implies B$): A VEX statement written for a base digest may apply to a repository-scoped variant, but the reverse or the scope rules might involve complex inclusion logic.

If our mapping declared $r_0 \equiv r_1$ just because the scanner outputs mismatched and we wanted the checker to fire, we would be committing a logical sin: inventing an identity relation where none exists.

Does the Grype OCI Case Present a Directional Trap?

Yes. The Grype case presents a classic tension between content identity and locator scope:

• The Trap: An evaluator might be tempted to say, "Because both PURLs point to the same SHA256 digest, they are identical in every operational context ($r_0 \equiv r_1$)."
• The Reality: While their content is identical, their lookup keys inside the scanner's internal database differ due to the repository_url string parameter.

How to Fix and Maintain Rigor

To ensure we never fake or force the mapping, we adhere to strict validation rules:

1. Separate Content from Lookup: Explicitly model the declared regime around immutable content hash preservation ($\tau$), while treating the scanner's string parser as an independent operational surface ($d$).
2. Check the Witness Interpretation: The divergence witness (r0, r1) must not be interpreted as "the PURLs are different." Instead, under the candidate SE-210 formalization it identifies a precise structural inconsistency: the modeled content-preservation relation connects $r_0$ and $r_1$, while the observed operational signatures assigned to those records differ. Whether that inconsistency constitutes an actual Grype/VEX nonconformance depends on independently establishing that the relevant matching commitment requires preservation across this transformation.

Strengths of Our Proposed Plan

1. Methodological Hygiene

Our plan establishes a clear boundary between retrospective validation and prospective discovery. By relying on a strict freeze policy, snapshot procedures, and a clear Stage 1 registered report structure, the project protocol prevents retroactive theorizing. Isolating the data/validation/ directory from the results/ directory ensures that method development does not contaminate the prospective execution.

2. Robust Engineering Foundation

The initial evidence includes over 40 passed tests, strict manifest validation, nearly 90% coverage, and verification of exact permitted fields and execution phases. It demonstrates that the underlying schema and validation machinery are stable. The infrastructure appears capable of handling complex execution routes (full_scanner, matcher_replay) without false positives caused by schema errors.

3. Criteria

The plan includes explicit Proceed, Revise, and No-go outcomes.

For example, the bounded demonstration does not justify proceeding if SE-210 adds only formal labels to conclusions already available from a high-rigor conventional conformance audit.

These criteria make the feasibility decision falsifiable without overstating a negative result as disconfirmation of the SE-210 framework itself.

4. SE-210 Represents Identity as Finite Partitions

SE-210 represents rules of sameness as partitions of a finite record domain. Each partition groups records that must be treated as equivalent under a particular declared identity rule.

Operational behavior induces its own grouping.

A divergence occurs when the operational grouping separates records that the declared identity rule requires to remain together.

This structure allows the framework to extract a finite divergence witness that can be checked independently once the formalization has been fixed.

5. SE-210 Dual-Checker Verification

SE-210 provides two independent checkers:

• an oracle.py that directly computes the mathematical definitions,
• and a fast.py that uses an optimized near-linear ($O(n \alpha(n))$) union-find algorithm

SE-210 compares their outputs across randomized instances and bounded validation cases, offering strong computational evidence that the optimized checker implements the same decision procedure as the oracle.

This cross-check validates the implementation of the formal machinery; it does not validate the external semantic assumptions used to construct a particular SE-210 instance.

6. Methodological Boundaries

The SE-210 paper is clear about what it does not do. It explicitly acknowledges that:

• Faithfulness is one-directional (merging records isn't necessarily a fault, but splitting them is).
• A "Pass" verdict is non-monotone (adding new history can suddenly create a divergence witness).
• The audit checks for internal consistency, not external truth.

7. Real-World Relevance (The Legal AI Example)

The SE-210 Section 6 legal-alignment example grounds the heavy math in a highly relevant modern problem: AI governance. When dealing with AI agents filing regulatory documents or citing rules, a system that breaks co-reference just because a text string was slightly reformatted (sub-sibling divergence) could derail an entire audit trail. The framework mathematically catches that error.

Value Proposition

The research transitions from a standard software engineering exercise into a formal scientific contribution if it successfully operationalizes SE-210.

Conventional differential testing relies heavily on output comparisons. Even a careful conformance audit using semantic oracles ultimately reports that a defect exists. SE-210 offers the potential to mathematically pinpoint why it exists in the structural logic. If SE-210 can generate a finite, independently checkable witness, categorize a justified broken relation, or automatically derive a formal repair condition from the architecture itself, it elevates vulnerability matching from heuristic patching to formal accountability.

SE-210 Challenges

The real-world deployment of the SE-210 framework will likely face practical bottlenecks:

• The "Discovery" Problem: The algorithm is fast, but it requires perfectly constructed inputs (the $R$ domain, the family histories, the evaluated surfaces, and the identified uses). As noted in Section 7, the framework evaluates the disclosed mechanisms. In a massive, undocumented legacy codebase or a complex cloud deployment, simply finding the mechanisms (the fields, workflow states, or app predicates) to feed into the registry will require immense manual labor or advanced static analysis.
• The Completeness Claims: The framework relies on Registry Completeness, Family Completeness, and Use Completeness. Because the audit only checks what is disclosed, a malicious or negligent operator could easily achieve a PASS verdict by simply omitting the specific mechanism or surface that carries the undeclared identity rule.

Risks and Required Adjustments

To clear the go/no-go hurdle, the bounded demonstration must navigate three strict constraints:

1. The Conformance Audit Baseline

The standard for comparison is set too low if SE-210 is only compared to a "raw output diff." A conventional, source-grounded conformance audit already incorporates commitments and semantic oracles to separate actual defects from permitted differences. The validation plan must explicitly define what SE-210 extracts from the Grype VAL-GRYPE-OCI-REPOSITORY-URL-001 case that a highly skilled human auditor using conventional differential testing would miss or be unable to formalize.

2. Forcing Equivalence on Directional Logic

As noted, OCI digest identity (a symmetric equivalence relation) does not automatically dictate VEX applicability (a directional rule). There is a high risk of forcing directional applicability into a symmetric identity to make the formal SE-210 witness "fit." If the mapping invents an equivalence relation merely because the scanner outputs match, the formal validity of the witness is destroyed. The mapping must strictly respect the difference between source underdetermination and implementation nonconformance.

3. The Corpus Adequacy Trap

The feasibility of the machinery using historical public evidence (like Grype and Trivy) does not guarantee the feasibility of the prospective study. A registered report protects against publication bias, but sparse findings will only support a meaningful paper if the analytical method (SE-210) extracts deep, structural insights from those few findings. If the yield is low and SE-210 fails to provide a novel repair condition, the resulting paper will be methodologically sound but scientifically thin.

Next Step

The bounded checker demonstration has been completed. For the supplied Grype formalization, both independent SE-210 implementations return:

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

The next step is not additional checker execution. It is validation of the abstraction.

We must independently establish the source-grounded matching commitment that governs the relationship between the bare-digest OCI PURL and the repository_url-qualified PURL, and determine whether that commitment requires the relevant operational treatment to be preserved.

Only after that commitment is established should the generated $(r_0, r_1)$ pair be called a Grype nonconformance witness.

The same case should then be analyzed using the high-rigor conventional conformance baseline so that the go/no-go comparison can answer:

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

To prove that Structural Explainability (SE-210) provides a defensible scientific contribution, the comparison structure must isolate the exact analytical surplus generated by formalizing the accountability surface. The baseline is a high-rigor conformance audit, one that already leverages semantic oracles and domain commitments. The comparison should be structured as a strict differential evaluation, testing whether SE-210 extracts structural logic that the conformance audit fundamentally cannot represent.

The Evaluation Matrix

Assess the identical validation case (VAL-GRYPE-OCI-REPOSITORY-URL-001) through both methods, grading the output against four specific criteria. If SE-210 cannot claim a distinct advantage in at least one of these areas, it fails the added-value test.

Structuring the Formal Comparison Document

When documenting the go/no-go demonstration, use the following structure to enforce a rigorous comparison.

Part 1: The Conformance Baseline

Execute the standard audit. Define the primary commitment, the execution route, and the specific failure. State the conclusion a highly skilled auditor would reach.

Constraint: Give the conventional audit the benefit of the doubt; assume the auditor deeply understands the tool's commitments and the semantic context.

Part 2: The SE-210 Abstraction

Translate the case into the finite core of SE-210. Explicitly map the domain commitments to the formal ontology.

Define the operational surfaces ($S$), the declared relations ($\mathcal{R}{commit}$), and the implemented relations ($\mathcal{R}{impl}$).

Part 3: The Delta Analysis (The Core Test)

Directly contrast the findings using the matrix criteria above. We must answer:

What is the formal witness? Define it precisely. For example, show that the implemented relation fails to preserve the required mapping: $$\mathcal{R}{impl}(x, y) \not\subset \mathcal{R}{commit}(x, y)$$

Did we invent identity? Prove that the SE-210 mapping respected the directionality of the source evidence (e.g., OCI digest matching vs. VEX applicability) without falsely classifying permitted directional matching as an identity violation.

What is the analytical surplus? State in one sentence what SE-210 proved that the raw conformance audit only implied.

If the abstraction in Part 2 requires logical leaps, or if the Delta Analysis in Part 3 yields nothing more than a formal translation of the auditor's prose, the method provides insufficient explanatory value.

Current Result: Candidate SE-210 Witness for the Grype Case

The bounded Grype demonstration now establishes one important technical result: SE-210 can represent the candidate case and both checker implementations independently return the same divergence witness.

The fixture preserves the OCI content digest while changing the repository_url qualifier. We modeled that transformation as $\mathsf{PRS}$ with respect to content identity and assigned the observed operational outcomes as signatures:

• $r_0$: SUPPRESSED
• $r_1$: NOT_SUPPRESSED

Under that formalization, both oracle.py and fast.py return:

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

This demonstrates that the formal machinery behaves as intended: given the supplied preservation relation and divergent operational signatures, it produces a finite, reproducible witness.

It does not yet establish that this witness proves Grype nonconformance. OCI content identity alone does not imply that VEX applicability must be invariant under every locator transformation. The remaining validation question is therefore external to the checker:

Does the applicable Grype/VEX matching specification, documented behavior, or other independently justified commitment require $r_0$ and $r_1$ to receive the same relevant operational treatment?

If yes, the candidate witness becomes a source-grounded nonconformance witness.

If no, the checker has correctly analyzed the supplied model, but the model does not represent a valid external commitment and the Grype case must not be claimed as an SE-210 defect witness.

Translation Barrier

The single greatest Achilles' heel of applied formal methods is the ontological gap (or the translation barrier).

It reveals an uncomfortable truth: formal verification does not eliminate human error; it merely relocates it.

If a human analyst has to manually inspect a messy codebase, decide what constitutes a "record" ($R$), guess at the family histories ($\tau$), and hand-wire the operational surfaces ($d$), then the resulting "mathematical proof" is only as objective as the human who wrote the mapping.

If the mapping is biased or flawed, the lattice checker will happily output a rigorous, mathematically pristine proof of a completely imaginary premise.

Why This Happens (And Why It's Inevitable)

Computers cannot natively read a sprawling Go or Python repository and understand what a developer meant by an OCI repository URL qualifier.

Semantic intent lives in human heads, design docs, and issue trackers.

Codebases are implementation artifacts; formal models are mathematical abstractions.

Bridging that gap requires an act of translation, and translation is inherently manual.

How to Defend Against the "Manual Mapping" Critique

When presenting this work to a cynical program committee or a rigorous review board, we have to face this objection head-on.

Here is how to keep it from sinking the research:

Explicitly Bound the Claim: SE-210 never claims to automate discovery. As noted in the framework's boundaries, it evaluates disclosed mechanisms. It is a tool for accountability, not automated bug-hunting. The goal isn't to prove the software is bug-free in the wild; the goal is to prove that given a declared specification of identity, the implementation violates it.

Shift from Ad-Hoc Code to Declarative Manifests: This is why structuring things via explicit schemas, manifests, and configuration files matters so much. If the mapping ($R, \tau, d$) is written as an opaque, ad-hoc Python script, it is not reviewable.

But if the mapping is expressed as a formal, version-controlled artifact, such as a structured JSON Schema or an accountable surfaces manifest, then the translation layer becomes a transparent, peer-reviewable specification.

The Long-Term Fix (Automated Lifting): Eventually, moving past the manual bottleneck requires "lifting" formal instances directly from static analysis, dependency graphs, or OpenAPI specs, rather than hand-writing them.

But for a foundational feasibility study, manual curation of historic benchmark cases (like Grype #3657) is a necessary first step to prove the lattice math even works under controlled conditions.