5.1 KiB
5.1 KiB
Belnap K4 Trust Lattice Engine (VEX Resolution, Trust Algebra)
Module
Policy
Status
VERIFIED
Description
Full K4 lattice implementation with 4-valued logic (unknown/true/false/conflict), trust labels, lattice store, claim score merging, conflict penalization, and disposition selection. VEX normalization for OpenVEX and CSAF formats. Deterministic, commutative, idempotent merge operations. Comprehensive tests including property-based tests.
Implementation Details
- K4Lattice:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/K4Lattice.cs-- Belnap four-valued logic implementationK4Valueenum: Unknown (bottom), True, False, Conflict (top)- Knowledge ordering: Unknown < True|False < Conflict; True and False are incomparable
Join(a, b)-- knowledge join (union of support): T join F = Conflict; short-circuits on ConflictJoinAll(values)-- order-independent aggregation over sequence; short-circuits on ConflictMeet(a, b)-- knowledge meet (intersection): T meet F = Unknown; Conflict meet X = XLessOrEqual(a, b)-- knowledge ordering predicateNegate(v)-- swaps True/False; Unknown and Conflict are self-negatingFromSupport(hasTrueSupport, hasFalseSupport)-- constructs K4 value from support flags- Helper predicates:
HasTrueSupport,HasFalseSupport,IsDefinite,IsIndeterminate
- TrustLatticeEngine:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/TrustLatticeEngine.cs-- orchestrates complete trust evaluation pipeline- Pipeline: VEX normalization -> claim ingestion -> K4 lattice evaluation -> disposition selection -> proof bundle generation
IngestVex(document, format, principal, trustLabel?)-- ingests VEX document via registered normalizersIngestClaim(claim)/IngestClaims(claims)-- direct claim ingestion into LatticeStoreGetDisposition(subject)-- evaluates subject and returns DispositionResultMergeClaims(scoredClaims, policy?)-- merges scored VEX claims using ClaimScore-based algorithmEvaluate(options?)-- evaluates all subjects with optional proof bundle generation and subject filtering- Fluent
ClaimBuilderwithAssert(atom, value),Present(),Applies(),Reachable(),Mitigated(),Fixed(),Misattributed()
- ClaimScoreMerger:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/ClaimScoreMerger.cs-- lattice-based merge with conflict penalizationMerge(scoredClaims, policy)-- orders by adjusted score, specificity, original score; selects winnerConflictPenalizerapplies configurable penalty (default 0.25) to conflicting claimsMergePolicyoptions:ConflictPenalty,PreferSpecificity,RequireReplayProofOnConflict- Returns
MergeResultwith: winning claim, all scored claims, conflict records, confidence, RequiresReplayProof flag
- LatticeStore:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/LatticeStore.cs-- subject state storage and claim aggregation - DispositionSelector:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/DispositionSelector.cs-- applies policy rules to select final disposition - ConflictPenalizer:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/ConflictPenalizer.cs-- applies configurable penalties to conflicting claims - SecurityAtom:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/SecurityAtom.cs-- atomic propositions (Present, Applies, Reachable, Mitigated, Fixed, Misattributed) - VEX Normalizers:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/VexNormalizers.cs,OpenVexNormalizer.cs,CsafVexNormalizer.cs-- normalize CycloneDX, OpenVEX, CSAF formats to claims - TrustLabel:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/TrustLabel.cs-- trust level annotations for claims - PolicyBundle / ProofBundle:
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/PolicyBundle.cs,ProofBundle.cs-- policy configuration and proof bundles with decision traces
E2E Test Plan
- Create TrustLatticeEngine with default policy; ingest two claims with True and False assertions for same subject; verify K4 value is Conflict
- Ingest claims from OpenVEX, CycloneDX, and CSAF documents; verify all three normalizers produce valid claims in the LatticeStore
- Verify Join commutativity:
Join(a, b) == Join(b, a)for all K4Value combinations - Verify Join idempotency:
Join(a, a) == afor all K4Value values - Verify Meet/Join absorption:
Join(a, Meet(a, b)) == afor all K4Value combinations - Verify conflict penalization: merge two claims with different VEX statuses; winning claim has lower adjusted score than original when conflict detected
- Verify
RequiresReplayProofis set whenRequireReplayProofOnConflict=trueand conflicts exist - Evaluate all subjects with
GenerateProofBundle=trueand verify proof bundle contains atom tables, claims, and decisions - Verify subject filter: evaluate with SubjectFilter containing one digest; only that subject's disposition is returned
- Verify ClaimBuilder fluent API: create claim with
Present().Reachable().Mitigated()and verify three assertions are ingested