From 2b3811e7ea891e123832105968e3ae3bfad34515 Mon Sep 17 00:00:00 2001 From: chasebryan Date: Tue, 7 Jul 2026 17:25:37 -0500 Subject: [PATCH] Add SEAL-Core v0 proof matrix --- Makefile | 2 +- README.md | 4 + docs/ARCHITECTURE.md | 9 ++ scripts/verify-core.sh | 3 +- src/Seal.Matrix.fst | 252 +++++++++++++++++++++++++++++++++++++++++ 5 files changed, 268 insertions(+), 2 deletions(-) create mode 100644 src/Seal.Matrix.fst diff --git a/Makefile b/Makefile index 57852f9..b3a26af 100644 --- a/Makefile +++ b/Makefile @@ -1,4 +1,4 @@ -CORE_MODULES := src/Seal.Types.fst src/Seal.Policy.fst src/Seal.Gate.fst src/Seal.Proofs.fst +CORE_MODULES := src/Seal.Types.fst src/Seal.Policy.fst src/Seal.Gate.fst src/Seal.Proofs.fst src/Seal.Matrix.fst .PHONY: toolchain verify extract test clean diff --git a/README.md b/README.md index 5d40ecc..190aa80 100644 --- a/README.md +++ b/README.md @@ -38,6 +38,10 @@ The v0 model has no parser. Files in `examples/` are documentation fixtures only `make extract` is non-fatal in v0. It reports `SEAL_EXTRACTION_NOT_READY` when `krml` is unavailable or the model is not ready for extraction. +## Proof Matrix + +`src/Seal.Matrix.fst` encodes explicit v0 decision cases for measure, open, seal, and transition operations. It proves capability checks dominate evidence and receipt checks, evidence checks dominate receipt checks where evidence is required, and disallowed state combinations cannot return `Allow`. + ## Non-Claims SEAL-Core v0 is: diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 244c352..f81361e 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -21,4 +21,13 @@ The F* model is intentionally direct. `Seal.Policy` defines the operation requir 3. missing receipt denies before allow 4. allow is returned only after all required conditions are present +Decision-order matrix: + +| Operation | Required capability | Evidence required | Receipt required | Allow condition | +| --- | --- | --- | --- | --- | +| `OpMeasure` | `CapMeasure` | no | no | capability present | +| `OpOpen` | `CapOpen` | yes | no | capability present and evidence valid | +| `OpSeal` | `CapSeal` | yes | no | capability present and evidence valid | +| `OpTransition` | `CapTransition` | yes | yes | capability present, evidence valid, and receipt valid | + There is no parser, no network path, no daemon, no plugin system, no package manager, and no seL4 integration in v0. diff --git a/scripts/verify-core.sh b/scripts/verify-core.sh index fd6bc67..084d4ea 100755 --- a/scripts/verify-core.sh +++ b/scripts/verify-core.sh @@ -30,6 +30,7 @@ fstar.exe \ src/Seal.Types.fst \ src/Seal.Policy.fst \ src/Seal.Gate.fst \ - src/Seal.Proofs.fst + src/Seal.Proofs.fst \ + src/Seal.Matrix.fst echo "SEAL_CORE_VERIFIED" diff --git a/src/Seal.Matrix.fst b/src/Seal.Matrix.fst new file mode 100644 index 0000000..ce7c3da --- /dev/null +++ b/src/Seal.Matrix.fst @@ -0,0 +1,252 @@ +module Seal.Matrix + +open Seal.Types +open Seal.Policy +open Seal.Gate + +let is_allow (decision:decision) : Tot bool = + match decision with + | Allow -> true + | DenyMissingCapability -> false + | DenyMissingEvidence -> false + | DenyMissingReceipt -> false + +let measure_missing_capability_denies + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapMeasure == false)) + (ensures (gate sub OpMeasure caps evidence receipt == DenyMissingCapability)) + = () + +let measure_capability_allows + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapMeasure == true)) + (ensures (gate sub OpMeasure caps evidence receipt == Allow)) + = () + +let measure_evidence_irrelevant + (sub:subject) + (caps:policy) + (left:evidence_state) + (right:evidence_state) + (receipt:receipt_state) + : Lemma + (ensures (gate sub OpMeasure caps left receipt == gate sub OpMeasure caps right receipt)) + = + if has_cap caps CapMeasure then () else () + +let measure_receipt_irrelevant + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (left:receipt_state) + (right:receipt_state) + : Lemma + (ensures (gate sub OpMeasure caps evidence left == gate sub OpMeasure caps evidence right)) + = + if has_cap caps CapMeasure then () else () + +let open_missing_capability_denies + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapOpen == false)) + (ensures (gate sub OpOpen caps evidence receipt == DenyMissingCapability)) + = () + +let open_missing_evidence_denies + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapOpen == true)) + (ensures (gate sub OpOpen caps EvidenceMissing receipt == DenyMissingEvidence)) + = () + +let open_valid_evidence_allows + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapOpen == true)) + (ensures (gate sub OpOpen caps EvidenceValid receipt == Allow)) + = () + +let open_receipt_irrelevant + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (left:receipt_state) + (right:receipt_state) + : Lemma + (ensures (gate sub OpOpen caps evidence left == gate sub OpOpen caps evidence right)) + = + if has_cap caps CapOpen then + match evidence with + | EvidenceMissing -> () + | EvidenceValid -> () + else + () + +let seal_missing_capability_denies + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapSeal == false)) + (ensures (gate sub OpSeal caps evidence receipt == DenyMissingCapability)) + = () + +let seal_missing_evidence_denies + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapSeal == true)) + (ensures (gate sub OpSeal caps EvidenceMissing receipt == DenyMissingEvidence)) + = () + +let seal_valid_evidence_allows + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapSeal == true)) + (ensures (gate sub OpSeal caps EvidenceValid receipt == Allow)) + = () + +let seal_receipt_irrelevant + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (left:receipt_state) + (right:receipt_state) + : Lemma + (ensures (gate sub OpSeal caps evidence left == gate sub OpSeal caps evidence right)) + = + if has_cap caps CapSeal then + match evidence with + | EvidenceMissing -> () + | EvidenceValid -> () + else + () + +let transition_missing_capability_denies + (sub:subject) + (caps:policy) + (evidence:evidence_state) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapTransition == false)) + (ensures (gate sub OpTransition caps evidence receipt == DenyMissingCapability)) + = () + +let transition_missing_evidence_denies + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps CapTransition == true)) + (ensures (gate sub OpTransition caps EvidenceMissing receipt == DenyMissingEvidence)) + = () + +let transition_missing_receipt_denies + (sub:subject) + (caps:policy) + : Lemma + (requires (has_cap caps CapTransition == true)) + (ensures (gate sub OpTransition caps EvidenceValid ReceiptMissing == DenyMissingReceipt)) + = () + +let transition_valid_evidence_and_receipt_allows + (sub:subject) + (caps:policy) + : Lemma + (requires (has_cap caps CapTransition == true)) + (ensures (gate sub OpTransition caps EvidenceValid ReceiptValid == Allow)) + = () + +let missing_capability_dominates_missing_evidence + (sub:subject) + (op:operation) + (caps:policy) + (receipt:receipt_state) + : Lemma + (requires (has_cap caps (required_capability op) == false)) + (ensures (gate sub op caps EvidenceMissing receipt == DenyMissingCapability)) + = () + +let missing_capability_dominates_missing_receipt + (sub:subject) + (op:operation) + (caps:policy) + (evidence:evidence_state) + : Lemma + (requires (has_cap caps (required_capability op) == false)) + (ensures (gate sub op caps evidence ReceiptMissing == DenyMissingCapability)) + = () + +let missing_evidence_dominates_missing_receipt_when_evidence_required + (sub:subject) + (op:operation) + (caps:policy) + : Lemma + (requires ((has_cap caps (required_capability op) == true) /\ (op_requires_evidence op == true))) + (ensures (gate sub op caps EvidenceMissing ReceiptMissing == DenyMissingEvidence)) + = + match op with + | OpMeasure -> () + | OpOpen -> () + | OpSeal -> () + | OpTransition -> () + +let allow_impossible_for_open_without_evidence_valid + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (ensures (is_allow (gate sub OpOpen caps EvidenceMissing receipt) == false)) + = + if has_cap caps CapOpen then () else () + +let allow_impossible_for_seal_without_evidence_valid + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (ensures (is_allow (gate sub OpSeal caps EvidenceMissing receipt) == false)) + = + if has_cap caps CapSeal then () else () + +let allow_impossible_for_transition_without_evidence_valid + (sub:subject) + (caps:policy) + (receipt:receipt_state) + : Lemma + (ensures (is_allow (gate sub OpTransition caps EvidenceMissing receipt) == false)) + = + if has_cap caps CapTransition then () else () + +let allow_impossible_for_transition_without_receipt_valid + (sub:subject) + (caps:policy) + (evidence:evidence_state) + : Lemma + (ensures (is_allow (gate sub OpTransition caps evidence ReceiptMissing) == false)) + = + if has_cap caps CapTransition then + match evidence with + | EvidenceMissing -> () + | EvidenceValid -> () + else + ()