Repository navigation
access model: cite real access-control systems in extdeps, derive std, enforce via lens - #5415
Merged
Merged
Conversation
…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>
…h (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>
…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>
…, 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>
…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>
6 tasks done
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…key-completeness lens #5418's external-authority gate scans the LIVE extdeps tree and fail-closes on any module lacking an anchor. Once #5422 cleared the FreeMonoid collision and the missing gate_is_heavy_resolve arm let the plan resolve, the gate correctly flagged 5 modules that landed on main AFTER #5418 authored its roster and were neither anchored nor backfilled: missing: extdeps.access.{aws_iam,posix,rbac,zanzibar} (#5415 access model) missing: extdeps.cache.key_completeness (#5423 cache lens) The 4 access modules already carry their real upstream citation in a `// Source:` comment (AWS IAM grammar, POSIX.1-2017/opengroup, ANSI/NIST RBAC, the Zanzibar USENIX paper) — promoted each to the structured `extdeps_external_authority_anchor` carrier the gate gates on (DESIGN §3: the mark on the carrier is the authority). No access sibling is backfilled, so anchoring (not backfilling) is the consistent treatment. extdeps.cache.key_completeness is an internal §5 cache-soundness LENS (a pure reader over the cache catalog), not a cited external-system model — so it joins its 8 extdeps.cache.* siblings on the backfill_pending roster as tracked debt, not a fake external anchor. Verified by execution: the floor's discovery-corpus (587 witnesses) and extdeps_external_authority_gate_passes both go GREEN with this change (live violation set empty, roster count > 150). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…ive #5297) (#5418) * extdeps: external-authority anchor carrier + fail-closed CI lens (revive #5297) Land the never-merged #5297 mechanism onto current main: a structured, lens-checkable external-authority citation on every dsl/extdeps module, enforced fail-closed on the CI floor. Carriers - extdeps.uri: Uri { scheme: UriScheme, locator } with closed-sum UriScheme = Http | Https | File | Ftp (RFC 3986 / 7595 grounded). - extdeps.external_authority: ExternalAuthority { uri }, FactAuthorityOverride, and the canonical `data extdeps_external_authority_anchor` row. Lens (v2.lens.extdeps_external_authority) - Fail-closed live policy per module: machinery-exempt -> backfill-pending -> else require a present external Http/Https anchor. Scheme decoded by exhaustive constructor identity (decode_uri_scheme), never a URL-prefix string. - Violations: MissingFormalAnchor / UnrecognizedAnchorScheme / NonExternalAnchorScheme. Host projection (extdeps_shape_transport_policy_project.rs) - Structural read of the anchor record; live roster derived from the module-path index (declared module name, not directory); backfill + machinery-exempt facts. - 9 builtins wired through 04_method.dag / v1_interpreter.rs / v1_compiler_infer_method.rs. CI - ExtdepsExternalAuthorityGate enrolled in gunbc_ci_spec and scheduled on the floor; runs uri witnesses + live-corpus clean-tree + RED perturb receipts. 44 extdeps modules carry external anchors; 125 remain in the shrinking backfill_pending snapshot. Reconciliation onto current main: the snapshot keys on declared module name, so the post-#5391 directory reorganizations (rust/, package_managers/, ...) need no rename. The only stale entry, extdeps.diagnostic.redfish, was dropped (redfish moved to extdeps.bmc.redfish, separately covered). Verified by execution: 18 projection unit tests; 14 floor-enrolled .dag witnesses (GREEN clean-tree + machinery-exempt fold + 3 RED perturbs + live anchor-drop RED); live-tree discrimination on a real cited module (Https->File and anchor-drop both flip the gate RED, revert restores GREEN); ci_spec/ci_floor_plan enrollment witnesses; gate main -> ExitSuccess via real shell; cargo fmt + clippy -D warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Mi3t2wX7UPzgqLyYAE1kS * ci_floor_plan: add missing gate_is_heavy_resolve arm for ExtdepsExternalAuthorityGate #5418 added ExtdepsExternalAuthorityGate to the Gate enum and to every match over it EXCEPT gate_is_heavy_resolve (ci_floor_plan.dag:154), so once the v1↔v2 FreeMonoid collision cleared (#5422 now in this branch) the plan resolve reached this fn and fail-closed on a non-exhaustive match: ci_floor_plan.dag:154:3: error: non-exhaustive match: missing variant(s) ExtdepsExternalAuthorityGate The extdeps external-authority gate is a focused lens witness (filesystem_read over dsl/extdeps/**), not a whole-tree heavy resolve like SourceRootIngest / DslCompileClean — so it joins the other lens gates (Layering/ResolvedImports) at `false`. Plan-data only; resolved at runtime by claim_executor, no stage0 seed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * extdeps live-clean: anchor the 4 access modules + backfill the cache key-completeness lens #5418's external-authority gate scans the LIVE extdeps tree and fail-closes on any module lacking an anchor. Once #5422 cleared the FreeMonoid collision and the missing gate_is_heavy_resolve arm let the plan resolve, the gate correctly flagged 5 modules that landed on main AFTER #5418 authored its roster and were neither anchored nor backfilled: missing: extdeps.access.{aws_iam,posix,rbac,zanzibar} (#5415 access model) missing: extdeps.cache.key_completeness (#5423 cache lens) The 4 access modules already carry their real upstream citation in a `// Source:` comment (AWS IAM grammar, POSIX.1-2017/opengroup, ANSI/NIST RBAC, the Zanzibar USENIX paper) — promoted each to the structured `extdeps_external_authority_anchor` carrier the gate gates on (DESIGN §3: the mark on the carrier is the authority). No access sibling is backfilled, so anchoring (not backfilling) is the consistent treatment. extdeps.cache.key_completeness is an internal §5 cache-soundness LENS (a pure reader over the cache catalog), not a cited external-system model — so it joins its 8 extdeps.cache.* siblings on the backfill_pending roster as tracked debt, not a fake external anchor. Verified by execution: the floor's discovery-corpus (587 witnesses) and extdeps_external_authority_gate_passes both go GREEN with this change (live violation set empty, roster count > 150). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
First substantive step of dismantling
ctrl: model code visibility / access as a real, derivedfact instead of a git-topology nickname. Supersedes #5414 (closed), which silently re-coined
Zanzibar as a std abstraction — the §3 violation this PR corrects.
Method (DESIGN §3): model real systems → derive std → validate
Rather than invent an access abstraction from one system, model several real access-control systems
faithfully in
extdeps/access/(cited, real names — asextdeps/cloud/gcp/iam+extdeps/githubalready do), then derive the std abstraction from their commonality and validate it by mapping
each system in. If a real system can't be expressed, the abstraction is wrong.
dsl/extdeps/access/— four systems, cited, compile-verifiedzanzibar.dagaws_iam.dagposix.dagrbac.dagdsl/std/access.dag— the DERIVED abstractionAccessRequest<S,A,O>,AccessDecision = Permit | Deny(combined Deny-wins — the fail-closed meet),AccessPolicy<S,A,O>(DESIGN §4 Realization: one interface, N system handlers).dsl/std/access_validation_test.dag+dsl/test/claim/access_iam_validation_test.dag— validationPOSIX (DAC), RBAC, and AWS IAM (ABAC) each fully inhabit the same
AccessPolicy<S,A,O>.11 decision witnesses, green by execution (
gunbc run --claim-run).The headline finding: ABAC "context" decomposes — no new dimension
The validation first flagged a strain: AWS IAM Conditions seem to decide on request context beyond
subject/action/object. Re-derivation shows "context" was itself a nickname — it decomposes:
s3:prefix→ an action parameter; tags → subject/object attributes), andaws:SourceIpinternal-CIDR → the request'sNetworkLocality;aws:CurrentTime→Timestamp).So
std/accessis structurally unchanged — the generics carry ABAC once instantiated richly.access_iam_validation_test.dagproves it: an "Allows3:GetObjectIF internal-network AND prefixmatches AND MFA present" statement decided entirely from grounded fields, with no context map.
src/v2/lens/{visibility,visibility_test}.dag— enforcement (Step 3, pure core)A fail-closed lens flagging the §5 leak the publication step must never commit: a public module
importing a non-public one. 4 lens-unit witnesses green by execution; breaking the scanner turns the
leak witness red. (Live-tree wiring — facts from the resolved program via a Rust seed /
dependency_lens— is the next step, marked in the file.)
Verification (DESIGN §5 — green by execution, not just typecheck)
0 diagnostics; perturbation of each new file produces a located error.test fnwitnesses green by execution across the access validation + the lens.SourceIp→NetworkLocalitydecomposition.Deferred (tracked)
std.access(the ReBAC action/grouping-fusion mapping).std.accessand walk the real import DAG (Rust-seed bridge).🤖 Generated with Claude Code