Model entity tags and Memento in the graph store model

.github/workflows/formal.yml

@@ -25,6 +25,11 @@ jobs:
       - name: Build the ACL model
         working-directory: formal/acl
         run: lake build
+      # 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: |

.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 models (formal/acl over formal/http) 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

formal/README.md

@@ -57,9 +57,11 @@ credibility; the fifth is the one that answers the agent-era question and change
    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. Next on the graph store model: entity tags, to
-   prove that a write guarded by `If-Match` changes only the version it quoted, and Memento's TimeGate and
-   TimeMap.
+   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

formal/http/LdhHttp.lean

@@ -2,4 +2,6 @@ import LdhHttp.Base
 import LdhHttp.Write
 import LdhHttp.Fin
 import LdhHttp.Answer
+import LdhHttp.ETag
+import LdhHttp.Memento
 import LdhHttp.IO

formal/http/LdhHttp/ETag.lean

@@ -0,0 +1,94 @@
+/-
+Entity tags, and what a write guarded by one guarantees.
+
+`EntityTags.entityTag` digests the document's URI and its graph as sorted N-Triples with SHA-256, keeps 128 bits,
+and folds in the negotiated variant. The model takes one variant, as the replay negotiates N-Triples throughout, and
+the tag as a function of the document and its graph with two properties: it is the graph's, so the order and
+repetition of triples do not count (`ETags.set`, the sorting), and different graphs have different tags
+(`ETags.sound`). The second is the one assumption: that the digest is collision-free on the graphs that occur.
+
+`answerB` takes the precondition as `current` or `stale`; `Cond.resolve` computes which, as `evaluatePreconditions`
+does, from the tag the request quotes and the graph the store has. Every write reads the graph, changes it in memory
+and writes the whole of it back, so a write the precondition does not guard can overwrite another's work; one it
+does guard cannot (`no_lost_update`).
+-/
+import LdhHttp.Answer
+
+namespace LdhHttp
+
+/-- An entity tag function. -/
+structure ETags (Tag : Type) where
+  tag : Node → List Triple → Tag
+  /-- The tag is of the graph, a set of triples: `toSortedNTriples` sorts the lines. -/
+  set : ∀ x ts ts', (∀ t, t ∈ ts ↔ t ∈ ts') → tag x ts = tag x ts'
+  /-- Collision-freeness: one tag of a document, one graph. -/
+  sound : ∀ x ts ts', tag x ts = tag x ts' → ∀ t, t ∈ ts ↔ t ∈ ts'
+
+/-- The conditional headers of a write. -/
+inductive Cond (Tag : Type) where
+  /-- Neither `If-Match` nor `If-None-Match`. -/
+  | none
+  /-- `If-Match` with an entity tag. -/
+  | ifMatch (t : Tag)
+  /-- `If-None-Match: *`. -/
+  | ifNoneMatchAny
+
+/-- `evaluatePreconditions`: `If-Match` holds when it quotes the tag of the graph the store has. -/
+def Cond.resolve {Tag : Type} [DecidableEq Tag] (E : ETags Tag) (fs : FinStore) (x : Node) : Cond Tag → Precond
+  | .none => .none
+  | .ifNoneMatchAny => .absent
+  | .ifMatch t => if hasDoc fs x = true ∧ E.tag x (graphOf fs x) = t then .current else .stale
+
+/-- A request whose `If-Match` quotes a tag the document does not have changes nothing. -/
+theorem stale_changes_nothing {hs : HSite} {fs : FinStore} {agent : Option Node} {req : HReq} {s : Success}
+    {fs' : FinStore} (hd : answerB hs fs agent .stale req = .ok (s, fs')) : fs' = fs := by
+  cases req with
+  | get x | head x =>
+    simp only [answerB, readB] at hd; split at hd
+    · cases hd; rfl
+    · cases hd
+  | post x payload =>
+    simp only [answerB, postB, precondFails] at hd
+    repeat' (first | (cases hd; rfl) | split at hd | cases hd)
+  | put x payload =>
+    simp only [answerB, putB, precondFails] at hd
+    repeat' (first | split at hd | cases hd)
+    all_goals simp_all
+  | patch x del ins =>
+    simp only [answerB, patchB, precondFails] at hd
+    repeat' (first | split at hd | cases hd)
+  | delete x =>
+    simp only [answerB, deleteB, precondFails] at hd
+    split at hd; · cases hd
+    split at hd
+    · cases hd
+    · rename_i hx
+      simp only [deleteChecked] at hd
+      split at hd; · cases hd
+      split at hd
+      · cases hd
+      · simp_all
+
+/-- **No lost update.** A write guarded by `If-Match` with the tag of the graph a client read changes the store
+only if the document still holds that graph: whatever another write did in between, this one is not made over it. -/
+theorem no_lost_update {Tag : Type} [DecidableEq Tag] (E : ETags Tag) {hs : HSite} {fs : FinStore}
+    {agent : Option Node} {req : HReq} {s : Success} {fs' : FinStore} {g₀ : List Triple}
+    (hd : answerB hs fs agent ((Cond.ifMatch (E.tag req.target g₀)).resolve E fs req.target) req = .ok (s, fs'))
+    (hw : fs' ≠ fs) :
+    hasDoc fs req.target = true ∧ ∀ t, t ∈ graphOf fs req.target ↔ t ∈ g₀ := by
+  simp only [Cond.resolve] at hd
+  split at hd
+  · rename_i hc
+    exact ⟨hc.1, E.sound _ _ _ hc.2⟩
+  · exact absurd (stale_changes_nothing hd) hw
+
+/-- **A write over another's is refused.** Two clients read the same graph; once one of them has changed it, the
+other's write, quoting the tag it read, changes nothing. -/
+theorem concurrent_write_changes_nothing {Tag : Type} [DecidableEq Tag] (E : ETags Tag) {hs : HSite}
+    {fs : FinStore} {agent : Option Node} {req : HReq} {s : Success} {fs' : FinStore} {g₀ : List Triple}
+    (hchanged : ¬ (hasDoc fs req.target = true ∧ ∀ t, t ∈ graphOf fs req.target ↔ t ∈ g₀))
+    (hd : answerB hs fs agent ((Cond.ifMatch (E.tag req.target g₀)).resolve E fs req.target) req = .ok (s, fs')) :
+    fs' = fs :=
+  Classical.byContradiction fun hw => hchanged (no_lost_update E hd hw)
+
+end LdhHttp