giles
9261d69cc5
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 36s
eff_grant/eff_deny derived relations inherit through member_of (group + role membership) and child_of (resource hierarchy); role_grant confers role capabilities. Deny-overrides via stratified negation, deny authoritative across the inheritance closure. Cyclic membership terminates. Phase 1 suite unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
56 lines
2.6 KiB
Plaintext
56 lines
2.6 KiB
Plaintext
;; lib/acl/engine.sx — ACL ruleset + decision reducer over lib/datalog/.
|
|
;;
|
|
;; The engine is a thin layer: it owns the permit ruleset (SX data rules) and
|
|
;; reduces a (subject, action, resource) decision to a Datalog query against a
|
|
;; db built from EDB facts. The rule engine itself is Datalog's.
|
|
;;
|
|
;; Policy — inheritance with deny-overrides:
|
|
;;
|
|
;; eff_grant(S,A,R) :- grant(S,A,R). ; direct
|
|
;; eff_grant(S,A,R) :- member_of(S,G), eff_grant(G,A,R). ; group/role chain
|
|
;; eff_grant(S,A,R) :- child_of(R,P), eff_grant(S,A,P). ; resource tree
|
|
;; eff_grant(S,A,R) :- member_of(S,Role), role_grant(Role,A,R). ; role expansion
|
|
;;
|
|
;; eff_deny(S,A,R) :- deny(S,A,R). ; direct
|
|
;; eff_deny(S,A,R) :- member_of(S,G), eff_deny(G,A,R). ; group chain
|
|
;; eff_deny(S,A,R) :- child_of(R,P), eff_deny(S,A,P). ; resource tree
|
|
;;
|
|
;; permit(S,A,R) :- eff_grant(S,A,R), not eff_deny(S,A,R).
|
|
;;
|
|
;; DENY-OVERRIDES: an effective deny anywhere in the inheritance closure of
|
|
;; (S,A,R) defeats any effective grant. Deny inherits through the *same* group
|
|
;; and resource chains as grant, so a group-level or ancestor-resource deny is
|
|
;; authoritative for members/descendants — not just a deny naming the exact
|
|
;; (S,A,R). This is the principled, fail-safe reading of "deny wins".
|
|
;;
|
|
;; Termination & stratification:
|
|
;; - eff_grant/eff_deny recurse only over member_of and child_of, which are
|
|
;; EDB relations with no function symbols, so the closure is finite (cyclic
|
|
;; membership/containment just reaches a fixpoint, never loops).
|
|
;; - permit negates eff_deny; neither eff_grant nor eff_deny depends on
|
|
;; permit, so the program is stratifiable (permit sits in a higher stratum).
|
|
|
|
(define
|
|
acl-rules
|
|
(quote
|
|
((eff_grant S A R <- (grant S A R))
|
|
(eff_grant S A R <- (member_of S G) (eff_grant G A R))
|
|
(eff_grant S A R <- (child_of R P) (eff_grant S A P))
|
|
(eff_grant S A R <- (member_of S Role) (role_grant Role A R))
|
|
(eff_deny S A R <- (deny S A R))
|
|
(eff_deny S A R <- (member_of S G) (eff_deny G A R))
|
|
(eff_deny S A R <- (child_of R P) (eff_deny S A P))
|
|
(permit S A R <- (eff_grant S A R) {:neg (eff_deny S A R)}))))
|
|
|
|
;; Build a Datalog db from a list of EDB facts under the ACL ruleset.
|
|
(define acl-build-db (fn (facts) (dl-program-data facts acl-rules)))
|
|
|
|
;; Core decision: does the db permit subject S to perform action A on
|
|
;; resource R? Reduces to a ground Datalog query on the derived `permit`
|
|
;; relation — non-empty result means permitted.
|
|
(define
|
|
acl-permit?
|
|
(fn
|
|
(db subj act res)
|
|
(> (len (dl-query db (list (quote permit) subj act res))) 0)))
|