Skip to content

access model: ownership + visibility over the node graph (ReBAC / Zanzibar) - #5414

Closed
briansrls wants to merge 1 commit into
mainfrom
worktree-access-model
Closed

briansrls wants to merge 1 commit into
mainfrom
worktree-access-model

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

First step of dismantling ctrl: model code visibility/privacy as a real fact instead of a
git-topology nickname, so private parts of the (public) gunbc tree are kept private by a label
rather than by which repo a file sits in.

The reframe (DESIGN §2/§3)

Today the only privacy lever is the repo split — repo == privacy. That fuses facts that must
live apart. The informal version already exists as comments (operator_fleet_network.dag:8
"secrets remain in ctrl"; ci_fleet.dag:4 "operator inventory remains private (ctrl)"). This
separates them:

Concept What it is Status
Ownership who owns a node (root of authority) this PR
Visibility who may read/write a node (ReBAC) this PR
Repo where code is stored + its own access level extdeps/github — referenced, not re-coined
Publication (labeled tree + audience) → which units → which repo/CI follow-up; the 2-repo split = one handler

Composes with SecretRef (orthogonal axis): SecretRef keeps secret values out of git; this keeps
private code/data out of the public projection.

Anchor & grounding

  • Google Zanzibar / ReBAC. A relation tuple ⟨object, relation, subject⟩ is structurally a
    substrate Edge, so the access graph is a subgraph of the node graph. Subjects are usersets:
    Everyone (public), Is (a specific node), MembersOf (members of an org / readers of a node).
  • Real .dag nodes. Principals (operator, org, alice, bob) are real nodes referenced by node
    identity (Symbol) — no minted id (§3 anti-nickname).
  • Placement. src/v2/std/ because the model references real node ids and dsl/ cannot import
    v2.std.node. Precedent: src/v2/lens/extdeps_shape_transport_policy keys facts on QualifiedName.

What's here

  • src/v2/std/access.dag — the framework. Ownership: owner_of / effective_owner
    (unowned ⇒ operator, fail-closed) / is_owner. Visibility: can_read / can_write
    (Owner ⊒ Writer ⊒ Reader), subject_admits (public / direct / one-level org membership),
    is_public, and the leak rule effective_public (a node is publishable only if it's public
    and every dependency it exposes is — so a public node importing a private one can't leak).
  • src/v2/std/access_test.dag — 17 executed test fn witnesses.

Verification (DESIGN §5 — green by execution, not just typecheck)

  • Compile 0 diagnostics; perturbation produces a located error (the file is really checked).
  • 17/17 witnesses green by execution (gunbc run --claim-run): public read, stranger denied,
    owner-implies-read, org-member read, non-member denied, writer can/can't write, writer-implies-read,
    public classification both ways, and the three leak-rule cases.
  • Targeted discriminating check: breaking effective_public to ignore dependencies turns the leak
    witness red.

Deferred to the enforcement lens (next PR)

The "exactly one owner" / inheritance-along-containment / DAC ("only the owner may grant")
invariants are modeled as intent but not yet enforced; recursive userset resolution is
one-level; and effective_public currently takes pre-folded dependency flags rather than walking
the real import DAG via fold_node. That lens is the next step.

🤖 Generated with Claude Code

…zibar)

Separate the facts conflated behind the "repo split" (repo == privacy) into independent
concepts (DESIGN §2/§3): ownership and visibility as relations over real .dag nodes,
anchored on Google Zanzibar / ReBAC. A relation tuple is structurally a substrate Edge,
so the access graph is a subgraph of the node graph — not a side-store. Composes with
SecretRef (orthogonal): SecretRef keeps secret values out of git; this keeps private
code/data out of the public projection.

v2.std.access:
- Relation (Owner|Reader|Writer|Member), Subject (Everyone | Is | MembersOf userset),
  Grant (= a labeled Edge).
- Ownership: OwnerResolution (Owned|Unowned, not Option-overloaded); owner_of /
  effective_owner (unowned => operator, fail-closed) / is_owner.
- Visibility: can_read / can_write (relation hierarchy Owner >= Writer >= Reader),
  subject_admits (public / direct / one-level org membership), is_public, and the
  leak rule effective_public (public AND every exposed dependency public — fail-closed
  meet-fold; a public node importing a private one cannot be published).

