Develop

.github/workflows/formal.yml

@@ -3,8 +3,8 @@ name: Formal
 on: [push, pull_request]
 
 jobs:
-  acl-model:
-    name: Build the Lean ACL model and check it tracks the code
+  models:
+    name: Build the Lean models and check they track the code
     runs-on: ubuntu-latest
     steps:
       - name: Install Linux packages
@@ -13,21 +13,32 @@ jobs:
         uses: actions/checkout@v7
         with:
           fetch-depth: 0
-      # elan picks the toolchain pinned in formal/acl/lean-toolchain on first use
+      # elan picks the toolchain pinned in each model's lean-toolchain on first use
       - name: Install elan
         run: |
           curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Build the model
+      - name: Build the graph store model
+        working-directory: formal/http
+        run: lake build
+      # the ACL model requires the graph store's, by path
+      - name: Build the ACL model
         working-directory: formal/acl
         run: lake build
-      # lake build only warns on sorry; the README's "no sorry" claim is checked here
+      # GraphVersioningServiceTest replays these cases against the Java TimeGate; here they are checked against the model
+      - name: The TimeGate cases are the model's
+        run: |
+          formal/http/.lake/build/bin/ldh-http --select-cases > /tmp/memento-cases.tsv
+          diff -u src/test/resources/com/atomgraph/linkeddatahub/server/util/memento-cases.tsv /tmp/memento-cases.tsv
+      # lake build only warns on sorry; the READMEs' "no sorry" claim is checked here
       - name: Every theorem is proven
         run: |
-          if grep -rnw --include='*.lean' sorry formal/acl; then
-            echo "::error::formal/acl has unproven theorems"
+          if grep -rnw --include='*.lean' --exclude-dir=.lake sorry formal; then
+            echo "::error::formal/ has unproven theorems"
             exit 1
           fi
-      - name: The model tracks the code
+      - name: The models track the code
         if: github.event_name == 'pull_request'
-        run: formal/acl/tracks-code.sh "${{ github.event.pull_request.base.sha }}"
+        run: |
+          formal/http/tracks-code.sh "${{ github.event.pull_request.base.sha }}"
+          formal/acl/tracks-code.sh "${{ github.event.pull_request.base.sha }}"

.github/workflows/http-tests.yml

@@ -51,7 +51,8 @@ jobs:
         working-directory: cli
       - name: Add the ldh launcher to PATH
         run: echo "$GITHUB_WORKSPACE/cli/bin" >> "$GITHUB_PATH"
-      # the formal suite replays the Lean model's decision (formal/acl) against the server through ldh-acl;
+      # the formal suite replays the Lean models (formal/acl over formal/http) against the server through ldh-acl,
+      # and the versioning suite the Memento model through ldh-http;
       # elan picks the toolchain pinned in formal/acl/lean-toolchain
       - name: Install elan
         run: |
@@ -60,6 +61,10 @@ jobs:
       - name: Build ldh-acl
         run: lake build ldh-acl
         working-directory: formal/acl
+      # the versioning suite replays the Memento model's TimeGate and TimeMap through ldh-http
+      - name: Build ldh-http
+        run: lake build ldh-http
+        working-directory: formal/http
       - name: Generating server certificate
         run: |
           server-cert-gen.sh .env nginx ssl

README.md

