571 lines
54 KiB
Markdown
571 lines
54 KiB
Markdown
# K4 Belnap Four-Valued Logic
|
||
|
||
## Overview
|
||
|
||
StellaOps uses K4 Belnap four-valued logic to handle uncertainty and conflicting evidence in policy decisions. This enables the system to represent "both true and false" (conflict) and "neither true nor false" (unknown) states that naturally arise when aggregating evidence from multiple sources.
|
||
|
||
---
|
||
|
||
## Why Four Values?
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ THE PROBLEM WITH BINARY LOGIC │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ In classical two-valued logic (True/False): │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ Scenario: Is this vulnerability reachable? │ │
|
||
│ │ │ │
|
||
│ │ Evidence sources: │ │
|
||
│ │ • Static analysis: "Yes, I found a path" → True │ │
|
||
│ │ • Runtime observation: "No activity seen" → ??? (not False) │ │
|
||
│ │ • VEX statement: "Not affected in our configuration" → False │ │
|
||
│ │ │ │
|
||
│ │ Problem: How do we combine True + False? │ │
|
||
│ │ • AND(True, False) = False (lose the static evidence) │ │
|
||
│ │ • OR(True, False) = True (lose the VEX evidence) │ │
|
||
│ │ │ │
|
||
│ │ Neither preserves the fact that we have CONFLICTING evidence! │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ Another scenario: No evidence available │ │
|
||
│ │ │ │
|
||
│ │ • No static analysis run → ??? │ │
|
||
│ │ • No runtime observation → ??? │ │
|
||
│ │ • No VEX statement → ??? │ │
|
||
│ │ │ │
|
||
│ │ Problem: This isn't "False" - we just don't know yet! │ │
|
||
│ │ Classical logic forces us to pick True or False when we have no information.│ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## The Four Values
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ K4 BELNAP TRUTH VALUES │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ THE BILATTICE │ │
|
||
│ │ │ │
|
||
│ │ ┌───────────┐ │ │
|
||
│ │ │ ⊤ │ BOTH (Conflict) │ │
|
||
│ │ │ "Both" │ Evidence says BOTH true AND false │ │
|
||
│ │ │ │ (conflicting sources) │ │
|
||
│ │ └─────┬─────┘ │ │
|
||
│ │ │ │ │
|
||
│ │ ╱─────┴─────╲ │ │
|
||
│ │ ╱ ╲ │ │
|
||
│ │ ╱ ╲ │ │
|
||
│ │ ┌───────┴───────┐ ┌───────┴───────┐ │ │
|
||
│ │ │ T │ │ F │ │ │
|
||
│ │ │ "True" │ │ "False" │ │ │
|
||
│ │ │ │ │ │ │ │
|
||
│ │ │ Evidence │ │ Evidence │ │ │
|
||
│ │ │ supports │ │ supports │ │ │
|
||
│ │ │ "yes" │ │ "no" │ │ │
|
||
│ │ └───────┬───────┘ └───────┬───────┘ │ │
|
||
│ │ ╲ ╱ │ │
|
||
│ │ ╲ ╱ │ │
|
||
│ │ ╲─────┬─────╱ │ │
|
||
│ │ │ │ │
|
||
│ │ ┌─────┴─────┐ │ │
|
||
│ │ │ ⊥ │ NEITHER (Unknown) │ │
|
||
│ │ │ "Neither" │ No evidence either way │ │
|
||
│ │ │ │ (insufficient data) │ │
|
||
│ │ └───────────┘ │ │
|
||
│ │ │ │
|
||
│ │ │ │
|
||
│ │ Two orderings (dimensions): │ │
|
||
│ │ │ │
|
||
│ │ TRUTH ordering (vertical): INFORMATION ordering (horizontal): │ │
|
||
│ │ F < ⊥ < T < ⊤ (for meet) ⊥ < T, ⊥ < F, T < ⊤, F < ⊤ (for join) │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Value Semantics
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ VALUE SEMANTICS │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ │ │
|
||
│ │ Value │ Symbol │ Meaning │ Example in StellaOps │ │
|
||
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
|
||
│ │ True │ T │ Evidence supports "yes" │ Static analysis found │ │
|
||
│ │ │ │ │ reachable path │ │
|
||
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
|
||
│ │ False │ F │ Evidence supports "no" │ VEX says "not affected" │ │
|
||
│ │ │ │ │ │ │
|
||
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
|
||
│ │ Both │ ⊤ │ Evidence supports BOTH │ Static says reachable, │ │
|
||
│ │ │ │ "yes" AND "no" │ VEX says not affected │ │
|
||
│ │ │ │ (contradiction/conflict) │ │ │
|
||
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
|
||
│ │ Neither│ ⊥ │ No evidence either way │ No analysis run yet, │ │
|
||
│ │ │ │ (unknown/insufficient data) │ no VEX available │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ INFORMATION CONTENT │ │
|
||
│ │ │ │
|
||
│ │ ⊥ (Neither): 0 bits - we know nothing │ │
|
||
│ │ T (True): 1 bit - we know "yes" │ │
|
||
│ │ F (False): 1 bit - we know "no" │ │
|
||
│ │ ⊤ (Both): 2 bits - we know "yes" AND "no" (conflicting sources) │ │
|
||
│ │ │ │
|
||
│ │ The JOIN operation adds information (moves up in the lattice) │ │
|
||
│ │ The MEET operation requires agreement (moves down in the lattice) │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Lattice Operations
|
||
|
||
### JOIN (∨) - Combining Evidence
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ JOIN OPERATION (∨) │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ JOIN combines evidence from multiple sources. │
|
||
│ It prefers "more information" - moves UP the information ordering. │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ JOIN TRUTH TABLE │ │
|
||
│ │ │ │
|
||
│ │ ┌─────────┬─────────┬─────────┬─────────┬─────────┐ │ │
|
||
│ │ │ ∨ │ ⊥ │ T │ F │ ⊤ │ │ │
|
||
│ │ ├─────────┼─────────┼─────────┼─────────┼─────────┤ │ │
|
||
│ │ │ ⊥ │ ⊥ │ T │ F │ ⊤ │ │ │
|
||
│ │ │ T │ T │ T │ ⊤ │ ⊤ │ │ │
|
||
│ │ │ F │ F │ ⊤ │ F │ ⊤ │ │ │
|
||
│ │ │ ⊤ │ ⊤ │ ⊤ │ ⊤ │ ⊤ │ │ │
|
||
│ │ └─────────┴─────────┴─────────┴─────────┴─────────┘ │ │
|
||
│ │ │ │
|
||
│ │ Key insight: T ∨ F = ⊤ (both) │ │
|
||
│ │ When evidence conflicts, we get "Both" - we don't lose either source! │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ EXAMPLES │ │
|
||
│ │ │ │
|
||
│ │ Example 1: Adding static analysis to unknown │ │
|
||
│ │ ───────────────────────────────────────── │ │
|
||
│ │ Before: ⊥ (no information) │ │
|
||
│ │ Static analysis: T (found reachable path) │ │
|
||
│ │ Result: ⊥ ∨ T = T │ │
|
||
│ │ │ │
|
||
│ │ Example 2: Static says yes, VEX says no │ │
|
||
│ │ ──────────────────────────────────────── │ │
|
||
│ │ Static analysis: T │ │
|
||
│ │ VEX statement: F (not affected) │ │
|
||
│ │ Result: T ∨ F = ⊤ (conflict!) │ │
|
||
│ │ │ │
|
||
│ │ Example 3: Multiple sources agree │ │
|
||
│ │ ────────────────────────────────── │ │
|
||
│ │ Static analysis: T │ │
|
||
│ │ Runtime observation: T │ │
|
||
│ │ Result: T ∨ T = T │ │
|
||
│ │ │ │
|
||
│ │ Example 4: Adding information to conflict │ │
|
||
│ │ ────────────────────────────────────────── │ │
|
||
│ │ Current: ⊤ (conflicting evidence) │ │
|
||
│ │ New source: T (yes, reachable) │ │
|
||
│ │ Result: ⊤ ∨ T = ⊤ (still conflicting) │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
### MEET (∧) - Requiring Agreement
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ MEET OPERATION (∧) │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ MEET requires agreement between sources. │
|
||
│ It prefers "less information" - moves DOWN the information ordering. │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ MEET TRUTH TABLE │ │
|
||
│ │ │ │
|
||
│ │ ┌─────────┬─────────┬─────────┬─────────┬─────────┐ │ │
|
||
│ │ │ ∧ │ ⊥ │ T │ F │ ⊤ │ │ │
|
||
│ │ ├─────────┼─────────┼─────────┼─────────┼─────────┤ │ │
|
||
│ │ │ ⊥ │ ⊥ │ ⊥ │ ⊥ │ ⊥ │ │ │
|
||
│ │ │ T │ ⊥ │ T │ ⊥ │ T │ │ │
|
||
│ │ │ F │ ⊥ │ ⊥ │ F │ F │ │ │
|
||
│ │ │ ⊤ │ ⊥ │ T │ F │ ⊤ │ │ │
|
||
│ │ └─────────┴─────────┴─────────┴─────────┴─────────┘ │ │
|
||
│ │ │ │
|
||
│ │ Key insight: T ∧ F = ⊥ (unknown) │ │
|
||
│ │ When evidence disagrees, we have no consensus - result is unknown │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ EXAMPLES │ │
|
||
│ │ │ │
|
||
│ │ Example 1: Requiring both sources to confirm │ │
|
||
│ │ ───────────────────────────────────────────── │ │
|
||
│ │ Source A: T (reachable) │ │
|
||
│ │ Source B: T (reachable) │ │
|
||
│ │ Result: T ∧ T = T (confirmed by both) │ │
|
||
│ │ │ │
|
||
│ │ Example 2: One confirms, one unknown │ │
|
||
│ │ ──────────────────────────────────────── │ │
|
||
│ │ Source A: T (reachable) │ │
|
||
│ │ Source B: ⊥ (no data) │ │
|
||
│ │ Result: T ∧ ⊥ = ⊥ (can't confirm without both) │ │
|
||
│ │ │ │
|
||
│ │ Example 3: Sources disagree │ │
|
||
│ │ ───────────────────────────── │ │
|
||
│ │ Source A: T (yes) │ │
|
||
│ │ Source B: F (no) │ │
|
||
│ │ Result: T ∧ F = ⊥ (no consensus possible) │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
### NEGATION (¬)
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ NEGATION OPERATION (¬) │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ Negation flips T↔F but preserves ⊤ and ⊥ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ NEGATION TABLE │ │
|
||
│ │ │ │
|
||
│ │ ┌─────────┬─────────┐ │ │
|
||
│ │ │ x │ ¬x │ │ │
|
||
│ │ ├─────────┼─────────┤ │ │
|
||
│ │ │ ⊥ │ ⊥ │ (unknown stays unknown) │ │
|
||
│ │ │ T │ F │ (true becomes false) │ │
|
||
│ │ │ F │ T │ (false becomes true) │ │
|
||
│ │ │ ⊤ │ ⊤ │ (both stays both) │ │
|
||
│ │ └─────────┴─────────┘ │ │
|
||
│ │ │ │
|
||
│ │ Key insight: ¬⊤ = ⊤ │ │
|
||
│ │ Conflict cannot be resolved by negation - "both yes and no" negated │ │
|
||
│ │ is still "both no and yes" │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Application in Policy Engine
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ K4 IN POLICY EVALUATION │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ EVIDENCE AGGREGATION FLOW │ │
|
||
│ │ │ │
|
||
│ │ Question: "Is CVE-2021-23337 exploitable in this image?" │ │
|
||
│ │ │ │
|
||
│ │ ┌─────────────────────────────────────────────────────────────────────┐ │ │
|
||
│ │ │ Source │ Finding │ K4 Value │ │ │
|
||
│ │ │ ─────────────────────┼───────────────────┼────────────────────────│ │ │
|
||
│ │ │ Static analysis │ Path found │ T (True) │ │ │
|
||
│ │ │ Runtime observation │ Not observed │ ⊥ (Unknown) │ │ │
|
||
│ │ │ VEX (RedHat) │ Not affected │ F (False) │ │ │
|
||
│ │ │ VEX (Ubuntu) │ Not affected │ F (False) │ │ │
|
||
│ │ └─────────────────────────────────────────────────────────────────────┘ │ │
|
||
│ │ │ │
|
||
│ │ Aggregation using JOIN: │ │
|
||
│ │ │ │
|
||
│ │ Step 1: T ∨ ⊥ = T (static + runtime) │ │
|
||
│ │ Step 2: T ∨ F = ⊤ (add VEX RedHat → conflict!) │ │
|
||
│ │ Step 3: ⊤ ∨ F = ⊤ (add VEX Ubuntu → still conflict) │ │
|
||
│ │ │ │
|
||
│ │ Final K4 Value: ⊤ (Both/Conflict) │ │
|
||
│ │ │ │
|
||
│ │ Interpretation: We have conflicting evidence. Static analysis found │ │
|
||
│ │ a path, but vendors say it's not affected. This needs human review. │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ VERDICT MAPPING │ │
|
||
│ │ │ │
|
||
│ │ K4 Value │ Verdict │ Action │ │
|
||
│ │ ─────────┼──────────┼──────────────────────────────────────────────────────│ │
|
||
│ │ T (True) │ FAIL │ Evidence supports vulnerability is exploitable │ │
|
||
│ │ F (False)│ PASS │ Evidence supports vulnerability is not exploitable │ │
|
||
│ │ ⊥ (Unknown)│ WARN │ Insufficient data - conservative warning │ │
|
||
│ │ ⊤ (Both) │ REVIEW │ Conflicting evidence - requires human decision │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Policy Rule Evaluation
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ POLICY RULE EVALUATION │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ RULE STRUCTURE │ │
|
||
│ │ │ │
|
||
│ │ Policy rules are predicates that evaluate to K4 values: │ │
|
||
│ │ │ │
|
||
│ │ rule no_critical_reachable: │ │
|
||
│ │ condition: severity == CRITICAL AND reachable == TRUE │ │
|
||
│ │ action: FAIL │ │
|
||
│ │ │ │
|
||
│ │ The "AND" uses K4 meet (∧): │ │
|
||
│ │ │ │
|
||
│ │ ┌────────────────────────────────────────────────────────────────────┐ │ │
|
||
│ │ │ severity == CRITICAL │ │ │
|
||
│ │ │ │ │ │
|
||
│ │ │ If CVSS >= 9.0 → T │ │ │
|
||
│ │ │ If CVSS < 9.0 → F │ │ │
|
||
│ │ │ If CVSS unknown → ⊥ │ │ │
|
||
│ │ └────────────────────────────────────────────────────────────────────┘ │ │
|
||
│ │ │ │
|
||
│ │ ┌────────────────────────────────────────────────────────────────────┐ │ │
|
||
│ │ │ reachable == TRUE │ │ │
|
||
│ │ │ │ │ │
|
||
│ │ │ From K4 reachability evidence (as shown above) │ │ │
|
||
│ │ └────────────────────────────────────────────────────────────────────┘ │ │
|
||
│ │ │ │
|
||
│ │ Combined: severity_k4 ∧ reachable_k4 │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ EVALUATION EXAMPLES │ │
|
||
│ │ │ │
|
||
│ │ Example 1: Critical + definitely reachable │ │
|
||
│ │ ───────────────────────────────────────── │ │
|
||
│ │ severity: T (CVSS 9.8) │ │
|
||
│ │ reachable: T (static + runtime confirmed) │ │
|
||
│ │ Result: T ∧ T = T → FAIL │ │
|
||
│ │ │ │
|
||
│ │ Example 2: Critical + not reachable │ │
|
||
│ │ ──────────────────────────────────── │ │
|
||
│ │ severity: T (CVSS 9.8) │ │
|
||
│ │ reachable: F (static analysis proves no path) │ │
|
||
│ │ Result: T ∧ F = ⊥ → WARN (can't prove both conditions) │ │
|
||
│ │ │ │
|
||
│ │ Example 3: Critical + unknown reachability │ │
|
||
│ │ ─────────────────────────────────────────── │ │
|
||
│ │ severity: T (CVSS 9.8) │ │
|
||
│ │ reachable: ⊥ (no analysis done) │ │
|
||
│ │ Result: T ∧ ⊥ = ⊥ → WARN (missing reachability data) │ │
|
||
│ │ │ │
|
||
│ │ Example 4: Critical + conflicting reachability │ │
|
||
│ │ ─────────────────────────────────────────────── │ │
|
||
│ │ severity: T (CVSS 9.8) │ │
|
||
│ │ reachable: ⊤ (static says yes, VEX says no) │ │
|
||
│ │ Result: T ∧ ⊤ = T → REVIEW (conflict in reachability) │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Conflict Resolution
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────────────────────┐
|
||
│ CONFLICT RESOLUTION │
|
||
├─────────────────────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ When K4 evaluation results in ⊤ (Both/Conflict): │
|
||
│ │
|
||
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
|
||
│ │ RESOLUTION STRATEGIES │ │
|
||
│ │ │ │
|
||
│ │ 1. TRUST WEIGHTING │ │
|
||
│ │ ─────────────────── │ │
|
||
│ │ Weight sources by trust level and use weighted voting: │ │
|
||
│ │ │ │
|
||
│ │ Sources claiming T: │ │
|
||
│ │ • Static analysis (trust: 0.7) │ │
|
||
│ │ Total T weight: 0.7 │ │
|
||
│ │ │ │
|
||
│ │ Sources claiming F: │ │
|
||
│ │ • VEX RedHat (trust: 1.0) │ │
|
||
│ │ • VEX Ubuntu (trust: 1.0) │ │
|
||
│ │ Total F weight: 2.0 │ │
|
||
│ │ │ │
|
||
│ │ Resolution: F wins (2.0 > 0.7) → PASS with note │ │
|
||
│ │ │ │
|
||
│ │ 2. RECENCY PREFERENCE │ │
|
||
│ │ ───────────────────── │ │
|
||
│ │ Prefer more recent evidence: │ │
|
||
│ │ │ │
|
||
│ │ • Static analysis: 2024-12-01 → T │ │
|
||
│ │ • VEX RedHat: 2024-12-28 → F │ │
|
||
│ │ │ │
|
||
│ │ Resolution: F wins (more recent) → PASS │ │
|
||
│ │ │ │
|
||
│ │ 3. CONSERVATIVE DEFAULT │ │
|
||
│ │ ───────────────────────── │ │
|
||
│ │ When conflict cannot be resolved, default to safer option: │ │
|
||
│ │ │ │
|
||
│ │ • Conflict in reachability → assume reachable (T) │ │
|
||
│ │ • Conflict in exploitability → assume exploitable (T) │ │
|
||
│ │ │ │
|
||
│ │ 4. HUMAN ESCALATION │ │
|
||
│ │ ──────────────────── │ │
|
||
│ │ Flag for human review with all evidence: │ │
|
||
│ │ │ │
|
||
│ │ { │ │
|
||
│ │ "verdict": "REVIEW", │ │
|
||
│ │ "reason": "conflicting_evidence", │ │
|
||
│ │ "evidence": { │ │
|
||
│ │ "supporting_true": ["static_analysis"], │ │
|
||
│ │ "supporting_false": ["vex_redhat", "vex_ubuntu"] │ │
|
||
│ │ } │ │
|
||
│ │ } │ │
|
||
│ │ │ │
|
||
│ └──────────────────────────────────────────────────────────────────────────────┘ │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
---
|
||
|
||
## Implementation
|
||
|
||
```csharp
|
||
// K4 value enumeration
|
||
public enum K4Value
|
||
{
|
||
Neither = 0, // ⊥ - Unknown
|
||
True = 1, // T
|
||
False = 2, // F
|
||
Both = 3 // ⊤ - Conflict
|
||
}
|
||
|
||
// K4 lattice operations
|
||
public static class K4Lattice
|
||
{
|
||
// JOIN (∨) - combines evidence
|
||
public static K4Value Join(K4Value a, K4Value b)
|
||
{
|
||
return (K4Value)((int)a | (int)b);
|
||
}
|
||
|
||
// MEET (∧) - requires agreement
|
||
public static K4Value Meet(K4Value a, K4Value b)
|
||
{
|
||
// Special handling for the bilattice structure
|
||
if (a == K4Value.Neither || b == K4Value.Neither)
|
||
return K4Value.Neither;
|
||
if (a == b)
|
||
return a;
|
||
if (a == K4Value.Both)
|
||
return b;
|
||
if (b == K4Value.Both)
|
||
return a;
|
||
// T meet F = Neither (no consensus)
|
||
return K4Value.Neither;
|
||
}
|
||
|
||
// Negation
|
||
public static K4Value Negate(K4Value x)
|
||
{
|
||
return x switch
|
||
{
|
||
K4Value.True => K4Value.False,
|
||
K4Value.False => K4Value.True,
|
||
_ => x // Neither and Both are self-dual
|
||
};
|
||
}
|
||
|
||
// Information ordering
|
||
public static bool LessOrEqualInfo(K4Value a, K4Value b)
|
||
{
|
||
// ⊥ ≤ T, ⊥ ≤ F, T ≤ ⊤, F ≤ ⊤
|
||
if (a == K4Value.Neither) return true;
|
||
if (b == K4Value.Both) return true;
|
||
return a == b;
|
||
}
|
||
}
|
||
|
||
// Evidence aggregation
|
||
public class EvidenceAggregator
|
||
{
|
||
public K4Value AggregateEvidence(IEnumerable<EvidenceSource> sources)
|
||
{
|
||
K4Value result = K4Value.Neither; // Start with no information
|
||
|
||
foreach (var source in sources)
|
||
{
|
||
K4Value sourceValue = EvaluateSource(source);
|
||
result = K4Lattice.Join(result, sourceValue);
|
||
}
|
||
|
||
return result;
|
||
}
|
||
|
||
private K4Value EvaluateSource(EvidenceSource source)
|
||
{
|
||
return source.Type switch
|
||
{
|
||
"static_reachable" => source.Finding ? K4Value.True : K4Value.False,
|
||
"runtime_observed" => source.Finding ? K4Value.True : K4Value.Neither,
|
||
"vex_not_affected" => K4Value.False,
|
||
"vex_affected" => K4Value.True,
|
||
_ => K4Value.Neither
|
||
};
|
||
}
|
||
}
|
||
```
|
||
|
||
---
|
||
|
||
## Related Documentation
|
||
|
||
- [Policy Engine Data Pipeline](policy-engine-data-pipeline.md) - Complete data flow
|
||
- [Confidence Scoring](confidence-scoring.md) - Weighted evidence scoring
|
||
- [Policy Evaluation Flow](../../flows/04-policy-evaluation-flow.md) - End-to-end flow
|
||
- [Reachability Analysis](call-graph-analysis.md) - 8-state reachability lattice
|