v2.std.access_test: principals (operator, gunb_ai_org, alice, bob) declared as real
.dag nodes, referenced by node identity (Symbol) — no minted id. 17 executed witnesses.

Verified (DESIGN §5): compile 0-diagnostics + discriminating red; 17/17 test fn
witnesses green by execution (gunbc run --claim-run); breaking the leak rule's
dependency meet-fold turns its witness red.

Deferred to the enforcement lens (follow-up): one-owner / inheritance / DAC invariants,
recursive userset resolution, and walking effective_public over the real import DAG.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Superseding this approach. src/v2/std/access.dag here silently re-coined Zanzibar as a std abstraction — the §3 nickname violation. Corrected method (per discussion): model several real access-control systems faithfully in dsl/extdeps/access/ (Zanzibar ✓, AWS IAM, POSIX, NIST RBAC — alongside the existing extdeps/cloud/gcp/iam + extdeps/github), then DERIVE the std abstraction from their commonality and validate it against each. The Step-3 visibility lens is independent and survives. New work continues on access-model-step3 / a follow-up PR.

@briansrls briansrls closed this Jun 20, 2026
briansrls added a commit that referenced this pull request Jun 21, 2026
…, enforce via lens (#5415)

* access model: ownership + visibility over the node graph (ReBAC / Zanzibar)

Separate the facts conflated behind the "repo split" (repo == privacy) into independent
concepts (DESIGN §2/§3): ownership and visibility as relations over real .dag nodes,
anchored on Google Zanzibar / ReBAC. A relation tuple is structurally a substrate Edge,
so the access graph is a subgraph of the node graph — not a side-store. Composes with
SecretRef (orthogonal): SecretRef keeps secret values out of git; this keeps private
code/data out of the public projection.

v2.std.access:
- Relation (Owner|Reader|Writer|Member), Subject (Everyone | Is | MembersOf userset),
  Grant (= a labeled Edge).
- Ownership: OwnerResolution (Owned|Unowned, not Option-overloaded); owner_of /
  effective_owner (unowned => operator, fail-closed) / is_owner.
- Visibility: can_read / can_write (relation hierarchy Owner >= Writer >= Reader),
  subject_admits (public / direct / one-level org membership), is_public, and the
  leak rule effective_public (public AND every exposed dependency public — fail-closed
  meet-fold; a public node importing a private one cannot be published).

v2.std.access_test: principals (operator, gunb_ai_org, alice, bob) declared as real
.dag nodes, referenced by node identity (Symbol) — no minted id. 17 executed witnesses.

Verified (DESIGN §5): compile 0-diagnostics + discriminating red; 17/17 test fn
witnesses green by execution (gunbc run --claim-run); breaking the leak rule's
dependency meet-fold turns its witness red.

Deferred to the enforcement lens (follow-up): one-owner / inheritance / DAC invariants,
recursive userset resolution, and walking effective_public over the real import DAG.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* access model step 3: visibility-leak lens over the module import graph (pure core)

A lens (pure reader, fail-closed) that flags the §5 leak the publication realization must
never commit: a PUBLIC module that imports a module which is not public. This is the
import-graph realization of access.dag's leak rule (effective_public).

src/v2/lens/visibility.dag:
- ModuleVisibilityFact { module: QualifiedName, public: Bool, imports: List<QualifiedName> }
  (keyed on the `module` identity, not a filepath), VisibilityLeak { importer, imported }.
- module_is_public (fail-closed: a module absent from the set is non-public, so an unknown
  import is a leak), scan_visibility_leaks (enumerates located leaks), visibility_clean.

src/v2/lens/visibility_test.dag: 4 lens-unit witnesses — leak caught, clean closure passes,
fail-closed unknown import, private-importer exempt.

Verified (DESIGN §5): compile 0-diagnostics; 4/4 witnesses green by execution
(gunbc run --claim-run); breaking the scanner turns the leak witness red.

Deferred (decision point): the LIVE corpus witness ("0 leaks in the real tree") needs live
ModuleVisibilityFacts from the resolved program — public via access.is_public over grants,
imports via v2.std.dependency.dependency_lens (kind ModuleDependsOn). That bridge is a Rust
seed / corpus-as-node handle (cf. the extdeps_shape_transport_policy lens). Also not yet
enforced: the ownership invariants (one-owner / inheritance / DAC).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* access model: extdeps-first rework — model real systems, derive std, validate

Corrects the §3 nickname violation: the earlier src/v2/std/access.dag silently re-coined
Zanzibar as a std abstraction. Method (per discussion): model several real access-control
systems faithfully in extdeps/access (cited, real names), then DERIVE the std abstraction
from their commonality and validate it against each ("see if anything breaks").

extdeps/access/ (cited, real names; each compile-verified):
- zanzibar.dag  — Google Zanzibar relation tuples + userset-rewrite config (USENIX ATC '19)
- aws_iam.dag   — AWS IAM JSON policy: Effect/Principal/Action/Resource/Condition (v2012-10-17)
- posix.dag     — POSIX.1-2017 file mode bits (owner/group/other rwx + setuid/setgid/sticky)
- rbac.dag      — NIST/ANSI INCITS 359-2004 Core+Hierarchical RBAC (UA/PA/RH, PRMS=OPS×OBS)
  (alongside the pre-existing extdeps/cloud/gcp/iam + extdeps/github as further data points)

std/access.dag — the DERIVED abstraction: AccessRequest<S,A,O>, AccessDecision = Permit|Deny
(combined Deny-wins), AccessPolicy<S,A,O> (DESIGN §4 Realization: one interface, N handlers).

std/access_validation_test.dag — POSIX (DAC) and RBAC both fully inhabit the abstraction;
7 decision witnesses green by execution; broken POSIX class-resolution turns a witness red.

Findings (what strains the shape): POSIX's object-attached ACL inhabits AccessPolicy directly;
RBAC's global policy must be curried in; AWS IAM Conditions decide on request CONTEXT beyond
S/A/O (ABAC needs a context dimension); Zanzibar fuses action + subject-grouping into `relation`.

Removes the superseded src/v2/std/{access,access_test}.dag (PR #5414, closed). The Step-3
visibility lens is independent and unaffected.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* access model: AWS IAM ABAC "context" decomposes — no opaque dimension, std core unchanged

The earlier validation flagged a "strain": AWS IAM Conditions decide on request context
beyond subject/action/object. Re-derivation shows that "context" is itself a nickname — it
DECOMPOSES, and the std abstraction needs no new dimension:

  * Most condition keys are attribute-carrying S/A/O — modeled thin (bare ids), they LOOKED
    like a separate dimension. s3:prefix -> an ACTION parameter; principal/resource tags ->
    subject/object attributes.
  * The environmental remainder grounds in frameworks already in the repo: aws:SourceIp
    (internal CIDR) -> the request's NetworkLocality (Lan/Loopback/... vs Internet);
    aws:CurrentTime -> Timestamp. ("derived" = decomposed to grounded atoms; the live values
    remain runtime observations, but their TYPES are existing frameworks — nothing minted.)

So AccessRequest<S,A,O> / AccessPolicy<S,A,O> are UNCHANGED — the generics carry it once
instantiated richly. test/claim/access_iam_validation_test.dag proves it: an
"Allow s3:GetObject IF internal-network AND prefix matches AND MFA present" statement decided
ENTIRELY from grounded S/A fields, inhabiting the SAME AccessPolicy<S,A,O> as POSIX/RBAC, with
no context map. 4 decision witnesses green by execution; breaking the SourceIp->NetworkLocality
decomposition turns the external-source witness red.

std/access.dag: derivation receipt updated (STRAIN -> RESOLVED); S/A/O noted as attribute-carrying.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(access): move access_validation_test out of the std layer (wrong-direction import)

The CI floor's layering witness (clean_tree_no_wrong_direction_imports_holds) went RED:
dsl/std/access_validation_test.dag was module std.test.access_validation (std layer) but
imports extdeps.access.posix/rbac — std must not import upward to extdeps.

Move it to dsl/test/claim/access_validation_test.dag (module test.claim.access_validation,
the test layer, which may import extdeps — the IAM validation test already does). No logic
change. dsl compiles 0-diagnostics.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant