agent-claw: automated task changes

cdk/node_modules/aws-cdk-lib/aws-iam/docs/policy-merging.als

@@ -0,0 +1,201 @@
+/*
+Alloy model to confirm the logic behind merging IAM Statements.
+
+This proves that merging two statements based on the following conditions:
+
+- Effects are the same
+- NotAction, NotResource, NotPrincipal are the same(*)
+- Of Action, Resource, Principal sets, 2 out of 3 are the same(*)
+
+Is sound, as the model doesn't find any examples of where the meaning
+of statements is changed by merging.
+
+Find Alloy at https://alloytools.org/.
+
+(*) Some of these sets may be empty--that is fine, the logic still works out.
+*/
+
+//-------------------------------------------------------
+// Base Statement definitions
+enum Effect { Allow, Deny }
+enum Resource { ResourceA, ResourceB }
+enum Action { ActionA, ActionB }
+enum Principal { PrincipalA, PrincipalB }
+
+sig Statement {
+  effect: Effect,
+  principal: set Principal,
+  notPrincipal: set Principal,
+  action: set Action,
+  notAction: set Action,
+  resource: set Resource,
+  notResource: set Resource,
+} {
+  // Exactly one of Xxx and notXxx is non-empty
+  (some principal) iff not (some notPrincipal)
+  (some action) iff not (some notAction)
+  (some resource) iff not (some notResource)
+}
+
+// So that we can compare Statements using =, if two Statements have
+// exactly the same properties then they are the same Statement
+fact {
+  all a, b: Statement {
+     (
+      a.effect = b.effect and
+      a.principal = b.principal and 
+      a.notPrincipal = b.notPrincipal and
+      a.action = b.action and
+      a.notAction = b.notAction and
+      a.resource = b.resource and
+      a.notResource = b.notResource) implies a = b 
+  }
+}
+
+//-------------------------------------------------------
+// Requests and evaluations
+sig Request {
+  principal: Principal,
+  action: Action,
+  resource: Resource,
+}
+
+// Whether the statement applies to the given request
+pred applies[s: Statement, req: Request] {
+  some s.principal implies req.principal in s.principal
+  some s.notPrincipal implies req.principal not in s.notPrincipal
+  some s.action implies req.action in s.action
+  some s.notAction implies req.action not in s.notAction
+  some s.resource implies req.resource in s.resource
+  some s.notResource implies req.resource not in s.notResource
+}
+
+// Whether or not to allow the given request according to the given statements
+//
+// A request is allowed if there's at least one statement allowing it and
+// no statements denying it.
+pred allow[req: Request, ss: some Statement] {
+  some s: ss | applies[s, req] and s.effect = Allow
+  no s: ss | applies[s, req] and s.effect = Deny
+}
+
+run show_some_allowed_requests {
+  some ss: set Statement, r: Request | allow[r, ss] and /* no useless Statements floating around */ (no s" : Statement | s" not in ss)
+} for 3 but 1 Request
+
+//-------------------------------------------------------
+// Statement merging
+
+// Assert that m is the merged version of a and b
+//
+// This encodes the important logic: the rules of merging.
+pred merged[a: Statement, b: Statement, m: Statement] {
+  // Preconditions
+  a.effect = b.effect
+  a.notAction = b.notAction
+  a.notResource = b.notResource
+  a.notPrincipal = b.notPrincipal
+
+  // Merging is allowed in one of 2 cases:
+  // - of the pairs { Resource, Action, Principal } 2 are the same (then the 3rd pair may be merged)
+  // - if one statement is a full subset of the other one (then it may be subsumed) [not implemented yet]
+  let R = a.resource = b.resource, A = a.action = b.action, P = a.principal = b.principal {
+    ((R and A) or (R and P) or  (A and P) or 
+     (a.resource in b.resource and a.action in b.action and a.principal in b.principal) or
+     (b.resource in a.resource and b.action in a.action and b.principal in a.principal))
+  }
+
+  // Result of merging
+  m.effect = a.effect
+  m.action = a.action + b.action
+  m.notAction = a.notAction
+  m.resource = a.resource + b.resource
+  m.notResource = a.notResource 
+  m.principal = a.principal + b.principal
+  m.notPrincipal = a.notPrincipal
+}
+
+run show_some_nontrivial_merges {
+  some disj s0, s1, M: Statement | merged[s0, s1, M] and s0.action != s1.action
+}
+
+// For any pair of statements, there is only one possible merging
+check merging_is_unique {
+  all s0, s1: Statement {
+    no disj m0, m1 : Statement | merged[s0, s1, m0] and merged[s0, s1, m1]
+  }
+} for 5
+
+// For all statements, the evaluation of the individual statements is the same as the evaluation
+// of the merged statement.
+check merging_does_not_change_evaluation {
+  all a: Statement, b: Statement, m: Statement, r: Request {
+    merged[a, b, m] implies (allow[r, a + b] iff allow[r, m])
+  }
+} for 3
+
+// There are no 3 statements such that merged(merged(s0, s1), s2) != merged(s0, merged(s1, s2))
+check merging_is_associative {
+  no s0, s1, s2, h0, h1, m0, m1: Statement {
+    merged[s0, s1, h0] and merged[h0, s2, m0]
+    merged[s1, s2, h1] and merged[h1, s0, m1]
+    m0 != m1
+  }
+} for 10
+
+// For all statements, merged(s0, s1) = merged(s1, s0)
+check merging_is_commutative {
+  all s0, s1, m: Statement {
+    merged[s0, s1, m] implies merged[s1, s0, m]
+  }
+} for 5
+
+//-------------------------------------------------------
+// Repeated application of merging
+
+// Whether a and b are mergeable
+pred mergeable[a: Statement, b: Statement] {
+  some m: Statement | m != a and m != b and merged[a, b, m]
+}
+
+// Maximally merged items in a set
+pred maxMerged(input: set Statement, output: set Statement) {
+  no disj a, b: output | mergeable[a, b]
+
+  input = output or {
+    #input > #output
+    some a, b: input | some m: Statement {
+      m != a
+      m != b
+      merged[a, b, m]
+      maxMerged[input - a - b + m, output]
+    }
+  }
+}
+
+run some_interesting_maxMerged_statements {
+  some input, output: set Statement { 
+    maxMerged[input, output]
+    #input = 3
+    #output = 1
+    all x: output | x not in input
+  }
+} for 5
+
+check max_merging_does_not_change_eval {
+  all input, output: set Statement, r: Request { 
+    maxMerged[input, output] implies (allow[r, input] iff allow[r, output])
+  }
+} for 5
+
+// This used to be written the opposite way. But you know: merging is NOT unique.
+// Counterexample found by Alloy:
+//     {{ A, B, A }, {B, B, A} { A, B, B }}
+// Reduces to either:
+//     {{ AB, B, A }, { A, B, B }}
+// or {{ A, B, AB }, { B, B, A }}
+run max_merging_is_not_unique {
+  some input, m0, m1: set Statement { 
+    maxMerged[input, m0] and maxMerged[input, m1] and m0 != m1
+  }
+} for 5