diff --git a/README.md b/README.md index 77f132c..4d7e2ae 100644 --- a/README.md +++ b/README.md @@ -52,6 +52,7 @@ Many `writ check` runs **exit 1** on purpose: a failing property is a finding | [`oversight/`](oversight/) | Can lawful moves permanently stop a case concluding? | Not as written; repeal one power and `writ compare` shows accountability **LOST**. | | [`workflow/`](workflow/) | Can a KYC case ever get stuck? | Never — and where automation ends, a declared gap hands it to a human. | | [`access/`](access/) | Can an admin grant always be revoked? | No: the break-glass grant is a latch. | +| [`entitlement-problems/`](entitlement-problems/) | Can a requester approve, a developer edit CloudTrail, a leaver keep admin? | Yes, each through steps that are fine one at a time. writ names who, and through which grants. | | [`two-phase-commit/`](two-phase-commit/) | Do the parties agree, and must they decide? | Always agree; a coordinator crash can strand them. Variants price a timeout and a lossy network. | **Design, judgement and change** diff --git a/docker-compose.yml b/docker-compose.yml index 41dfc88..754ec7a 100644 --- a/docker-compose.yml +++ b/docker-compose.yml @@ -59,6 +59,24 @@ services: image: writ-problems command: ["access"] + # Separation of duties: the toxic-combination table, and the role it misses. + separation-of-duties: + build: . + image: writ-problems + command: ["separation_of_duties"] + + # An OU move that leaves the guardrails behind — `writ compare` reports LOST. + scp-escalation: + build: . + image: writ-problems + command: ["scp_escalation"] + + # Group-based offboarding, and the direct grant that survives it. + joiner-mover-leaver: + build: . + image: writ-problems + command: ["joiner_mover_leaver"] + # A timetable CP-SAT decided, audited: one state, two broken school rules, # two questions the curriculum never answered. timetable: diff --git a/entitlement-problems/README.md b/entitlement-problems/README.md new file mode 100644 index 0000000..442fdc2 --- /dev/null +++ b/entitlement-problems/README.md @@ -0,0 +1,53 @@ +# Entitlement problems + +Three access-control designs, each with a control that reads correctly and +lets a privilege through anyway. Each directory writes the design down as a +writ model and checks every reachable configuration, not one access decision. +The safe version passes. A version with one condition removed (or, in +`scp-escalation/`, one administrative step added) fails, and writ names the +broken guarantee, the shortest sequence of grants or administrative steps +that reaches it, and who is affected. + +| problem | the mistake | route to the fault | +| --- | --- | --- | +| [`separation-of-duties/`](separation-of-duties/) | checking grants against a table of group names, when the conflict lives in a role | 2 grants | +| [`scp-escalation/`](scp-escalation/) | moving an account between OUs, which swaps the SCP guardrails out from under its roles | 1–2 steps | +| [`joiner-mover-leaver/`](joiner-mover-leaver/) | offboarding through groups, which cannot see a direct assignment | 4 steps | + +Start with `separation-of-duties/`. Each directory holds the two models, one +`.claims` file asked of both, a `.rules` file that answers the same questions +through `writ derive` as a cross-check (`../modality-cross-check.sh`) and +prints the privilege path as a table, and a README. + +What the three have in common: + +- **The mistake is never in one grant.** Every individual step is legitimate: + joining a group, assuming a role, moving an account, offboarding a leaver. + The privilege exists only in the composition. +- **The unsafe version still works.** People can still be given access and + deploys still ship, so every question except "is it safe at every step" + answers in its favour. +- **The answer is in the domain's vocabulary.** Each failing property names + a query with `(show …)`, so the verdict says *who* (`a = alice`, + `p = dev`, `e = prod-admin`), and each `.rules` file adds *through what*: + the two groups, the role → account → OU path, the grant marked `direct`. + +`writ compare` reports the difference between the two models of each pair as +guarantees `LOST`, exit 1. In `scp-escalation/` that is the natural gate, +because the change *is* the difference: one administrative step added. One +caution: an equation that both files declare compares as `preserved` even when +one of them violates it (`separation` in `separation-of-duties/`), because +`compare` matches laws by declaration. Ask the safety question as a property +if `compare` is your gate. + +From any of the directories (here, `separation-of-duties/`): + +```sh +writ check separation-of-duties.writ --claims separation-of-duties.claims # exit 0 +writ check separation-of-duties-shortcut.writ --claims separation-of-duties.claims # exit 1 +``` + +These are deliberately small, a few hundred situations at most, and each +README says what its reduction leaves out. A model built from a real IAM +export is the job of a bridge that reads the policies and writes the model. +That is a separate tool, not a scenario. diff --git a/entitlement-problems/joiner-mover-leaver/README.md b/entitlement-problems/joiner-mover-leaver/README.md new file mode 100644 index 0000000..ef5d742 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/README.md @@ -0,0 +1,174 @@ +# Joiner, mover, leaver: the grant offboarding cannot see + +Access follows a person through a job. They join and request access, someone +approves, and it is provisioned. Later they move to another team or leave, +and the access should go. The usual rule is "access is managed through +groups": provisioning adds the person to groups, and offboarding takes them +out. When the HR system's leaving date arrives, an automated integration +removes the person from every group the same day. + +That covers every grant made through a group. It does not cover the grant +made directly, on the day the request needed something no group yet mapped +to: the administrator permission set assigned to one person by name. +Offboarding works on groups, and nothing that works on groups can see it. + +## The model + +[`joiner-mover-leaver.writ`](joiner-mover-leaver.writ) follows one person and +one request: + +- **people**: `ada` (joins the platform team, needs production) and `bob` + (her manager), each with a `status` (`active`, `left`) and a `team` + (`platform`, `marketing`); +- **entitlements**: `prod-engineers`, the identity provider's production + group, which syncs to AWS, and `prod-admin`, the administrator permission + set assigned to Ada directly. Each records `via` (`group` or `direct`) and + its holder; +- **the request** `ada-prod`, with its stage (`none` → `requested` → + `approved` → `provisioned`) and its approver. + +The moves are the lifecycle: `ada-requests-prod`, `bob-approves` (and +`ada-approves`, whose guard refuses her own request), `provision-ada` (grants +both entitlements), `ada-moves-to-marketing` and `ada-leaves`. The mover and +leaver steps run their own deprovisioning in the same step, as an HR-driven +SCIM integration does. + +Two laws about the request hold in both plans: + +- `provisioned-means-approved`: nothing is provisioned that nobody approved; +- `no-self-approval`: the approver is not the requester. + +The two files differ in what deprovisioning removes. The safe plan removes +both entitlements: + +```lisp +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) +``` + +[`joiner-mover-leaver-shortcut.writ`](joiner-mover-leaver-shortcut.writ) +removes only the group membership, in both the mover and the leaver step. + +## What writ answers + +Both plans are asked the questions in +[`joiner-mover-leaver.claims`](joiner-mover-leaver.claims). The safe plan, +exit 0: + +``` +states: 16 edges: 19 +regime: committing — no move can be undone +… +holds ada-gets-access +holds movers-lose-prod +holds leavers-lose-everything +holds leavers-can-be-cut-off +certified: every answer re-derived from the model (writ-cert) +``` + +The shortcut, exit 1: + +``` +fails leavers-lose-everything + "nobody who has left ever holds production access" + witness: 1. ada-requests-prod → #1 ada-prod.stage: none → requested + 2. bob-approves → #4 ada-prod.stage: requested → approved, ada-prod.approver: ∅ → bob + 3. provision-ada → #8 prod-engineers.holder: ∅ → ada, prod-admin.holder: ∅ → ada, ada-prod.stage: approved → provisioned + 4. ada-leaves → #13 ada.status: active → left, prod-engineers.holder: ada → ∅ + stranded (at state 13) + e = prod-admin +fails leavers-can-be-cut-off + "from every reachable situation, a leaver can still end up holding nothing" + stuck at: #13 (ada.status=left … prod-engineers.holder=∅ prod-admin.holder=ada …) +``` + +Read the witness as an incident timeline. Each line says what changed. Step 4 +shows the leaver step doing its job: the group membership goes. The +administrator permission set is not in that line, because nothing removed it. +`stranded` answers the query the property names: what is left behind. + +`leavers-can-be-cut-off` fails as well, which makes this a **trap**, not a +delay. At situation 13 nothing that can still run touches a direct grant. No +later batch job or second pass will fix it, because there isn't one. The +mover fails the same way (`movers-lose-prod`, ending in +`ada-moves-to-marketing`). A person who changes team keeps production admin +indefinitely, which is how privilege creep happens. + +## What is left behind + +[`joiner-mover-leaver.rules`](joiner-mover-leaver.rules) lists every +entitlement held by someone with no business holding it, with how it was +granted: + +```sh +writ derive joiner-mover-leaver-shortcut.writ joiner-mover-leaver.rules left-behind +``` + +``` +left-behind (3 rows) + 12 prod-admin direct ada + 13 prod-admin direct ada + 15 prod-admin direct ada +``` + +The `via` column is the finding: every row says `direct`. + +## What writ found while this was being written + +The first draft of the safe plan had a second bug, and writ reported it before +the shortcut existed. `provision-ada` checked only that the request was +approved. The report, with each step's change column trimmed: + +``` +fails leavers-lose-everything + witness: 1. ada-requests-prod + 2. bob-approves + 3. ada-leaves + 4. provision-ada + stranded (at state 16) + e = prod-engineers + e = prod-admin +``` + +Approve, leave, *then* provision: an approval is a judgement about someone in +a role, and this one outlived the situation it judged. The fix, in both files, +is that provisioning re-checks the person (`ada.status active`, +`ada.team platform`) as well as the request. Queued provisioning jobs and +approvals that sit in a ticket for a week make this a real gap, and it is +easy to miss because every step is correct in the order the runbook shows. + +## Why the law is written from the entitlement's side + +"No leaver holds anything" would naturally be written about the person. writ +cannot put a type name on the right of `is`, so the property is written from +the other end of the arrow: no *entitlement* has a holder whose status is +`left`. The forms `held-by-leaver` and `held-outside-platform` in +[`joiner-mover-leaver.lib.writ`](joiner-mover-leaver.lib.writ) say so once, +for the claims and the rules alike. + +## What to take away + +The unsafe plan is the one the runbook describes, and it is right about every +grant it can see. The grant that survives was made outside the mechanism +offboarding relies on, for a good reason, on a busy day. The fix is either to +remove direct grants by name in every lifecycle step, as the safe plan does, +or to forbid them. Either way, the question to ask of the process is "can a +leaver still hold anything", not "did offboarding run". + +To adapt it, add an entitlement per system access can live in (Vault +policies, SaaS seats, SSH keys) with its real `via`, and say in each lifecycle +step what it actually removes. + +## Run it + +```sh +writ check joiner-mover-leaver.writ --claims joiner-mover-leaver.claims # exit 0 +writ check joiner-mover-leaver-shortcut.writ --claims joiner-mover-leaver.claims # exit 1 +``` + +`../../modality-cross-check.sh` checks the `.rules` encoding against `writ +check`. Siblings: [`../separation-of-duties/`](../separation-of-duties/), +[`../scp-escalation/`](../scp-escalation/). diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ new file mode 100644 index 0000000..864012f --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver-shortcut.writ @@ -0,0 +1,113 @@ +; The same lifecycle, with ONE THING MISSING from the mover and leaver steps: +; they remove Ada from her groups, and nothing else. +; +; That is what group-based offboarding does, and it is what the runbook says: +; "access is managed through groups". It is true of every grant made through a +; group. The administrator permission set was assigned directly, on the day +; the request needed it, and nothing that acts on groups can see it. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "joiner-mover-leaver.lib.writ") + +(schema joiner-mover-leaver + + (type status (active left)) + (type team (platform marketing)) + + (type person + (arrow status (to status)) + (arrow team (to team))) + + ; How a grant was made, which decides what removes it. A `group` grant goes + ; when the person leaves the group; a `direct` one goes only when someone + ; removes it by name. + (type via-t (group direct)) + + ; A production entitlement, and who holds it. + (type entitlement + (arrow via (to via-t) fixed) + (maybe holder person)) + + (type stage (none requested approved provisioned)) + + ; The one access request this model follows. + (type request + (arrow requester (to person) fixed) + (arrow stage (to stage)) + (maybe approver person)) + + ; ---- the rules of the request ---- + + ; Nothing is provisioned that nobody approved. + (equation provisioned-means-approved + (not (and (is request.stage provisioned) (not (defined request.approver))))) + + ; Nobody approves their own request. + (equation no-self-approval + (not (is request.approver request.requester)))) + +(instance start joiner-mover-leaver + + (person ada (status active) (team platform)) ; joins, needs production + (person bob (status active) (team platform)) ; her manager + + ; The production group in the identity provider. Its membership syncs to + ; AWS IAM Identity Center and grants the engineers' permission set. + (entitlement prod-engineers (via group) (holder vacant)) + ; The administrator permission set on the production account, assigned to + ; the person directly: at the time, no group mapped to it, and the request + ; needed it that day. + (entitlement prod-admin (via direct) (holder vacant)) + + (request ada-prod (requester ada) (stage none) (approver vacant))) + +(use joiner-mover-leaver) +(initial start) + +; ---- joiner ---- + +(transition ada-requests-prod + (when (and (is ada-prod.stage none) (is ada.status active))) + (do (set ada-prod.stage requested))) + +; Whoever approves must not be the requester. Each possible approver is a move +; of its own, so the guard can say so. +(form (approve-by N P) + (transition N + (when (and (is ada-prod.stage requested) + (is P.status active) + (not (is ada-prod.requester P)))) + (do (set ada-prod.stage approved) (set ada-prod.approver P)))) +(approve-by ada-approves ada) ; never fires: she is the requester +(approve-by bob-approves bob) + +; Provisioning re-checks the person, not only the request. An approval is a +; judgement about someone in a role; if they have since moved or left, the +; approval is about a situation that no longer exists. (The first draft of +; this file did not re-check, and writ found it: approve, leave, provision — +; access granted to someone who had already gone. See the README.) +(transition provision-ada + (when (and (is ada-prod.stage approved) + (is ada.status active) + (is ada.team platform))) + (do (set ada-prod.stage provisioned) + (set prod-engineers.holder ada) + (set prod-admin.holder ada))) + +; ---- mover and leaver ---- + +; Each lifecycle event runs its own deprovisioning, the way an HR-driven +; (SCIM) integration does: the change of team or the leaving date arrives, and +; access is removed in the same step. It removes the person from their groups, +; which is what the integration knows how to do. +(transition ada-moves-to-marketing + (when (and (is ada.status active) (is ada.team platform))) + (do (set ada.team marketing) + (vacate prod-engineers.holder))) ; <- prod-admin, not removed + +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder))) ; <- prod-admin, not removed diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims new file mode 100644 index 0000000..fb37e1f --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.claims @@ -0,0 +1,36 @@ +; The questions, put to both plans. + +(load "joiner-mover-leaver.lib.writ") + +(property ada-gets-access + "the request can end with Ada holding production access" + (possible (and (is prod-engineers.holder ada) (is prod-admin.holder ada)))) + +(property movers-lose-prod + "nobody off the platform team ever holds production access" + (never (some (e entitlement) (held-outside-platform e))) + (show stranded)) + +(property leavers-lose-everything + "nobody who has left ever holds production access" + (never (some (e entitlement) (held-by-leaver e))) + (show stranded)) + +(property leavers-can-be-cut-off + "from every reachable situation, a leaver can still end up holding nothing" + (live (or (is ada.status active) + (and (not (defined prod-engineers.holder)) + (not (defined prod-admin.holder)))))) + +; ---- what is left behind ---- +(query stranded + (where (e entitlement)) + (or (held-outside-platform e) (held-by-leaver e))) + +; ---- ownership ---- +; The request's own steps are what can break its rules; their guards are what +; keep them. Each is acknowledged, and neither rule is violated in either plan. +(accept ada-requests-prod provisioned-means-approved) +(accept ada-approves provisioned-means-approved no-self-approval) +(accept bob-approves provisioned-means-approved no-self-approval) +(accept provision-ada provisioned-means-approved) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ new file mode 100644 index 0000000..dd7d791 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.lib.writ @@ -0,0 +1,11 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +; E is held by someone who is no longer entitled to production: they have +; left, or they have moved off the platform team. Written from the +; entitlement's side, because a type name cannot be the right of `is`. +(form (held-by-leaver E) + (and (defined E.holder) (is E.holder.status left))) +(form (held-outside-platform E) + (and (defined E.holder) (is E.holder.team marketing))) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules new file mode 100644 index 0000000..e4be8f3 --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.rules @@ -0,0 +1,39 @@ +; The same four questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "joiner-mover-leaver.lib.writ") + +(satisfies ada-gets-access + (and (is prod-engineers.holder ada) (is prod-admin.holder ada))) + +(satisfies movers-lose-prod (some (e entitlement) (held-outside-platform e))) + +(satisfies leavers-lose-everything (some (e entitlement) (held-by-leaver e))) + +(satisfies cut-off + (or (is ada.status active) + (and (not (defined prod-engineers.holder)) + (not (defined prod-admin.holder))))) +(can-reach can-cut-off cut-off) +(trapped leavers-can-be-cut-off can-cut-off) + +; ---- the explanation ---- +; Every entitlement still held by someone with no business holding it: the +; situation, the entitlement, how it was granted, and who holds it. The `via` +; column is the finding — every row says `direct`. +(relation left-behind (Situation entitlement via-t person)) +(rule (left-behind S E V P) + (situation S) + (holds S (is E.holder P)) + (holds S (is P.status left)) + (is E.via V)) +(rule (left-behind S E V P) + (situation S) + (holds S (is E.holder P)) + (holds S (is P.team marketing)) + (is E.via V)) diff --git a/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ new file mode 100644 index 0000000..e30dbdf --- /dev/null +++ b/entitlement-problems/joiner-mover-leaver/joiner-mover-leaver.writ @@ -0,0 +1,118 @@ +; Joiner, mover, leaver — access that follows a person through a job. +; +; Ada joins the platform team and requests production access. Her manager +; approves; provisioning gives her two things: membership of the production +; group, and an administrator permission set assigned to her directly, because +; no group mapped to it at the time. Later she moves to another team, or +; leaves. +; +; Offboarding is automatic: the HR system's event removes her access in the +; same step. In this plan it removes everything she holds, by name. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "joiner-mover-leaver.lib.writ") + +(schema joiner-mover-leaver + + (type status (active left)) + (type team (platform marketing)) + + (type person + (arrow status (to status)) + (arrow team (to team))) + + ; How a grant was made, which decides what removes it. A `group` grant goes + ; when the person leaves the group; a `direct` one goes only when someone + ; removes it by name. + (type via-t (group direct)) + + ; A production entitlement, and who holds it. + (type entitlement + (arrow via (to via-t) fixed) + (maybe holder person)) + + (type stage (none requested approved provisioned)) + + ; The one access request this model follows. + (type request + (arrow requester (to person) fixed) + (arrow stage (to stage)) + (maybe approver person)) + + ; ---- the rules of the request ---- + + ; Nothing is provisioned that nobody approved. + (equation provisioned-means-approved + (not (and (is request.stage provisioned) (not (defined request.approver))))) + + ; Nobody approves their own request. + (equation no-self-approval + (not (is request.approver request.requester)))) + +(instance start joiner-mover-leaver + + (person ada (status active) (team platform)) ; joins, needs production + (person bob (status active) (team platform)) ; her manager + + ; The production group in the identity provider. Its membership syncs to + ; AWS IAM Identity Center and grants the engineers' permission set. + (entitlement prod-engineers (via group) (holder vacant)) + ; The administrator permission set on the production account, assigned to + ; the person directly: at the time, no group mapped to it, and the request + ; needed it that day. + (entitlement prod-admin (via direct) (holder vacant)) + + (request ada-prod (requester ada) (stage none) (approver vacant))) + +(use joiner-mover-leaver) +(initial start) + +; ---- joiner ---- + +(transition ada-requests-prod + (when (and (is ada-prod.stage none) (is ada.status active))) + (do (set ada-prod.stage requested))) + +; Whoever approves must not be the requester. Each possible approver is a move +; of its own, so the guard can say so. +(form (approve-by N P) + (transition N + (when (and (is ada-prod.stage requested) + (is P.status active) + (not (is ada-prod.requester P)))) + (do (set ada-prod.stage approved) (set ada-prod.approver P)))) +(approve-by ada-approves ada) ; never fires: she is the requester +(approve-by bob-approves bob) + +; Provisioning re-checks the person, not only the request. An approval is a +; judgement about someone in a role; if they have since moved or left, the +; approval is about a situation that no longer exists. (The first draft of +; this file did not re-check, and writ found it: approve, leave, provision — +; access granted to someone who had already gone. See the README.) +(transition provision-ada + (when (and (is ada-prod.stage approved) + (is ada.status active) + (is ada.team platform))) + (do (set ada-prod.stage provisioned) + (set prod-engineers.holder ada) + (set prod-admin.holder ada))) + +; ---- mover and leaver ---- + +; Each lifecycle event runs its own deprovisioning, the way an HR-driven +; (SCIM) integration does: the change of team or the leaving date arrives, and +; access is removed in the same step. Both remove the group membership AND the +; direct assignment. +(transition ada-moves-to-marketing + (when (and (is ada.status active) (is ada.team platform))) + (do (set ada.team marketing) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) + +(transition ada-leaves + (when (is ada.status active)) + (do (set ada.status left) + (vacate prod-engineers.holder) + (vacate prod-admin.holder))) diff --git a/entitlement-problems/scp-escalation/README.md b/entitlement-problems/scp-escalation/README.md new file mode 100644 index 0000000..5a24399 --- /dev/null +++ b/entitlement-problems/scp-escalation/README.md @@ -0,0 +1,169 @@ +# An OU move that leaves the guardrails behind + +In AWS Organizations, a *service control policy* (SCP) is attached to an +organizational unit (OU) and caps what any role in that OU's accounts can do. +It never grants anything; it only takes away. Teams lean on that: the roles +inside a production account are broad, because the production OU's SCP denies +the few things nobody should do there, like switching off CloudTrail. + +So the guardrail belongs to the OU, not to the account. Move the account to +another OU, as a reorganisation does, and it leaves its guardrails behind and +picks up whatever the new OU carries. No role changes and no IAM policy is +edited. The change is drag-and-drop in the console, reviewed as an +organizational chore. + +## Before and after + +`writ compare` checks one set of questions against both versions of the +organization: + +```sh +writ compare scp-escalation.writ scp-escalation-restructured.writ # exit 1 +``` + +``` +equations: +properties: dev-can-deploy preserved + dev-never-edits-cloudtrail LOST witness: 1. dev-assumes-power 2. move-prod-to-workloads + sec-can-always-audit LOST witness: 1. move-prod-to-workloads +``` + +Deploying still works. Two guarantees are gone, each with the shortest route to +where it fails: + +- **Developers can now modify CloudTrail.** An engineer signed in as `power` + (PowerUserAccess, which includes CloudTrail) was held back only by the + production OU's SCP. After the move, nothing holds them back. +- **The security team is locked out of production's audit trail.** No sign-in + is needed for this one: the move alone does it, and nothing moves the account + back. + +The properties come from [`scp-escalation.claims`](scp-escalation.claims), +beside the original. `compare` reads the questions from there and asks them of +both files. A `LOST` line exits 1, so the comparison is a gate a pipeline can +run on every change to the organization model. + +## The model, and what it leaves out + +[`scp-escalation.writ`](scp-escalation.writ) keeps only what the three +questions need: + +- **Three actions**: `prod-write`, `cloudtrail-edit`, `audit-read`. +- **OUs** as one deny flag per action. `production` denies CloudTrail edits. + `security` denies production writes. `workloads` is new: its SCPs were copied + from the sandbox template, which has no CloudTrail guardrail and denies access + from outside the unit (the security team's read is cross-account). +- **Accounts**: `prod-acct` in `production`, `sec-acct` in `security`. Which OU + an account sits in is the one thing an administrator changes here. +- **Roles**, each living in one account with fixed grants: `deploy`, `power`, + `audit-reader`, all in `prod-acct`. +- **Principals** `dev` and `sec`, and the role each is signed in as, if any. + +Who may assume which role is listed rather than computed: one move per trust +relationship (`dev-assumes-deploy`, `dev-assumes-power`, +`sec-assumes-audit-reader`), plus signing out. + +AWS evaluation is reduced to one conjunction, in +[`scp-escalation.lib.writ`](scp-escalation.lib.writ): the role grants the +action **and** the role's account's OU does not deny it. + +```lisp +(form (edits-cloudtrail P) + (and (is P.assumed.cloudtrail-edit yes) + (is P.assumed.in.ou.deny-cloudtrail-edit no))) +``` + +Left out: permission boundaries, resource policies, session policies, explicit +denies in identity policies, nested OUs and SCP inheritance, conditions, and +every action not named above. Each would be another conjunct in those forms. +A reader whose question depends on them needs a bridge that reads real policy +and writes the model. That is a separate tool, not this scenario. + +[`scp-escalation-restructured.writ`](scp-escalation-restructured.writ) is the +same file plus one transition: + +```lisp +(transition move-prod-to-workloads + (when (is prod-acct.ou production)) + (do (set prod-acct.ou workloads))) +``` + +## Checking each version + +The original, exit 0: + +``` +states: 6 edges: 14 +… +holds dev-can-deploy +holds dev-never-edits-cloudtrail +holds sec-can-always-audit +``` + +The restructured one, exit 1: + +``` +states: 12 edges: 34 +… +fails dev-never-edits-cloudtrail + "developers cannot modify CloudTrail" + witness: 1. dev-assumes-power → #2 dev.assumed: ∅ → power + 2. move-prod-to-workloads → #8 prod-acct.ou: production → workloads + cloudtrail-editors (at state 8) + p = dev +fails sec-can-always-audit + "whatever has happened, the security team can still get to production's audit trail" + stuck at: #4 (prod-acct.ou=workloads sec-acct.ou=security dev.assumed=∅ sec.assumed=∅) + witness: 1. move-prod-to-workloads → #4 prod-acct.ou: production → workloads + audit-readers (at state 4) +``` + +The CloudTrail witness happens in the order it would in practice. An engineer +is already signed in as `power` when the account moves, and their session +gains the capability without them doing anything. `audit-readers` at state 4 +is empty: once the account has moved, nobody can read the trail, now or later. + +## The privilege path + +[`scp-escalation.rules`](scp-escalation.rules) lays out every effective +CloudTrail edit as a path: the principal, the role it assumed, the account the +role lives in, and the OU whose SCP failed to stop it. + +```sh +writ derive scp-escalation-restructured.writ scp-escalation.rules escalation +``` + +``` +escalation (2 rows) + 8 dev power prod-acct workloads + 11 dev power prod-acct workloads +``` + +Read across a row: dev → power → prod-acct → workloads. The guardrail was the +last hop, and the move replaced it. + +## What to take away + +Guardrails that live on a container travel with the container, not with what +is in it. A review of the IAM change finds nothing, because there is no IAM +change. A review of the OU move sees a chore. Neither file says which +guarantees depended on which OU. Asking the same questions before and after +does. + +`check` on the new model fails too, but `compare` is the gate that fits the +change. Its subject is a difference: it says which guarantees the +reorganisation took away, and keeps the ones it did not. + +## Run it + +```sh +writ check scp-escalation.writ --claims scp-escalation.claims # exit 0 +writ check scp-escalation-restructured.writ --claims scp-escalation.claims # exit 1 +writ compare scp-escalation.writ scp-escalation-restructured.writ # exit 1 +``` + +With the organization model under git, `writ compare --git HEAD~1 HEAD +scp-escalation.writ` asks the same questions across two commits. +`../../modality-cross-check.sh` checks the `.rules` encoding against `writ +check`. Siblings: [`../separation-of-duties/`](../separation-of-duties/), +[`../joiner-mover-leaver/`](../joiner-mover-leaver/). diff --git a/entitlement-problems/scp-escalation/scp-escalation-restructured.writ b/entitlement-problems/scp-escalation/scp-escalation-restructured.writ new file mode 100644 index 0000000..ec7c7b7 --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation-restructured.writ @@ -0,0 +1,95 @@ +; The same organization, with ONE MOVE ADDED: the reorganisation moves the +; production account into the new `workloads` OU. +; +; Nothing about any role changes, and no IAM policy is edited. The move is a +; one-line change in the console, reviewed as an organizational chore. But an +; SCP is attached to an OU, not to an account, so the account leaves its +; guardrails behind and picks up new ones. +; +; Compare it with the original: `writ compare scp-escalation.writ +; scp-escalation-restructured.writ` exits 1 and names what was lost. + +(load "stdlib.writ") +(load "scp-escalation.lib.writ") + +(schema scp-escalation + + (type yn (no yes)) + + ; An organizational unit, reduced to its service control policy: for each of + ; the three actions the questions are about, does the SCP deny it? An SCP + ; never grants anything. It only takes away. + (type ou + (arrow deny-prod-write (to yn) fixed) + (arrow deny-cloudtrail-edit (to yn) fixed) + (arrow deny-audit-read (to yn) fixed)) + + ; Which OU an account sits in is the one thing an administrator changes here. + (type account (arrow ou (to ou))) + + ; An IAM role lives in one account and grants a fixed set of actions. Whether + ; a grant is effective depends on the account's OU, which is not the role's + ; business, and that is the gap the questions probe. + (type role + (arrow in (to account) fixed) + (arrow prod-write (to yn) fixed) + (arrow cloudtrail-edit (to yn) fixed) + (arrow audit-read (to yn) fixed)) + + ; A person, and the role they are currently signed in as, if any. + (type principal (maybe assumed role))) + +(instance start scp-escalation + + ; The guardrails. Production's SCP denies CloudTrail changes, so no role in + ; a production account can switch off the audit trail, however broad its + ; IAM policy. The security OU's denies production writes. + (ou security (deny-prod-write yes) (deny-cloudtrail-edit no) (deny-audit-read no)) + (ou production (deny-prod-write no) (deny-cloudtrail-edit yes) (deny-audit-read no)) + ; Created for the reorganisation, with its SCPs copied from the sandbox + ; template: no CloudTrail guardrail (sandboxes are disposable) and no access + ; from outside the unit (sandboxes are isolated), which is where the security + ; team's cross-account read comes from. + (ou workloads (deny-prod-write no) (deny-cloudtrail-edit no) (deny-audit-read yes)) + + (account prod-acct (ou production)) + (account sec-acct (ou security)) + + ; Deploys to production. + (role deploy (in prod-acct) (prod-write yes) (cloudtrail-edit no) (audit-read no)) + ; The broad role engineers use to debug production. Its IAM policy is + ; PowerUserAccess, which includes CloudTrail. Nobody narrowed it, because + ; the production OU's SCP already denies CloudTrail changes. + (role power (in prod-acct) (prod-write yes) (cloudtrail-edit yes) (audit-read no)) + ; How the security team reads production's audit trail: a role inside the + ; production account that their own account is trusted to assume. + (role audit-reader (in prod-acct) (prod-write no) (cloudtrail-edit no) (audit-read yes)) + + (principal dev (assumed vacant)) + (principal sec (assumed vacant))) + +(use scp-escalation) +(initial start) + +; ---- signing in and out ---- + +; One move per trust relationship, written out: who may assume which role is +; wiring, and wiring is listed rather than computed. +(form (assume N P R) + (transition N (when (not (defined P.assumed))) (do (set P.assumed R)))) +(form (sign-out N P) + (transition N (when (defined P.assumed)) (do (vacate P.assumed)))) + +(assume dev-assumes-deploy dev deploy) +(assume dev-assumes-power dev power) +(assume sec-assumes-audit-reader sec audit-reader) +(sign-out dev-signs-out dev) +(sign-out sec-signs-out sec) + +; ---- the reorganisation ---- + +; Moving an account between OUs. In the console it is drag and drop. Nothing +; moves it back; the reorganisation is not undone. +(transition move-prod-to-workloads + (when (is prod-acct.ou production)) + (do (set prod-acct.ou workloads))) diff --git a/entitlement-problems/scp-escalation/scp-escalation.claims b/entitlement-problems/scp-escalation/scp-escalation.claims new file mode 100644 index 0000000..896e9e0 --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.claims @@ -0,0 +1,22 @@ +; The questions, held fixed across the reorganisation. `writ compare` reads +; them from here for both models. + +(load "scp-escalation.lib.writ") + +(property dev-can-deploy + "a developer can still ship to production" + (possible (writes-prod dev))) + +(property dev-never-edits-cloudtrail + "developers cannot modify CloudTrail" + (never (edits-cloudtrail dev)) + (show cloudtrail-editors)) + +(property sec-can-always-audit + "whatever has happened, the security team can still get to production's audit trail" + (live (reads-audit sec)) + (show audit-readers)) + +; ---- who ---- +(query cloudtrail-editors (where (p principal)) (edits-cloudtrail p)) +(query audit-readers (where (p principal)) (reads-audit p)) diff --git a/entitlement-problems/scp-escalation/scp-escalation.lib.writ b/entitlement-problems/scp-escalation/scp-escalation.lib.writ new file mode 100644 index 0000000..8963b1f --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.lib.writ @@ -0,0 +1,21 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +; What a principal can effectively do: the role it has assumed grants the +; action, AND the service control policy of the OU that role's account sits in +; does not deny it. That conjunction is the whole of the AWS evaluation this +; model keeps (see the README for what it leaves out). +; +; One form per action, because a form parameter cannot name an arrow. +(form (writes-prod P) + (and (is P.assumed.prod-write yes) + (is P.assumed.in.ou.deny-prod-write no))) + +(form (edits-cloudtrail P) + (and (is P.assumed.cloudtrail-edit yes) + (is P.assumed.in.ou.deny-cloudtrail-edit no))) + +(form (reads-audit P) + (and (is P.assumed.audit-read yes) + (is P.assumed.in.ou.deny-audit-read no))) diff --git a/entitlement-problems/scp-escalation/scp-escalation.rules b/entitlement-problems/scp-escalation/scp-escalation.rules new file mode 100644 index 0000000..0a3195e --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.rules @@ -0,0 +1,30 @@ +; The same three questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "scp-escalation.lib.writ") + +(satisfies dev-can-deploy (writes-prod dev)) + +(satisfies dev-never-edits-cloudtrail (edits-cloudtrail dev)) + +(satisfies sec-audits (reads-audit sec)) +(can-reach can-audit sec-audits) +(trapped sec-can-always-audit can-audit) + +; ---- the explanation ---- +; Every effective CloudTrail edit, as a privilege path: the situation, the +; principal, the role it assumed, the account that role lives in, and the OU +; that account sits in at that moment, whose SCP did not stop it. +(relation escalation (Situation principal role account ou)) +(rule (escalation S P R A O) + (situation S) + (holds S (is P.assumed R)) + (is R.cloudtrail-edit yes) + (is R.in A) + (holds S (is A.ou O)) + (is O.deny-cloudtrail-edit no)) diff --git a/entitlement-problems/scp-escalation/scp-escalation.writ b/entitlement-problems/scp-escalation/scp-escalation.writ new file mode 100644 index 0000000..838cc5c --- /dev/null +++ b/entitlement-problems/scp-escalation/scp-escalation.writ @@ -0,0 +1,89 @@ +; An AWS organization, before a reorganisation. +; +; Production sits in the `production` OU, whose service control policy denies +; CloudTrail changes. The roles inside the production account are broad, +; because the SCP is the guardrail: an engineer signed in as `power` has +; PowerUserAccess, and the SCP takes CloudTrail back out of it. +; +; A new `workloads` OU exists, created for a reorganisation, but nothing has +; been moved into it yet. `scp-escalation-restructured.writ` is this file plus +; the one administrative step that moves production there. +; +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "scp-escalation.lib.writ") + +(schema scp-escalation + + (type yn (no yes)) + + ; An organizational unit, reduced to its service control policy: for each of + ; the three actions the questions are about, does the SCP deny it? An SCP + ; never grants anything. It only takes away. + (type ou + (arrow deny-prod-write (to yn) fixed) + (arrow deny-cloudtrail-edit (to yn) fixed) + (arrow deny-audit-read (to yn) fixed)) + + ; Which OU an account sits in is the one thing an administrator changes here. + (type account (arrow ou (to ou))) + + ; An IAM role lives in one account and grants a fixed set of actions. Whether + ; a grant is effective depends on the account's OU, which is not the role's + ; business, and that is the gap the questions probe. + (type role + (arrow in (to account) fixed) + (arrow prod-write (to yn) fixed) + (arrow cloudtrail-edit (to yn) fixed) + (arrow audit-read (to yn) fixed)) + + ; A person, and the role they are currently signed in as, if any. + (type principal (maybe assumed role))) + +(instance start scp-escalation + + ; The guardrails. Production's SCP denies CloudTrail changes, so no role in + ; a production account can switch off the audit trail, however broad its + ; IAM policy. The security OU's denies production writes. + (ou security (deny-prod-write yes) (deny-cloudtrail-edit no) (deny-audit-read no)) + (ou production (deny-prod-write no) (deny-cloudtrail-edit yes) (deny-audit-read no)) + ; Created for the reorganisation, with its SCPs copied from the sandbox + ; template: no CloudTrail guardrail (sandboxes are disposable) and no access + ; from outside the unit (sandboxes are isolated), which is where the security + ; team's cross-account read comes from. + (ou workloads (deny-prod-write no) (deny-cloudtrail-edit no) (deny-audit-read yes)) + + (account prod-acct (ou production)) + (account sec-acct (ou security)) + + ; Deploys to production. + (role deploy (in prod-acct) (prod-write yes) (cloudtrail-edit no) (audit-read no)) + ; The broad role engineers use to debug production. Its IAM policy is + ; PowerUserAccess, which includes CloudTrail. Nobody narrowed it, because + ; the production OU's SCP already denies CloudTrail changes. + (role power (in prod-acct) (prod-write yes) (cloudtrail-edit yes) (audit-read no)) + ; How the security team reads production's audit trail: a role inside the + ; production account that their own account is trusted to assume. + (role audit-reader (in prod-acct) (prod-write no) (cloudtrail-edit no) (audit-read yes)) + + (principal dev (assumed vacant)) + (principal sec (assumed vacant))) + +(use scp-escalation) +(initial start) + +; ---- signing in and out ---- + +; One move per trust relationship, written out: who may assume which role is +; wiring, and wiring is listed rather than computed. +(form (assume N P R) + (transition N (when (not (defined P.assumed))) (do (set P.assumed R)))) +(form (sign-out N P) + (transition N (when (defined P.assumed)) (do (vacate P.assumed)))) + +(assume dev-assumes-deploy dev deploy) +(assume dev-assumes-power dev power) +(assume sec-assumes-audit-reader sec audit-reader) +(sign-out dev-signs-out dev) +(sign-out sec-signs-out sec) diff --git a/entitlement-problems/separation-of-duties/README.md b/entitlement-problems/separation-of-duties/README.md new file mode 100644 index 0000000..cd172a3 --- /dev/null +++ b/entitlement-problems/separation-of-duties/README.md @@ -0,0 +1,173 @@ +# Separation of duties, through a role nobody listed + +The person who raises a payment must not be the person who approves it. +Everyone knows the rule, and the usual control enforces it with a table of +*toxic combinations*: pairs of groups nobody may hold together. Every access +request is checked against the table before anyone is added to a group. + +The table is written in group names, but the rule is about capabilities, and +a person gets capabilities from a group's *role*. The two agree only as long +as every group whose role can raise or approve appears in the table. Nothing +checks that. When the finance team creates a group for its own leads and +gives it a role that approves invoices, the table is still correct about every +pair it lists, and a requester can now become an approver. + +## The model + +[`separation-of-duties.writ`](separation-of-duties.writ) has three kinds of +thing: + +- a **role** is a fixed bundle of capabilities: `can-request` and + `can-approve`; +- a **group** grants exactly one role; +- an **account** is in at most two groups, as two slots `g1` and `g2`. + +Three roles: `requester`, `approver`, and `ap-lead`, which approves invoices. +Three groups grant them: `requesters`, `approvers`, `finance-leads`. Two +accounts, `alice` and `bob`, start in no group. The moves add an account to a +group (`alice-joins-requesters` fills the first slot, +`alice-also-joins-finance-leads` the second) or take it out again. + +The rule is a law, written once over the account's slots and read *through* +the group to its role: + +```lisp +(equation separation (not (conflicted account))) +``` + +where `conflicted` (in [`separation-of-duties.lib.writ`](separation-of-duties.lib.writ)) +spells out every pair of slots: `g1`'s role can request and `g2`'s can approve, +and so on. A law is reported whenever any reachable situation breaks it, +whatever the moves allowed. + +The two files differ in one conjunct of the grant's guard. The safe plan +refuses a grant if the table lists the pair **or** if the group's role would +complete a conflict with the other slot: + +```lisp +(when (and (not (defined A.g1)) + (not (listed-pair G A.g2)) + (not (grant-conflicts G A.g2)))) +``` + +[`separation-of-duties-shortcut.writ`](separation-of-duties-shortcut.writ) +keeps `listed-pair` and drops `grant-conflicts`. That is the check most access +tooling performs. + +## What writ answers + +Both plans are asked the questions in +[`separation-of-duties.claims`](separation-of-duties.claims). The safe plan, +exit 0: + +``` +states: 144 edges: 768 +regime: reversible — 144 of 144 situations lie on cycles +… +holds staffable + "someone can be given the power to approve" + witness: 1. alice-joins-approvers → #2 alice.g1: ∅ → approvers +holds no-conflict + "nobody ever holds both halves of a payment" +holds revocable + "from every reachable situation, everyone can still be taken out of every group" +certified: every answer re-derived from the model (writ-cert) +``` + +The shortcut, exit 1: + +``` +states: 196 edges: 1120 +… +equation separation + … + violated in 52 reachable situations witness: 1. alice-joins-requesters 2. alice-also-joins-finance-leads → #14 +… +fails no-conflict + "nobody ever holds both halves of a payment" + witness: 1. alice-joins-requesters → #1 alice.g1: ∅ → requesters + 2. alice-also-joins-finance-leads → #14 alice.g2: ∅ → finance-leads + conflicted-accounts (at state 14) + a = alice +``` + +Two grants, each of which passes the table. The first is what Alice's job +needs. The second is a group whose name says nothing about approving. The +`conflicted-accounts` line answers the query the property names with +`(show …)`: who is in the bad situation. + +The shortcut still lets anyone be made an approver and still lets everyone be +taken out of every group, so `staffable` and `revocable` hold for both. Only +the safety question tells them apart. + +## Who, and through which grants + +A law's subject is one account at a time, and a query's variables cannot be +compared with each other. So "which two groups" is a join, and joins are what +[`separation-of-duties.rules`](separation-of-duties.rules) is for: + +```sh +writ derive separation-of-duties-shortcut.writ separation-of-duties.rules conflict +``` + +``` +conflict (56 rows) + 14 alice requesters finance-leads + 29 alice requesters finance-leads + 57 bob requesters finance-leads + … +``` + +Every row is the same pair. `requesters` + `approvers`, the pair the table +lists, never appears. The first column is a situation number, and +`writ show` reads any of them back: + +```sh +writ show separation-of-duties-shortcut.writ --at 14 +``` + +``` +situation 14 of 196 + cells: (alice.g1=requesters bob.g1=∅ alice.g2=finance-leads bob.g2=∅) + route: 1. alice-joins-requesters + 2. alice-also-joins-finance-leads + moves: … alice-leaves-first-group → 6 alice-leaves-second-group → 1 +``` + +That is the violation stated in the domain's own terms: the account, the two +grants, the order they were made in, and the two moves that would undo it. + +## Why two slots + +Two slots per account is enough to show the finding, and it keeps the space +small (196 situations). The ceiling is the model's, not writ's: a third slot +is a third `maybe` arrow, and `conflicted` gains the pairs that involve it. + +The slots are there because writ cannot compare two bound variables. "No +account holds two groups that conflict" cannot be a `some … some …` law. It +is a law rooted at **one** account over a bounded number of slots. + +## What to take away + +The mistake is never in one grant. Each of Alice's two grants is legitimate on +its own, and the control that checks grants against a list of group names +passed both. The conflict exists only in the composition, through a role that +was added later by someone else. A check that reads what a group *grants* +catches it on the second grant. A check that reads what a group is *called* +cannot. + +To adapt it, list your roles' capabilities from the policy documents rather +than from group names, and add a slot if your people commonly hold three +groups. + +## Run it + +```sh +writ check separation-of-duties.writ --claims separation-of-duties.claims # exit 0 +writ check separation-of-duties-shortcut.writ --claims separation-of-duties.claims # exit 1 +``` + +[`separation-of-duties.rules`](separation-of-duties.rules) also encodes the +three properties for `writ derive`. `../../modality-cross-check.sh` checks the +two answers agree. Siblings: [`../scp-escalation/`](../scp-escalation/), +[`../joiner-mover-leaver/`](../joiner-mover-leaver/). diff --git a/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ b/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ new file mode 100644 index 0000000..5bd6777 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties-shortcut.writ @@ -0,0 +1,92 @@ +; The same access process, with ONE CONDITION REMOVED from every grant: the +; request is checked against the toxic-combination table, and nothing else. +; +; That is how most access tooling works. The table names `requesters` and +; `approvers`, so nobody can hold both. It does not name `finance-leads`: that +; group was created later, by another team, and its role `ap-lead` approves. +; The table was written in group names; the conflict lives in a role. +; +; `writ check` exits 1 on this file. + +(load "stdlib.writ") +(load "separation-of-duties.lib.writ") + +(schema separation-of-duties + + (type yn (no yes)) + + ; A role is a bundle of capabilities, fixed when it was designed. + (type role + (arrow can-request (to yn) fixed) + (arrow can-approve (to yn) fixed)) + + ; A group grants exactly one role. Access is given by adding people to groups, + ; so a person's capabilities are never written down anywhere: they are + ; whatever their groups' roles add up to. + (type group (arrow role (to role) fixed)) + + ; Two group slots per account. What changes is who is in which group. + (type account + (maybe g1 group) + (maybe g2 group)) + + ; ---- the rule ---- + + ; Separation of duties: nobody can both raise a payment and approve it. + ; A law, not a guard: writ reports it if any reachable situation breaks it, + ; whatever the moves allowed. + (equation separation (not (conflicted account)))) + +(instance start separation-of-duties + + (role requester (can-request yes) (can-approve no)) + (role approver (can-request no) (can-approve yes)) + ; Team leads in accounts payable sign off invoices. It is an approver by + ; another name, created by the finance team for its own leads, after the + ; toxic-combination table was written. + (role ap-lead (can-request no) (can-approve yes)) + + (group requesters (role requester)) + (group approvers (role approver)) + (group finance-leads (role ap-lead)) + + (account alice (g1 vacant) (g2 vacant)) + (account bob (g1 vacant) (g2 vacant))) + +(use separation-of-duties) +(initial start) + +; ---- granting and removing access ---- + +; The first group goes in slot g1, a second in g2. +; The grant is refused if the toxic-combination table lists the pair. +(form (join1 N A G) + (transition N + (when (and (not (defined A.g1)) + (not (listed-pair G A.g2)))) ; <- grant-conflicts, gone + (do (set A.g1 G)))) +(form (join2 N A G) + (transition N + (when (and (not (defined A.g2)) + (not (listed-pair G A.g1)))) ; <- grant-conflicts, gone + (do (set A.g2 G)))) + +(form (leave1 N A) (transition N (when (defined A.g1)) (do (vacate A.g1)))) +(form (leave2 N A) (transition N (when (defined A.g2)) (do (vacate A.g2)))) + +(join1 alice-joins-requesters alice requesters) +(join1 alice-joins-approvers alice approvers) +(join1 alice-joins-finance-leads alice finance-leads) +(join2 alice-also-joins-requesters alice requesters) +(join2 alice-also-joins-approvers alice approvers) +(join2 alice-also-joins-finance-leads alice finance-leads) +(join1 bob-joins-requesters bob requesters) +(join1 bob-joins-approvers bob approvers) +(join1 bob-joins-finance-leads bob finance-leads) +(join2 bob-also-joins-requesters bob requesters) +(join2 bob-also-joins-approvers bob approvers) +(join2 bob-also-joins-finance-leads bob finance-leads) +(leave1 alice-leaves-first-group alice) +(leave2 alice-leaves-second-group alice) +(leave1 bob-leaves-first-group bob) +(leave2 bob-leaves-second-group bob) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.claims b/entitlement-problems/separation-of-duties/separation-of-duties.claims new file mode 100644 index 0000000..a276f39 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.claims @@ -0,0 +1,47 @@ +; The questions, put to both plans. + +(load "separation-of-duties.lib.writ") + +(property staffable + "someone can be given the power to approve" + (possible (some (a account) (or (is a.g1.role.can-approve yes) + (is a.g2.role.can-approve yes))))) + +(property no-conflict + "nobody ever holds both halves of a payment" + (never (some (a account) (conflicted a))) + (show conflicted-accounts)) + +(property revocable + "from every reachable situation, everyone can still be taken out of every group" + (live (all (a account) (and (not (defined a.g1)) (not (defined a.g2)))))) + +; ---- ownership ---- +; Every grant can break separation; that is what the grant checks are for, and +; on the shortcut it is what the law reports. A removal cannot add a capability, +; but writ's reading is syntactic: it writes a slot the law reads, so it is +; acknowledged too. +(accept alice-joins-requesters separation) +(accept alice-joins-approvers separation) +(accept alice-joins-finance-leads separation) +(accept alice-also-joins-requesters separation) +(accept alice-also-joins-approvers separation) +(accept alice-also-joins-finance-leads separation) +(accept bob-joins-requesters separation) +(accept bob-joins-approvers separation) +(accept bob-joins-finance-leads separation) +(accept bob-also-joins-requesters separation) +(accept bob-also-joins-approvers separation) +(accept bob-also-joins-finance-leads separation) +(accept alice-leaves-first-group separation) +(accept alice-leaves-second-group separation) +(accept bob-leaves-first-group separation) +(accept bob-leaves-second-group separation) + +; ---- who ---- +; Answered at the situation a failing verdict singles out. A query binder +; cannot be compared with another, so this names the ACCOUNT; which two groups +; it holds is a join, and that is `conflict` in separation-of-duties.rules. +(query conflicted-accounts + (where (a account)) + (conflicted a)) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ b/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ new file mode 100644 index 0000000..133642c --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.lib.writ @@ -0,0 +1,27 @@ +; Shared by the models and the questions, because a questions file has its own +; form scope and there is no implicit prelude. +(load "stdlib.writ") + +; A holds, through its two group slots, both the power to raise a payment and +; the power to approve one. Spelled out over every pair of slots, the same slot +; twice included: a single group whose role carries both is a conflict too. +; It is rooted at ONE account because two bound accounts cannot be compared; +; that is also why the slots are bounded (see the README). +(form (conflicted A) + (or (and (is A.g1.role.can-request yes) (is A.g1.role.can-approve yes)) + (and (is A.g1.role.can-request yes) (is A.g2.role.can-approve yes)) + (and (is A.g2.role.can-request yes) (is A.g1.role.can-approve yes)) + (and (is A.g2.role.can-request yes) (is A.g2.role.can-approve yes)))) + +; What joining group G would add to account A, whose OTHER slot is OTHER. +; The capability check: read through the group to its role. +(form (grant-conflicts G OTHER) + (or (and (is G.role.can-request yes) (is G.role.can-approve yes)) + (and (is G.role.can-request yes) (is OTHER.role.can-approve yes)) + (and (is G.role.can-approve yes) (is OTHER.role.can-request yes)))) + +; The name check: the toxic-combination table as an IAM team writes it — two +; groups that must never be held together, listed by name. +(form (listed-pair G OTHER) + (or (and (is G requesters) (is OTHER approvers)) + (and (is G approvers) (is OTHER requesters)))) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.rules b/entitlement-problems/separation-of-duties/separation-of-duties.rules new file mode 100644 index 0000000..d89679a --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.rules @@ -0,0 +1,31 @@ +; The same three questions, answered a second time by a different part of +; `writ`, so that `modality-cross-check.sh` can compare them. A disagreement is +; a bug in one of them, not a number to adjust. +; +; POLARITY: +; `possible F` is the SATISFYING set — non-empty means it holds. +; `never F` and `live F` are COUNTEREXAMPLE sets — EMPTY means it holds. +(load "ct.rules") +(load "separation-of-duties.lib.writ") + +(satisfies staffable + (some (a account) (or (is a.g1.role.can-approve yes) (is a.g2.role.can-approve yes)))) + +(satisfies no-conflict (some (a account) (conflicted a))) + +(satisfies everyone-out (all (a account) (and (not (defined a.g1)) (not (defined a.g2))))) +(can-reach can-empty everyone-out) +(trapped revocable can-empty) + +; ---- the explanation ---- +; The question the law cannot answer, because its subject is one account at a +; time: WHO holds both halves, and through WHICH two groups. Here variables +; join, so the answer is a table: situation, account, the group that lets them +; raise a payment, the group that lets them approve it. +(relation conflict (Situation account group group)) +(rule (conflict S A G H) + (situation S) (holds S (is A.g1 G)) (holds S (is A.g2 H)) + (is G.role.can-request yes) (is H.role.can-approve yes)) +(rule (conflict S A G H) + (situation S) (holds S (is A.g2 G)) (holds S (is A.g1 H)) + (is G.role.can-request yes) (is H.role.can-approve yes)) diff --git a/entitlement-problems/separation-of-duties/separation-of-duties.writ b/entitlement-problems/separation-of-duties/separation-of-duties.writ new file mode 100644 index 0000000..405cb15 --- /dev/null +++ b/entitlement-problems/separation-of-duties/separation-of-duties.writ @@ -0,0 +1,100 @@ +; Separation of duties — and a conflict that arrives through a role. +; +; The rule is old and everyone knows it: the person who raises a payment must +; not be the person who approves it. The usual control is a table of toxic +; combinations: these two groups may never be held together. Access requests +; are checked against the table before anyone is added to a group. +; +; The table is written in GROUP names. The rule is about CAPABILITIES, which a +; person gets from a group's role. The two agree only as long as every group +; that carries both capabilities is in the table, and nothing checks that. +; +; This plan checks both: the table, and what the group would actually add. +; `writ check` exits 0 on this file. + +(load "stdlib.writ") +(load "separation-of-duties.lib.writ") + +(schema separation-of-duties + + (type yn (no yes)) + + ; A role is a bundle of capabilities, fixed when it was designed. + (type role + (arrow can-request (to yn) fixed) + (arrow can-approve (to yn) fixed)) + + ; A group grants exactly one role. Access is given by adding people to groups, + ; so a person's capabilities are never written down anywhere: they are + ; whatever their groups' roles add up to. + (type group (arrow role (to role) fixed)) + + ; Two group slots per account. What changes is who is in which group. + (type account + (maybe g1 group) + (maybe g2 group)) + + ; ---- the rule ---- + + ; Separation of duties: nobody can both raise a payment and approve it. + ; A law, not a guard: writ reports it if any reachable situation breaks it, + ; whatever the moves allowed. + (equation separation (not (conflicted account)))) + +(instance start separation-of-duties + + (role requester (can-request yes) (can-approve no)) + (role approver (can-request no) (can-approve yes)) + ; Team leads in accounts payable sign off invoices. It is an approver by + ; another name, created by the finance team for its own leads, after the + ; toxic-combination table was written. + (role ap-lead (can-request no) (can-approve yes)) + + (group requesters (role requester)) + (group approvers (role approver)) + (group finance-leads (role ap-lead)) + + (account alice (g1 vacant) (g2 vacant)) + (account bob (g1 vacant) (g2 vacant))) + +(use separation-of-duties) +(initial start) + +; ---- granting and removing access ---- + +; The first group goes in slot g1, a second in g2. +; The grant is refused if the toxic-combination table lists the pair, or if +; the group's role would give the account, together with its other slot, both +; halves of a payment. The second check reads through the group to the role. +(form (join1 N A G) + (transition N + (when (and (not (defined A.g1)) + (not (listed-pair G A.g2)) + (not (grant-conflicts G A.g2)))) + (do (set A.g1 G)))) +(form (join2 N A G) + (transition N + (when (and (not (defined A.g2)) + (not (listed-pair G A.g1)) + (not (grant-conflicts G A.g1)))) + (do (set A.g2 G)))) + +(form (leave1 N A) (transition N (when (defined A.g1)) (do (vacate A.g1)))) +(form (leave2 N A) (transition N (when (defined A.g2)) (do (vacate A.g2)))) + +(join1 alice-joins-requesters alice requesters) +(join1 alice-joins-approvers alice approvers) +(join1 alice-joins-finance-leads alice finance-leads) +(join2 alice-also-joins-requesters alice requesters) +(join2 alice-also-joins-approvers alice approvers) +(join2 alice-also-joins-finance-leads alice finance-leads) +(join1 bob-joins-requesters bob requesters) +(join1 bob-joins-approvers bob approvers) +(join1 bob-joins-finance-leads bob finance-leads) +(join2 bob-also-joins-requesters bob requesters) +(join2 bob-also-joins-approvers bob approvers) +(join2 bob-also-joins-finance-leads bob finance-leads) +(leave1 alice-leaves-first-group alice) +(leave2 alice-leaves-second-group alice) +(leave1 bob-leaves-first-group bob) +(leave2 bob-leaves-second-group bob) diff --git a/modality-cross-check.sh b/modality-cross-check.sh index dce80fc..bd3c147 100755 --- a/modality-cross-check.sh +++ b/modality-cross-check.sh @@ -34,7 +34,7 @@ set -u here=$(cd "$(dirname "$0")" && pwd) WRIT=${WRIT:-writ} -scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column" +scenarios="river island queens jobshop-possible jobshop-best oversight workflow access arch two-phase-commit db-migration-problems/rename-a-column db-migration-problems/drop-a-column db-migration-problems/add-a-required-column entitlement-problems/separation-of-duties entitlement-problems/scp-escalation entitlement-problems/joiner-mover-leaver" considered=0 compared=0 diff --git a/run-tests.sh b/run-tests.sh index 53242dd..9742087 100755 --- a/run-tests.sh +++ b/run-tests.sh @@ -431,16 +431,17 @@ crosscheck() { st=$? printf '%s\n' "$out" | sed 's/^/ | /' exit_is "cross-check: the two implementations agree everywhere" "$st" 0 - # The thirteen scenarios this script walks by convention, and their 31 + # The sixteen scenarios this script walks by convention, and their 41 # properties. `calculation/` and `gotha/` are not among them: each carries its # own explicit cross-check.sh, run from its own test function above. Adding a - # property to any of the thirteen fails this line, which is the point of it — - # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, and - # 26 -> 31 with two-phase-commit, and this line is where each of those had to - # be said out loud. - has "cross-check: all 31 properties of the thirteen scenarios were considered" \ - "$out" "considered 31 properties" - # One of the 31 is not compared, and the count above is the only place that + # property to any of the sixteen fails this line, which is the point of it — + # the count went 20 -> 22 -> 26 as the three db-migration-problems joined, + # 26 -> 31 with two-phase-commit, and 31 -> 41 with the three + # entitlement-problems (3 + 3 + 4), and this line is where each of those had + # to be said out loud. + has "cross-check: all 41 properties of the sixteen scenarios were considered" \ + "$out" "considered 41 properties" + # One of the 41 is not compared, and the count above is the only place that # would notice if the reason changed: two-phase-commit asks one property under # a fairness assumption, which ct.rules §8 does not encode. has "cross-check: with the one fair property skipped, and saying why" \ @@ -454,9 +455,10 @@ crosscheck() { # `arch` brought the repository's first two `never` properties, so this # branch — which announced itself as unexercised on every prior run — is now # measured. If it ever reads "unexercised" again, a scenario went missing. - # two-phase-commit's atomicity is the third. + # two-phase-commit's atomicity is the third; the entitlement problems bring + # four more, since "nobody ever holds X" is how an access rule is said. has "cross-check: C. the never branch is exercised" "$out" \ - "never: 3 properties compared" + "never: 7 properties compared" # And `inevitable`, whose two are two-phase-commit's — the newest modality, # and the one whose second implementation is newest, so the line that says it # is being compared at all is worth having. @@ -598,9 +600,93 @@ add_a_required_column() { fi } +separation_of_duties() { + d="$here/entitlement-problems/separation-of-duties" + echo "== Separation of duties — a conflict that arrives through a role ==" + echo " Q: the toxic-combination table is checked on every grant. Is that enough?" + out=$("$WRIT" check "$d/separation-of-duties.writ" --claims "$d/separation-of-duties.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "separation-of-duties: checking capabilities, the plan is clean" "$st" 0 + has "separation-of-duties: A. an approver can still be appointed" "$out" "holds staffable" + has "separation-of-duties: B. nobody holds both halves of a payment" "$out" "holds no-conflict" + has "separation-of-duties: and everyone can still be taken out of every group" "$out" "holds revocable" + lacks "separation-of-duties: nothing is violated" "$out" "violated in" + + sc=$("$WRIT" check "$d/separation-of-duties-shortcut.writ" --claims "$d/separation-of-duties.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "separation-of-duties: checking the table alone is refused" "$sst" 1 + has "separation-of-duties: C. two grants the table never listed" "$sc" "violated in 52 reachable situations" + near "separation-of-duties: the first is innocent" "$sc" "fails no-conflict" "1. alice-joins-requesters" + near "separation-of-duties: the second is a group nobody put in the table" "$sc" "fails no-conflict" "2. alice-also-joins-finance-leads" + near "separation-of-duties: and the verdict names who" "$sc" "fails no-conflict" "a = alice" + # Which two groups is a join, which a query cannot do and the rules engine + # can: every row it prints is the same pair, and that pair is the finding. + dv=$("$WRIT" derive "$d/separation-of-duties-shortcut.writ" "$d/separation-of-duties.rules" conflict 2>&1) + has "separation-of-duties: D. derive names the account and both groups" "$dv" "14 alice requesters finance-leads" + lacks "separation-of-duties: and the pair the table lists never appears" "$dv" "requesters approvers" +} + +scp_escalation() { + d="$here/entitlement-problems/scp-escalation" + echo "== An OU move — the guardrails stay behind ==" + echo " Q: moving an account between OUs changes no role. What does it change?" + out=$("$WRIT" check "$d/scp-escalation.writ" --claims "$d/scp-escalation.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "scp-escalation: the organization as approved is clean" "$st" 0 + has "scp-escalation: A. developers cannot modify CloudTrail" "$out" "holds dev-never-edits-cloudtrail" + has "scp-escalation: B. the security team can always reach the audit trail" "$out" "holds sec-can-always-audit" + + cmp=$("$WRIT" compare "$d/scp-escalation.writ" "$d/scp-escalation-restructured.writ" 2>&1) + cst=$? + printf '%s\n' "$cmp" | sed 's/^/ | /' + exit_is "scp-escalation: compare refuses the reorganisation" "$cst" 1 + has "scp-escalation: C. deploying still works" "$cmp" "dev-can-deploy preserved" + has "scp-escalation: D. the CloudTrail guardrail is LOST" "$cmp" "dev-never-edits-cloudtrail LOST witness: 1. dev-assumes-power 2. move-prod-to-workloads" + has "scp-escalation: E. and the security team is locked out, by the move alone" "$cmp" "sec-can-always-audit LOST witness: 1. move-prod-to-workloads" + + dv=$("$WRIT" derive "$d/scp-escalation-restructured.writ" "$d/scp-escalation.rules" escalation 2>&1) + has "scp-escalation: F. derive prints the privilege path" "$dv" "dev power prod-acct workloads" +} + +joiner_mover_leaver() { + d="$here/entitlement-problems/joiner-mover-leaver" + echo "== Joiner, mover, leaver — the grant that offboarding cannot see ==" + echo " Q: offboarding removes people from their groups. Is that everything?" + out=$("$WRIT" check "$d/joiner-mover-leaver.writ" --claims "$d/joiner-mover-leaver.claims" 2>&1) + st=$? + printf '%s\n' "$out" | sed 's/^/ | /' + exit_is "joiner-mover-leaver: removing everything by name, the plan is clean" "$st" 0 + has "joiner-mover-leaver: A. Ada can be given production access" "$out" "holds ada-gets-access" + has "joiner-mover-leaver: B. a mover loses it" "$out" "holds movers-lose-prod" + has "joiner-mover-leaver: C. a leaver loses it" "$out" "holds leavers-lose-everything" + has "joiner-mover-leaver: and can always be cut off" "$out" "holds leavers-can-be-cut-off" + + sc=$("$WRIT" check "$d/joiner-mover-leaver-shortcut.writ" --claims "$d/joiner-mover-leaver.claims" 2>&1) + sst=$? + printf '%s\n' "$sc" | sed 's/^/ | /' + exit_is "joiner-mover-leaver: group-only offboarding is refused" "$sst" 1 + has "joiner-mover-leaver: D. a leaver keeps production access" "$sc" "fails leavers-lose-everything" + near "joiner-mover-leaver: after an ordinary four-step history" "$sc" "fails leavers-lose-everything" "4. ada-leaves" + # The query answer sits below the four-move witness, past `near`'s six lines, + # so it is anchored on the situation the verdict singled out. + near "joiner-mover-leaver: and the verdict names what was left behind" "$sc" "stranded (at state 13)" "e = prod-admin" + has "joiner-mover-leaver: E. so does a mover" "$sc" "fails movers-lose-prod" + # Not a delay but a trap: nothing that runs later removes a direct grant. + has "joiner-mover-leaver: F. and nothing left can cut the leaver off" "$sc" "fails leavers-can-be-cut-off" + near "joiner-mover-leaver: stuck holding the direct assignment" "$sc" "fails leavers-can-be-cut-off" "prod-admin.holder=ada" + has "joiner-mover-leaver: while the group grant was removed" "$sc" "prod-engineers.holder: ada → ∅" + + dv=$("$WRIT" derive "$d/joiner-mover-leaver-shortcut.writ" "$d/joiner-mover-leaver.rules" left-behind 2>&1) + has "joiner-mover-leaver: G. every entitlement left behind was granted directly" "$dv" "prod-admin direct ada" + lacks "joiner-mover-leaver: and none through a group" "$dv" " group " +} + # The scenarios, in order — the single source of truth for `all`, numbering # (1-based, as `list` prints), and name lookup. Each is a function above. -scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column control gitcompare crosscheck" +scenarios="river island queens jobshop_possible jobshop_best oversight workflow two_phase_commit access calculation gotha arch timetable rename_a_column drop_a_column add_a_required_column separation_of_duties scp_escalation joiner_mover_leaver control gitcompare crosscheck" list_scenarios() { echo "tests (run one by name or number, e.g. '$0 3' or '$0 river'):"