@@ -368,6 +368,17 @@ LinkedDataHub includes an HTTP [test suite](https://github.com/AtomGraph/LinkedD
 
 ![HTTP-tests](https://github.com/AtomGraph/LinkedDataHub/actions/workflows/http-tests.yml/badge.svg)
 
+## Formal verification
+
+The parts of LinkedDataHub whose failure is a security incident are specified in [Lean 4](https://lean-lang.org/), with machine-checked proofs of what the server guarantees:
+
+* [graph store](formal/http/): its answer to every request, and the invariants every write keeps, covering the document hierarchy, types limited to the hierarchy classes, and ownership. A write guarded by `If-Match` loses no update, and the Memento TimeGate selects the version closest to the requested datetime
+* [access control](formal/acl/): the authorization decision in front of the graph store. A denied request answers `403` and reveals nothing else, not even whether the document exists. A write to an end-user document changes no authorization over any other document, and an authorization scoped to end-user documents opens no admin document
+
+The models are transcribed from the code, not extracted from it. The `Formal` workflow builds them on every push, fails on an unproven theorem, and fails a pull request that changes a transcribed source without changing the model. The HTTP test suite replays the models' answers against a running server, comparing the status and the document's graph after each request. See [`formal/README.md`](formal/README.md) for the roadmap.
+
+![Formal](https://github.com/AtomGraph/LinkedDataHub/actions/workflows/formal.yml/badge.svg)
+
 ## Dependencies
 
 ### Browser

cli/pom.xml

@@ -4,7 +4,7 @@
 
     <groupId>com.atomgraph</groupId>
     <artifactId>linkeddatahub-cli</artifactId>
-    <version>6.3.0</version>
+    <version>6.3.1-SNAPSHOT</version>
     <packaging>jar</packaging>
 
     <name>LinkedDataHub CLI</name>

formal/README.md

@@ -5,12 +5,16 @@ model lives in its own directory with its own toolchain, README and mapping to t
 
 | Directory | Tool | Covers |
 |-----------|------|--------|
-| [`acl/`](acl/) | Lean 4 | The authorization decision, the graph store writes that change what it reads, and the 6.0 migration of seeded authorizations |
+| [`http/`](http/) | Lean 4 | The graph store: its documents, its writes and the invariants they keep, and its answer to every request |
+| [`acl/`](acl/) | Lean 4 | The authorization decision over the graph store's data, the server's answer with the decision in front of the graph store, and the 6.0 migration of seeded authorizations |
+
+The graph store model stands alone; the ACL model requires it, by path, since the decision reads the graph store's
+data and its theorems about writes are about the graph store's writes.
 
 The `Formal` workflow (`.github/workflows/formal.yml`) builds every model on each push, fails on an
 unproven theorem, and on a pull request fails when a transcribed source changes without the model
-(`acl/tracks-code.sh`). The HTTP test suite replays the ACL model's decision against the server
-(`tests/http/formal/`).
+(`http/tracks-code.sh`, `acl/tracks-code.sh`). The HTTP test suite replays the models' answers against the server:
+the status and the document's graph after each request (`tests/http/formal/`).
 
 ## Why
 
@@ -28,7 +32,7 @@ about the authorization decision, which is the part already modelled.
 ## Roadmap
 
 Each step is independent of the ones after it. The first three are the cheapest and buy most of the
-credibility; the fourth is the one that answers the agent-era question and changes the product.
+credibility; the fifth is the one that answers the agent-era question and changes the product.
 
 1. **The model is a build artifact.** Done in this directory's `Formal` workflow: `lake build`, a
    `sorry` check and the drift check. The README mapping stops being a promise kept by hand.
@@ -40,29 +44,44 @@ credibility; the fourth is the one that answers the agent-era question and chang
    before every request. Verifying the Java directly is not worth the cost; this is how the proofs
    constrain the code.
 
-3. **Every hypothesis of a theorem is an enforced constraint.** `AdminTyped`, `Typed`, `Site.Finite`
-   and `Reader.Expressive` (see `acl/README.md`, "What the proofs need of the data") are premises an
-   attacker can try to falsify. Each gets a server-side check and a negative HTTP test.
-
-4. **Delegation as non-interference.** Model `On-Behalf-Of` and `acl:delegates`, and prove that for
+3. **Every hypothesis of a theorem is an enforced constraint.** Done: of the premises in `acl/README.md`,
+   "What the proofs need of the data", the two a request can falsify, `AdminTyped` and `Typed`, are kept by
+   a type rule on every write (`checkDocumentTypes`), proven preserved by `Step.adminTyped` and `Step.typed`,
+   and tried by negative HTTP tests. `Site.Finite` and `Reader.Expressive` are facts about URIs and the
+   query, with nothing to falsify.
+
+4. **The graph store's answer is modelled, and the server is replayed against it.** Done: the graph store
+   is a model of its own, `http/`, which the ACL model now requires. `http/LdhHttp/Answer.lean` gives every
+   status a graph store request can get and the store after it, as a program, and proves that a refused
+   request changes nothing and that a request that goes through is a `Write`, so the graph store keeps
+   every invariant a `Write` does. `acl/LdhAcl/Gate.lean` puts the decision in front of it and proves that
+   `403` is the decision's alone (a denied agent learns nothing else, not even whether the document
+   exists) and that what goes through is an authorized `Write`. The replay checks the server's status and
+   the document's graph after each request against it. `ETag.lean` proves that a write guarded by
+   `If-Match` loses no update, on the assumption that the tag's digest is collision-free. `Memento.lean`
+   models the TimeGate (the closest commit, the more recent of two as close), the TimeMap and the commit
+   queue, and the TimeGate is replayed against the Java on generated histories and against the server on a
+   versioned dataspace.
+
+5. **Delegation as non-interference.** Model `On-Behalf-Of` and `acl:delegates`, and prove that for
    any plan an LLM emits, the requests the secretary can execute on behalf of a caller are exactly those
    the caller could execute alone, independently of prompt content. That reduces prompt injection to
    misuse within existing rights, and motivates scoping `acl:delegates`, which today delegates
    everything. Scoped delegation is the one design change this roadmap expects to force.
 
-5. **Concurrency in its own model.** The lock protocol (a `PUT` holds its parent's lock and re-checks
+6. **Concurrency in its own model.** The lock protocol (a `PUT` holds its parent's lock and re-checks
    the parent exists, a `DELETE` checks for children) is a TLA+ problem: a small model and TLC, in a
    sibling directory. Lean is the wrong tool for it.
 
-6. **Chokepoints checked by structure.** The input-handling class is closed by `SecureXML` and
+7. **Chokepoints checked by structure.** The input-handling class is closed by `SecureXML` and
    `URLValidator` being the only paths to a parser or an outbound connection. Architecture tests that
    forbid raw XML parser factories, URL opening and SPARQL string concatenation outside those classes
    turn that from a convention into a build failure.
 
-7. **The claims are published.** A threat model page in the wiki, a `SECURITY.md` stating what is
+8. **The claims are published.** A threat model page in the wiki, a `SECURITY.md` stating what is
    proven and under which hypotheses, and the model handed to the next penetration retest as its oracle.
 
 ## Not in scope
 
-Authentication (WebID, OAuth, delegation until step 4), content negotiation, caching, imports, uploads,
+Authentication (WebID, OAuth, delegation until step 5), content negotiation, caching, imports, uploads,
 XSLT and the client. Each is a candidate for its own model once the ones above hold.

formal/acl/LdhAcl.lean

@@ -1,6 +1,6 @@
-import LdhAcl.Base
 import LdhAcl.Model
 import LdhAcl.Step
 import LdhAcl.Theorems
 import LdhAcl.Migration
 import LdhAcl.Decide
+import LdhAcl.Gate

formal/acl/LdhAcl/Decide.lean

@@ -7,131 +7,7 @@ import LdhAcl.Theorems
 
 namespace LdhAcl
 
-/-! ## Finite data -/
-
-/-- A store as data: a document's graph as the list of its triples. A document listed more than once has the
-union of its lists. -/
-abbrev FinStore := List (Node × List Triple)
-
-/-- The graph store's notion of existence, computed. -/
-def hasDoc (fs : FinStore) (d : Node) : Bool := fs.any (·.1 == d)
-
-/-- The triples of a document's own graph. -/
-def graphOf (fs : FinStore) (d : Node) : List Triple :=
-  fs.foldr (fun p acc => if p.1 = d then p.2 ++ acc else acc) []
-
-/-- The abstract store the data denotes. -/
-def FinStore.toStore (fs : FinStore) : Store :=
-  fun d => if hasDoc fs d then some (fun t => t ∈ graphOf fs d) else none
-
-theorem hasDoc_iff {fs : FinStore} {d : Node} : hasDoc fs d = true ↔ ∃ ts, (d, ts) ∈ fs := by
-  simp only [hasDoc, List.any_eq_true, beq_iff_eq]
-  constructor
-  · rintro ⟨⟨d', ts⟩, h, rfl⟩
-    exact ⟨ts, h⟩
-  · rintro ⟨ts, h⟩
-    exact ⟨(d, ts), h, rfl⟩
-
-theorem graphOf_cons {p : Node × List Triple} {fs : FinStore} {d : Node} :
-    graphOf (p :: fs) d = if p.1 = d then p.2 ++ graphOf fs d else graphOf fs d := rfl
-
-theorem mem_graphOf {fs : FinStore} {d : Node} {t : Triple} :
-    t ∈ graphOf fs d ↔ ∃ ts, (d, ts) ∈ fs ∧ t ∈ ts := by
-  induction fs with
-  | nil => simp [graphOf]
-  | cons p fs ih =>
-    obtain ⟨p1, p2⟩ := p
-    rw [graphOf_cons]
-    by_cases h : p1 = d
-    · subst h
-      simp only [if_true, List.mem_append, ih, List.mem_cons]
-      constructor
-      · rintro (ht | ⟨ts, hts, ht⟩)
-        · exact ⟨p2, Or.inl rfl, ht⟩
-        · exact ⟨ts, Or.inr hts, ht⟩
-      · rintro ⟨ts, hts | hts, ht⟩
-        · cases hts; exact Or.inl ht
-        · exact Or.inr ⟨ts, hts, ht⟩
-    · simp only [h, if_false, ih, List.mem_cons]
-      constructor
-      · rintro ⟨ts, hts, ht⟩
-        exact ⟨ts, Or.inr hts, ht⟩
-      · rintro ⟨ts, hts | hts, ht⟩
-        · cases hts; exact absurd rfl h
-        · exact ⟨ts, hts, ht⟩
-
-theorem hasDoc_of_mem_graphOf {fs : FinStore} {d : Node} {t : Triple} (h : t ∈ graphOf fs d) :
-    hasDoc fs d = true := by
-  obtain ⟨ts, hm, _⟩ := mem_graphOf.1 h
-  exact hasDoc_iff.2 ⟨ts, hm⟩
-
-theorem toStore_of_hasDoc {fs : FinStore} {d : Node} (h : hasDoc fs d = true) :
-    fs.toStore d = some (fun t => t ∈ graphOf fs d) := by
-  simp [FinStore.toStore, h]
-
-theorem toStore_of_not_hasDoc {fs : FinStore} {d : Node} (h : ¬ hasDoc fs d = true) :
-    fs.toStore d = none := by
-  simp [FinStore.toStore, h]
-
-theorem present_iff {fs : FinStore} {d : Node} : present fs.toStore d ↔ hasDoc fs d = true := by
-  constructor
-  · rintro ⟨g, hg⟩
-    unfold FinStore.toStore at hg
-    split at hg
-    · assumption
-    · cases hg
-  · intro h
-    exact ⟨_, toStore_of_hasDoc h⟩
-
-/-- A triple of a document's own graph. -/
-theorem own_iff {fs : FinStore} {d : Node} {t : Triple} :
-    (∃ g, fs.toStore d = some g ∧ g t) ↔ t ∈ graphOf fs d := by
-  constructor
-  · rintro ⟨g, hg, ht⟩
-    by_cases h : hasDoc fs d = true
-    · rw [toStore_of_hasDoc h] at hg
-      cases hg
-      exact ht
-    · rw [toStore_of_not_hasDoc h] at hg
-      cases hg
-  · intro ht
-    exact ⟨_, toStore_of_hasDoc (hasDoc_of_mem_graphOf ht), ht⟩
-
-theorem ownTypes_iff {fs : FinStore} {x t : Node} :
-    ownTypes fs.toStore x t ↔ ⟨x, .rdfType, t⟩ ∈ graphOf fs x := own_iff
-
-theorem owner_iff {fs : FinStore} {x a : Node} :
-    owner fs.toStore x a ↔ ⟨x, .aclOwner, a⟩ ∈ graphOf fs x := own_iff
-
-/-- The objects of a document's own `rdf:type` triples. -/
-def typesOf (fs : FinStore) (x : Node) : List Node :=
-  (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .rdfType then some t.o else none
-
-/-- The objects of a document's own `acl:owner` triples. -/
-def ownersOf (fs : FinStore) (x : Node) : List Node :=
-  (graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = .aclOwner then some t.o else none
-
-theorem mem_filterMap_prop {fs : FinStore} {x p o : Node} :
-    o ∈ ((graphOf fs x).filterMap fun t => if t.s = x ∧ t.p = p then some t.o else none) ↔
-      ⟨x, p, o⟩ ∈ graphOf fs x := by
-  simp only [List.mem_filterMap]
-  constructor
-  · rintro ⟨⟨s, p', o'⟩, ht, h⟩
-    simp only at h
-    split at h
-    · rename_i hsp
-      cases h
-      obtain ⟨rfl, rfl⟩ := hsp
-      exact ht
-    · cases h
-  · intro h
-    exact ⟨_, h, by simp⟩
-
-theorem mem_typesOf {fs : FinStore} {x t : Node} : t ∈ typesOf fs x ↔ ownTypes fs.toStore x t :=
-  mem_filterMap_prop.trans ownTypes_iff.symm
-
-theorem mem_ownersOf {fs : FinStore} {x a : Node} : a ∈ ownersOf fs x ↔ owner fs.toStore x a :=
-  mem_filterMap_prop.trans owner_iff.symm
+open LdhHttp
 
 /-! ## Containment, as edges -/
 
@@ -277,8 +153,7 @@ def FinAdmin.reader (fa : FinAdmin) : Reader where
   sub_refl := fun _ => Or.inl rfl
 
 /-- The deployment constants, computed. -/
-structure FinSite where
-  parent : Node → Node
+structure FinSite extends HSite where
   admin : Node → Bool
 
 def FinSite.agrees (fsite : FinSite) (site : Site) : Prop :=