add diagram sharing design and tla verification specs

specs/CascadeClosure.cfg

@@ -0,0 +1,12 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    d1 = d1
+    d2 = d2
+    d3 = d3
+
+INVARIANT
+    TypeOK
+    InvCascadeSound
+    InvFrontierSound
+    InvCascadeComplete

specs/CascadeClosure.tla

@@ -0,0 +1,57 @@
+-------------------------------- MODULE CascadeClosure --------------------------------
+\* Verifies the transitive-share cascade (docs/design/diagram-sharing.md):
+\* sharing a root diagram must grant exactly the diagrams reachable from it via
+\* diagram->diagram references -- no more (over-sharing = leak), no less
+\* (under-sharing = broken functionality) -- and must terminate on cyclic graphs.
+\*
+\* The BFS (visited/frontier, visited-guarded) is checked against an independent
+\* fixpoint reachability, over EVERY possible reference graph on 3 diagrams.
+
+EXTENDS Integers, FiniteSets
+
+CONSTANTS d1, d2, d3
+Diagrams == {d1, d2, d3}
+Root     == d1
+
+VARIABLES refs, visited, frontier
+vars == <<refs, visited, frontier>>
+
+\* independent definition of reachability: least fixpoint of the neighbour step
+RECURSIVE ReachSet(_)
+ReachSet(S) ==
+    LET S2 == S \cup {y \in Diagrams : \E x \in S : <<x, y>> \in refs}
+    IN IF S2 = S THEN S ELSE ReachSet(S2)
+
+Reachable == ReachSet({Root})
+
+Init ==
+    /\ refs \in SUBSET (Diagrams \X Diagrams)   \* every graph, incl. cycles & self-loops
+    /\ visited = {}
+    /\ frontier = {Root}
+
+\* visit one frontier node; enqueue its not-yet-visited neighbours (cycle-safe)
+Step ==
+    /\ frontier # {}
+    /\ \E d \in frontier :
+        LET nv   == visited \cup {d}
+            nbrs == {y \in Diagrams : <<d, y>> \in refs}
+        IN /\ visited'  = nv
+           /\ frontier' = (frontier \ {d}) \cup (nbrs \ nv)
+           /\ UNCHANGED refs
+
+Next == Step
+Spec == Init /\ [][Next]_vars
+
+TypeOK ==
+    /\ refs \subseteq (Diagrams \X Diagrams)
+    /\ visited \subseteq Diagrams
+    /\ frontier \subseteq Diagrams
+
+\* never grant outside the reference closure (no over-sharing / leak)
+InvCascadeSound == visited \subseteq Reachable
+\* frontier stays within the closure too
+InvFrontierSound == frontier \subseteq Reachable
+\* on termination, granted set equals the closure exactly (no under-sharing)
+InvCascadeComplete == (frontier = {}) => (visited = Reachable)
+
+=============================================================================

specs/DiagramSharing.cfg

@@ -0,0 +1,27 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    u1 = u1
+    u2 = u2
+    adm = adm
+    d1 = d1
+    d2 = d2
+    c1 = c1
+    PUBLIC = PUBLIC
+    PENDING = PENDING
+    ANON = ANON
+
+INVARIANT
+    TypeOK
+    InvEventConfidentiality
+    InvEventCompleteness
+    InvEditImpliesSee
+    InvDeleteOwnerOnly
+    InvChildNeedsParentSee
+    InvChildNeedsParentEdit
+    InvViewGranteeCannotEditChild
+    InvAnonConfinedSee
+    InvAnonConfinedEdit
+    InvAnonPublicReceives
+    InvPendingNoAccess
+    InvReservedNotOwner

specs/DiagramSharing.tla

