-
Notifications
You must be signed in to change notification settings - Fork 4.4k
fix(iam): IAM Policies are too large to deploy #19114
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 1 commit
f8208e9
777c24d
e9b6cdc
68d3940
243f9c0
1f40baa
ef260c2
8b896d5
281df8b
a00582a
aeb902f
adf50cb
ccb192b
79f17d1
09cdce1
02274c3
ef354b4
00d0266
cc54755
e4c3a2a
8fbee24
625b2a7
8875096
3e570f0
fe4be84
812d4fb
fac4952
bdb113f
1f0b3c4
4988a90
2d2f16b
e1f701c
8eb3cfa
80d7a07
793da77
4fb02ef
37eaa56
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,116 @@ | ||
| /* | ||
| 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, and one of: | ||
| - Both have some Actions and the rest of the statements is the same | ||
| - Both have some Resources and the rest of the statements is the same | ||
| - Both have some Principals and the rest of the statements is 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/. | ||
| */ | ||
|
|
||
| --------------------------------------------------------- | ||
| -- Base Statement definitions | ||
rix0rrr marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
| enum Effect { Allow, Deny } | ||
| enum Resource { ResourceA, ResourceB } | ||
| enum Action { ActionA, ActionB } | ||
| enum Principal { PrincipalA, PrincipalB } | ||
|
Comment on lines
+21
to
+23
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe it makes sense to add three kinds of each since there are some checks at the end of the file with 3+ distinct statements?
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't think it makes a difference. Wouldn't 2 of each be enough to represent "different from the other one"? We don't need 3 to show that. |
||
|
|
||
| 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) | ||
| } | ||
|
|
||
| --------------------------------------------------------- | ||
| -- Requests and evaluations | ||
| sig Request { | ||
| principal: Principal, | ||
| resource: Resource, | ||
| action: Action, | ||
| } | ||
|
|
||
| // Whether the statement applies to the given request | ||
| pred applies[s: Statement, req: Request] { | ||
| req.principal in s.principal or req.principal not in s.notPrincipal | ||
| req.action in s.action or req.action not in s.notAction | ||
| req.resource in s.resource or 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 | ||
| } | ||
|
|
||
| --------------------------------------------------------- | ||
| -- Statement merging | ||
|
|
||
| // Helpers to assert that certain fields are the same | ||
| let sameAction[a, b] = { a.action = b.action and a.notAction = b.notAction } | ||
| let sameResource[a, b] = { a.resource = b.resource and a.notResource = b.notResource } | ||
| let samePrincipal[a, b] = { a.principal = b.principal and a.notPrincipal = b.notPrincipal } | ||
|
|
||
| // 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] { | ||
| m.effect = a.effect and m.effect = b.effect | ||
| { | ||
| // Writing 'some a.action', 'some b.action' here is critical | ||
| // This asserts we are dealing with a POSITIVE action and not | ||
| // a notAction (that's excluded by the fact on Statement that only | ||
| // one of the two can be set. | ||
| // | ||
| // We can show that we have a bug if you uncomment the next line. | ||
| some a.action and some b.action // Excludes notAction | ||
|
|
||
| // The constraint on notAction here is not necessary, because | ||
| // in practice it must always the empty set, but it is necessary to | ||
| // correctly show the bug in action if the previous line is commented out. | ||
| m.action = a.action + b.action and m.notAction = a.notAction + b.notAction | ||
| sameResource[a, b] and sameResource[b, m] | ||
| samePrincipal[a, b] and samePrincipal[b, m] | ||
| } or { | ||
| some a.resource and some b.resource // Excludes notResource | ||
| m.resource = a.resource + b.resource and m.notResource = a.notResource + b.notResource | ||
| sameAction[a, b] and sameAction[b, m] | ||
| samePrincipal[a, b] and samePrincipal[b, m] | ||
| } or { | ||
| some a.principal and some b.principal // Excludes notPrincipal | ||
| m.principal = a.principal + b.principal and m.notPrincipal = a.notPrincipal + b.notPrincipal | ||
| sameAction[a, b] and sameAction[b, m] | ||
| sameResource[a, b] and sameResource[b, m] | ||
| } | ||
| } | ||
|
|
||
| // Maximum merging of all statements in orig | ||
| pred maxMerged[orig: some Statement, merged: some Statement] { | ||
| } | ||
|
|
||
| // There are no statements so that if they are merged, | ||
| // the evaluation of the separate statements is different than the evaluation | ||
| // of the merged statement | ||
| check merging_does_not_change_evaluation { | ||
| no a: Statement, b: Statement, m: Statement, r: Request { | ||
| merged[a, b, m] | ||
| allow[r, a + b] iff not allow[r, m] | ||
| } | ||
| } for 5 | ||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. While this is very cool 🙂 What's assuring that the algorithm described here is the same as the one in the TS code?
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Isn't that always the problem with modeling languages? Careful review, I suppose
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I’ll be happy to explain this in detail btw
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Maybe good topic for a team time even?
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It would be nice if we could ensure they are side-by-side able... Like if we could annotate the TypeScript with the Alloy model pieces, and then have a tool that extracts the alloy model from the code. This way would reduce the likelihood that one side is changed without the other side being changed to match; and would hopefully make it easier to validate that the code is expressing the same thing as the model. Now - this is obviously work for a different PR, that is already more than enough things to look at in this one... |
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,25 +1,12 @@ | ||
| const LENGTH_CACHE_SYM = Symbol(); | ||
rix0rrr marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
|
||
| type IamValue = unknown | unknown[]; | ||
|
|
||
| /** | ||
| * Only the parts of the policy schema we're interested in | ||
| */ | ||
| interface StatementSchema { | ||
| readonly Sid?: string; | ||
| readonly Effect?: string; | ||
| readonly Principal?: IamValue | Record<string, IamValue>; | ||
| readonly Resource?: IamValue; | ||
| readonly Action?: IamValue; | ||
| } | ||
|
|
||
| /** | ||
| * Merge as many statements as possible to shrink the total policy doc, modifying the input array in place | ||
| */ | ||
| export function mergeStatements(statements: StatementSchema[]): StatementSchema[] { | ||
| let merges = findMerges(statements); | ||
| while (merges.length > 0) { | ||
| merges.sort((a, b) => a.sizeDelta - b.sizeDelta); // Most negative number first | ||
| merges.sort((a, b) => a.sizeDelta - b.sizeDelta); // Biggest reduction first | ||
| if (merges[0].sizeDelta >= 0) { break; } // Nothing more to be gained | ||
|
|
||
| // Apply all merges, order biggest to smallest gain | ||
|
|
@@ -28,7 +15,12 @@ export function mergeStatements(statements: StatementSchema[]): StatementSchema[ | |
| statements[merge.i0] = merge.combined; | ||
| statements.splice(merge.i1, 1); | ||
|
|
||
| // This invalidates all merges involving i0 or i1, and adjusts all indices > i1 | ||
| // Optimization: we can still merges that are for other pairs in this same | ||
| // go-around (which saves us recalculating all merge pairs again). We will | ||
| // need to adjust indices because we just changed the input array. | ||
| // | ||
| // The following removes all merges involving i0 or i1 (no longer valid, | ||
| // these have been used up), and shifts all indices > i1 left by 1. | ||
| // Assumes i0 < i1. | ||
| const invalidIndices = [merge.i0, merge.i1]; | ||
| let j = 0; | ||
|
|
@@ -48,6 +40,9 @@ export function mergeStatements(statements: StatementSchema[]): StatementSchema[ | |
| return statements; | ||
| } | ||
|
|
||
| /** | ||
| * Return all possible merges between all pairs of statements in the input array | ||
| */ | ||
| function findMerges(statements: StatementSchema[]): StatementMerge[] { | ||
| const ret = new Array<StatementMerge>(); | ||
| for (let i0 = 0; i0 < statements.length; i0++) { | ||
|
|
@@ -62,7 +57,9 @@ function tryMerge(statements: StatementSchema[], i0: number, i1: number, into: S | |
| const a = statements[i0]; | ||
| const b = statements[i1]; | ||
|
|
||
| if (a.Effect !== 'Allow' || b.Effect !== 'Allow') { return; } | ||
| // Effects must be the same | ||
| if (a.Effect !== b.Effect) { return; } | ||
| // We don't merge Sids (for now) | ||
| if (a.Sid || b.Sid) { return; } | ||
rix0rrr marked this conversation as resolved.
Outdated
Show resolved
Hide resolved
|
||
|
|
||
| const beforeLen = jsonLength(a) + jsonLength(b); | ||
|
|
@@ -175,6 +172,19 @@ function normalizedArray(...xs: unknown[]) { | |
| return Array.from(new Set(xs)).sort(); | ||
| } | ||
|
|
||
| type IamValue = unknown | unknown[]; | ||
|
|
||
| /** | ||
| * Only the parts of the policy schema we're interested in | ||
| */ | ||
| interface StatementSchema { | ||
|
||
| readonly Sid?: string; | ||
| readonly Effect?: string; | ||
| readonly Principal?: IamValue | Record<string, IamValue>; | ||
| readonly Resource?: IamValue; | ||
| readonly Action?: IamValue; | ||
| } | ||
|
|
||
| interface StatementMerge { | ||
| /** | ||
| * Index of statement 0 | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.