diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md index e08eac7..2fa8c4c 100644 --- a/PROOF-NEEDS.md +++ b/PROOF-NEEDS.md @@ -94,25 +94,38 @@ These encode computational hardness assumptions unprovable in any formal system. | `tamperEvidence` | Theorems.idr | sha256CollisionResistant + signatureNonReplayable + list concat non-injectivity | | `replayPrevention` | Theorems.idr | signatureNonReplayable (different record type) | -### String Primitive Limitations (6) — INFRASTRUCTURE BUILT - -`isPrefixOf` and `isInfixOf` are C primitives with no reduction rules. Proven List Char equivalents exist in `StringLemmas.idr` (`charsPrefixOf`, `charsInfixOf`, `charsPrefixOfAppend`). To eliminate these postulates, add a bridge postulate connecting String operations to their List Char equivalents. - -| Postulate | File | Proven equivalent in StringLemmas.idr | -|-----------|------|--------------------------------------| -| `extractionSafety` | ImporterProofs.idr | `charsPrefixOfAppend` | -| `symlinkSafety` | ImporterProofs.idr | `charsPrefixOfAppend` | -| `zipSlipPrevention` | ImporterProofs.idr | `charsPrefixOfAppend` | -| `normalizedIsSafe` | ImporterProofs.idr | `dotDotNotInfix` (partial) | -| `absolutePathRejection` | ImporterProofs.idr | Needs SafePath definition over List Char | -| `ociLayoutEnforcement` | ImporterProofs.idr | Needs DecEq on TarEntry paths | - -### Path to eliminating String postulates - -1. Add bridge postulate: `isPrefixOf s1 s2 = charsPrefixOf (unpack s1) (unpack s2)` (1 postulate) -2. Prove `unpack` distributes over `++`: `unpack (a ++ b) = unpack a ++ unpack b` (may need 1 more postulate) -3. Derive extractionSafety, symlinkSafety, zipSlipPrevention from bridge + `charsPrefixOfAppend` -4. Net: 3 postulates → 1-2 bridge postulates (improvement) +### String Primitive Limitations — 3 of 6 ELIMINATED 2026-05-18 + +`isPrefixOf` is a C primitive with no reduction rules. The bridge is now +in place (`StringLemmas.idr`): two minimal documented axioms +`isPrefixOfBridge` (`isPrefixOf s1 s2 = charsPrefixOf (unpack s1) +(unpack s2)`) and `unpackAppend` (`unpack (a ++ b) = unpack a ++ unpack +b`). Via these + the already-proven `charsPrefixOfAppend`, three +postulates are now **real proofs** (full `cerro-torre.ipkg` green under +idris2 0.8.0). Net: 3 ad-hoc string postulates → 2 fundamental, +well-understood ones (same justified category as estate backend +string-primitive axioms, e.g. boj-server SafetyLemmas). + +| Postulate | File | Status | +|-----------|------|--------| +| `extractionSafety` | ImporterProofs.idr | **PROVEN** (isPrefixOfBridge + unpackAppend + charsPrefixOfAppend) | +| `symlinkSafety` | ImporterProofs.idr | **PROVEN** (idem) | +| `zipSlipPrevention` | ImporterProofs.idr | **PROVEN** (idem) | +| `normalizedIsSafe` | ImporterProofs.idr | postulate — needs `dotDotNotInfix` + infix bridge | +| `absolutePathRejection` | ImporterProofs.idr | postulate — needs SafePath over List Char | +| `ociLayoutEnforcement` | ImporterProofs.idr | postulate — needs DecEq on TarEntry paths | + +Remaining bridge axioms (minimal trusted base): `isPrefixOfBridge`, +`unpackAppend` in `StringLemmas.idr`. + +### Path to eliminating remaining String postulates + +1. ~~Add `isPrefixOfBridge` + `unpackAppend`~~ — DONE 2026-05-18. +2. ~~Derive extractionSafety / symlinkSafety / zipSlipPrevention~~ — DONE. +3. `normalizedIsSafe`: add an `isInfixOf` bridge analogous to + `isPrefixOfBridge`, then derive from `dotDotNotInfix`. +4. `absolutePathRejection`: define `SafePath` semantics over `List Char`. +5. `ociLayoutEnforcement`: add `DecEq` on `TarEntry` paths. ## assert_total Usage (2) — ACCEPTABLE diff --git a/container-stack/cerro-torre/verification/idris/ImporterProofs.idr b/container-stack/cerro-torre/verification/idris/ImporterProofs.idr index ed470b6..3b041ff 100644 --- a/container-stack/cerro-torre/verification/idris/ImporterProofs.idr +++ b/container-stack/cerro-torre/verification/idris/ImporterProofs.idr @@ -19,6 +19,7 @@ import Data.List import Data.List1 import Data.Nat import Decidable.Equality +import StringLemmas %default total @@ -160,7 +161,10 @@ extractionSafety : (root : Path) -> (entry : TarEntry) -> SafePath (entry.path) -> isPrefixOf root (root ++ "/" ++ entry.path) = True -extractionSafety _ _ _ = idris_crash "extractionSafety: string-primitive postulate — type-level use only" +extractionSafety root entry _ = + rewrite isPrefixOfBridge root (root ++ "/" ++ entry.path) in + rewrite unpackAppend root ("/" ++ entry.path) in + charsPrefixOfAppend (unpack root) (unpack ("/" ++ entry.path)) ||| POSTULATE: Symlink Safety ||| @@ -178,7 +182,10 @@ symlinkSafety : (root : Path) -> entry.symlinkTarget = Just target -> SafePath target -> isPrefixOf root (root ++ "/" ++ target) = True -symlinkSafety _ _ _ _ _ _ = idris_crash "symlinkSafety: string-primitive postulate — type-level use only" +symlinkSafety root _ target _ _ _ = + rewrite isPrefixOfBridge root (root ++ "/" ++ target) in + rewrite unpackAppend root ("/" ++ target) in + charsPrefixOfAppend (unpack root) (unpack ("/" ++ target)) ||| POSTULATE: Absolute Path Rejection ||| @@ -278,4 +285,7 @@ zipSlipPrevention : (root : Path) -> (entry : TarEntry) -> SafePath (normalizePath entry.path) -> isPrefixOf root (root ++ "/" ++ normalizePath entry.path) = True -zipSlipPrevention _ _ _ = idris_crash "zipSlipPrevention: string-primitive postulate — type-level use only" +zipSlipPrevention root entry _ = + rewrite isPrefixOfBridge root (root ++ "/" ++ normalizePath entry.path) in + rewrite unpackAppend root ("/" ++ normalizePath entry.path) in + charsPrefixOfAppend (unpack root) (unpack ("/" ++ normalizePath entry.path)) diff --git a/container-stack/cerro-torre/verification/idris/StringLemmas.idr b/container-stack/cerro-torre/verification/idris/StringLemmas.idr index 70c04f6..9d3db02 100644 --- a/container-stack/cerro-torre/verification/idris/StringLemmas.idr +++ b/container-stack/cerro-torre/verification/idris/StringLemmas.idr @@ -14,6 +14,7 @@ module StringLemmas +import Data.String import Data.List import Decidable.Equality @@ -74,3 +75,39 @@ dotDotNotInfix : (xs : List Char) -> charsInfixOf ['.', '.'] xs = False -> Not (charsInfixOf ['.', '.'] xs = True) dotDotNotInfix xs prf contra = absurd (trans (sym prf) contra) + +-- ============================================================================ +-- Bridge Axioms (string-primitive postulates) +-- ============================================================================ +-- +-- These two are the *minimal* trusted base connecting Idris2's opaque C +-- String primitives to the proven List-Char operations above. They are +-- the same justified category as backend string-primitive axioms +-- elsewhere in the estate (cf. boj-server SafetyLemmas charEqSound/ +-- unpackLength): not provable in Idris2 (no reduction rules for the C +-- prims), minimal, isolated, documented. Per the repo idiom (Idris2 0.8 +-- has no `postulate` keyword) they are `partial`+`idris_crash` stubs. +-- +-- NET EFFECT: they let ImporterProofs.idr discharge `extractionSafety`, +-- `symlinkSafety`, `zipSlipPrevention` with real proofs — replacing 3 +-- ad-hoc string postulates with 2 fundamental, well-understood ones. + +||| BRIDGE AXIOM: String.isPrefixOf agrees with the proven List-Char +||| `charsPrefixOf` under `unpack`. `isPrefixOf` is a C primitive with +||| no reduction rules; this equivalence is a backend-semantics fact. +partial +public export +isPrefixOfBridge : (s1, s2 : String) + -> isPrefixOf s1 s2 = charsPrefixOf (unpack s1) (unpack s2) +isPrefixOfBridge _ _ = + idris_crash "isPrefixOfBridge: string-primitive axiom — type-level use only" + +||| BRIDGE AXIOM: `unpack` distributes over String `++`. Backend +||| primitive guarantee (`prim__strAppend` / `prim__strToCharList`), +||| not reducible at the Idris2 type level. +partial +public export +unpackAppend : (a, b : String) + -> unpack (a ++ b) = unpack a ++ unpack b +unpackAppend _ _ = + idris_crash "unpackAppend: string-primitive axiom — type-level use only"