@@ -0,0 +1,160 @@
+-------------------------------- MODULE DiagramSharing --------------------------------
+\* Authorization core of the diagram-sharing design (docs/design/diagram-sharing.md).
+\* Verifies the PROPOSED design: named view/edit grants + public grants + pending
+\* grants + child-entity derivation + recipient-scoped event routing.
+\*
+\* Threat model: authenticated users are mutually untrusting tenants.
+\* Assumption NOT modeled (taken as given): mqtt-lib's %u ACL correctly isolates
+\* per-user event topics, so a user only receives events published to their own
+\* namespace (or the public namespace). Under that assumption "u receives event for
+\* x" == "u in Recipients(x) OR x is public" == Delivers(u, x) below.
+
+EXTENDS Integers, FiniteSets
+
+CONSTANTS u1, u2, adm, d1, d2, c1, PUBLIC, PENDING, ANON
+
+Users    == {u1, u2}            \* regular principals: can own and be grantees
+Admins   == {adm}               \* bypass everything
+Diagrams == {d1, d2}            \* ownership-enabled resources
+Children == {c1}                \* derive permission from a parent diagram
+Parent   == (c1 :> d1)          \* c1 belongs to diagram d1
+
+Resources    == Diagrams \cup Children
+Readers      == Users \cup Admins \cup {ANON}
+GranteeSpace == Users \cup {PUBLIC, PENDING}   \* who a grant may name
+Levels       == {"view", "edit"}
+LevelOrNone  == {"none", "view", "edit"}
+GrantKeys    == Diagrams \X GranteeSpace
+
+VARIABLES owner, grants
+vars == <<owner, grants>>
+
+GrantOf(d, g) == IF <<d, g>> \in DOMAIN grants THEN grants[<<d, g>>] ELSE "none"
+IsAdmin(u)    == u \in Admins
+DiagramOf(x)  == IF x \in Diagrams THEN x ELSE Parent[x]
+
+\* ---- permission predicates on a diagram ----
+SeeDiagram(u, d) ==
+    \/ IsAdmin(u)
+    \/ u = owner[d]
+    \/ GrantOf(d, u) \in {"view", "edit"}
+    \/ GrantOf(d, PUBLIC) \in {"view", "edit"}
+
+EditDiagram(u, d) ==
+    \/ IsAdmin(u)
+    \/ u = owner[d]
+    \/ GrantOf(d, u) = "edit"
+    \/ GrantOf(d, PUBLIC) = "edit"
+
+\* ---- the resolver: children derive from their parent diagram ----
+CanSee(u, x)  == SeeDiagram(u, DiagramOf(x))
+CanEdit(u, x) == EditDiagram(u, DiagramOf(x))
+
+\* delete: a diagram is owner/admin only; a child follows edit-of-parent
+CanDelete(u, x) ==
+    IF x \in Diagrams
+    THEN IsAdmin(u) \/ u = owner[x]
+    ELSE CanEdit(u, x)
+
+\* ---- event recipients (who the emitter publishes to) ----
+DiagramRecipients(d) ==
+    {owner[d]}
+    \cup {u \in Users : GrantOf(d, u) \in {"view", "edit"}}
+    \cup (IF GrantOf(d, PUBLIC) \in {"view", "edit"} THEN {PUBLIC} ELSE {})
+
+Recipients(x) == DiagramRecipients(DiagramOf(x))
+
+\* a reader receives the event iff it landed in their own namespace (membership)
+\* or in the public namespace (PUBLIC in the recipient set => published publicly)
+Delivers(u, x) == (u \in Recipients(x)) \/ (PUBLIC \in Recipients(x))
+
+\* ---- state machine ----
+Init ==
+    /\ owner \in [Diagrams -> Users]
+    /\ grants = [k \in GrantKeys |-> "none"]
+
+SetGrant(d, g, l) ==
+    /\ grants' = [grants EXCEPT ![<<d, g>>] = l]
+    /\ UNCHANGED owner
+
+ClearGrant(d, g) ==
+    /\ grants' = [grants EXCEPT ![<<d, g>>] = "none"]
+    /\ UNCHANGED owner
+
+\* ownership transfer changes only the owner field; grants are preserved
+Transfer(d, u) ==
+    /\ owner' = [owner EXCEPT ![d] = u]
+    /\ UNCHANGED grants
+
+Next ==
+    \/ \E d \in Diagrams, g \in GranteeSpace, l \in Levels : SetGrant(d, g, l)
+    \/ \E d \in Diagrams, g \in GranteeSpace : ClearGrant(d, g)
+    \/ \E d \in Diagrams, u \in Users : Transfer(d, u)
+
+Spec == Init /\ [][Next]_vars
+
+\* ===================== invariants =====================
+
+TypeOK ==
+    /\ owner \in [Diagrams -> Users]
+    /\ grants \in [GrantKeys -> LevelOrNone]
+
+\* No over-delivery: anyone who receives an event for x can also read x.
+\* Ties the recipient-scoped routing to the CRUD read predicate.
+InvEventConfidentiality ==
+    \A u \in Readers, x \in Resources : Delivers(u, x) => CanSee(u, x)
+
+\* No under-delivery: every authorized non-admin reader receives the event.
+\* (Admins read on demand; they are not on the event feed by design.)
+InvEventCompleteness ==
+    \A u \in Users, x \in Resources : (CanSee(u, x) /\ ~IsAdmin(u)) => Delivers(u, x)
+
+\* Edit is at least as strong as view.
+InvEditImpliesSee ==
+    \A u \in Readers, x \in Resources : CanEdit(u, x) => CanSee(u, x)
+
+\* Delete of a diagram is strictly owner/admin -- never via an edit/public grant.
+InvDeleteOwnerOnly ==
+    \A u \in Readers, d \in Diagrams : CanDelete(u, d) => (IsAdmin(u) \/ u = owner[d])
+
+\* A child can never be seen/edited by someone who can't see/edit its parent.
+InvChildNeedsParentSee ==
+    \A u \in Readers, x \in Children : CanSee(u, x) => CanSee(u, Parent[x])
+InvChildNeedsParentEdit ==
+    \A u \in Readers, x \in Children : CanEdit(u, x) => CanEdit(u, Parent[x])
+
+\* A view-only grantee (no other relationship, no public-edit) cannot edit a child.
+\* This is the "view is a lie" property the design must defeat.
+InvViewGranteeCannotEditChild ==
+    \A u \in Users, x \in Children :
+        ( u # owner[Parent[x]]
+          /\ ~IsAdmin(u)
+          /\ GrantOf(Parent[x], u) = "view"
+          /\ GrantOf(Parent[x], PUBLIC) # "edit" )
+        => ~CanEdit(u, x)
+
+\* Anonymous callers reach only public resources, and never edit except public-edit.
+InvAnonConfinedSee ==
+    \A x \in Resources : CanSee(ANON, x) => (GrantOf(DiagramOf(x), PUBLIC) \in {"view", "edit"})
+InvAnonConfinedEdit ==
+    \A x \in Resources : CanEdit(ANON, x) => (GrantOf(DiagramOf(x), PUBLIC) = "edit")
+
+\* Completeness for anonymous viewers: a public resource's events reach anonymous.
+InvAnonPublicReceives ==
+    \A x \in Resources :
+        (GrantOf(DiagramOf(x), PUBLIC) \in {"view", "edit"}) => Delivers(ANON, x)
+
+\* A pending grant (grantee = PENDING) is inert: a user with no personal/public
+\* grant and not owner/admin cannot see the diagram even if a PENDING grant exists.
+InvPendingNoAccess ==
+    \A u \in Readers, d \in Diagrams :
+        ( ~IsAdmin(u) /\ u # owner[d]
+          /\ GrantOf(d, u) = "none"
+          /\ GrantOf(d, PUBLIC) = "none" )
+        => ~CanSee(u, d)
+
+\* Reserved sentinels are never principals that own resources.
+InvReservedNotOwner ==
+    \A d \in Diagrams : owner[d] \notin {PUBLIC, PENDING, ANON}
+
+=============================================================================

specs/DiagramSharingCurrent.cfg

@@ -0,0 +1,15 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    u1 = u1
+    u2 = u2
+    adm = adm
+    d1 = d1
+    d2 = d2
+    c1 = c1
+
+INVARIANT
+    TypeOK
+    InvEventConfidentiality
+    InvChildNeedsParentSee
+    InvChildNeedsParentEdit

specs/DiagramSharingCurrent.tla

@@ -0,0 +1,59 @@
+----------------------------- MODULE DiagramSharingCurrent -----------------------------
+\* The CURRENT (pre-feature) behavior, modeled to demonstrate that the security
+\* invariants in DiagramSharing.tla have teeth: today's behavior VIOLATES them.
+\* Verified facts encoded here:
+\*   - diagrams: read/update/delete gated to owner (transport_execute.rs:72-129)
+\*   - child entities: NO access control at all (types.rs:144-155) -> see/edit = TRUE
+\*   - events: broadcast to every authenticated subscriber (dispatcher.rs:72-82)
+\* Expectation: InvEventConfidentiality and the child invariants FAIL.
+
+EXTENDS Integers, FiniteSets
+
+CONSTANTS u1, u2, adm, d1, d2, c1
+
+Users    == {u1, u2}
+Admins   == {adm}
+Diagrams == {d1, d2}
+Children == {c1}
+Parent   == (c1 :> d1)
+
+Resources == Diagrams \cup Children
+Readers   == Users \cup Admins
+
+VARIABLES owner
+vars == <<owner>>
+
+IsAdmin(u) == u \in Admins
+
+SeeDiagram(u, d)  == IsAdmin(u) \/ u = owner[d]
+EditDiagram(u, d) == IsAdmin(u) \/ u = owner[d]
+
+\* children are ungated today
+CanSee(u, x)  == IF x \in Diagrams THEN SeeDiagram(u, x)  ELSE TRUE
+CanEdit(u, x) == IF x \in Diagrams THEN EditDiagram(u, x) ELSE TRUE
+
+\* events broadcast to every authenticated principal
+Delivers(u, x) == u \in (Users \cup Admins)
+
+Init == owner \in [Diagrams -> Users]
+
+Transfer(d, u) ==
+    /\ owner' = [owner EXCEPT ![d] = u]
+
+Next == \E d \in Diagrams, u \in Users : Transfer(d, u)
+
+Spec == Init /\ [][Next]_vars
+
+TypeOK == owner \in [Diagrams -> Users]
+
+\* Same property as the proposed spec: receiving an event implies being able to read.
+InvEventConfidentiality ==
+    \A u \in Readers, x \in Resources : Delivers(u, x) => CanSee(u, x)
+
+InvChildNeedsParentSee ==
+    \A u \in Readers, x \in Children : CanSee(u, x) => CanSee(u, Parent[x])
+
+InvChildNeedsParentEdit ==
+    \A u \in Readers, x \in Children : CanEdit(u, x) => CanEdit(u, Parent[x])
+
+=============================================================================

specs/DiagramSharingCurrentChild.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    u1 = u1
+    u2 = u2
+    adm = adm
+    d1 = d1
+    d2 = d2
+    c1 = c1
+
+INVARIANT
+    TypeOK
+    InvChildNeedsParentEdit

specs/GrantLifecycle.cfg

@@ -0,0 +1,10 @@
+SPECIFICATION Spec
+
+INVARIANT
+    TypeOK
+    InvCascadeNeverDowngrades
+    InvCascadeMeetsRequest
+    InvCascadeIsMax
+    InvDirectSetsExact
+    InvRevokeRemovesSee
+    InvRevokeRemovesEdit