Chapter 2 — Discrete mathematics
Lesson map
Lesson 02 published. Map, example, EX004.
flowchart TD
N0["Learning outcomes"]
N1["2.1 Policies as logic"]
N2["2.2 Sets and wildcards"]
N3["Lab — Lab — policy evaluation"]
N4["2.3 Lab result"]
N5["2.4 Why this structure"]
N6["2.5 Proving properties"]
N7["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> N7
N7 --> EX["Worked example"]
EX --> Q["Exercise EX004"]
Logical drawing
flowchart LR
N0["Learning outcomes"]
N1["2.1 Policies as logic"]
N2["2.2 Sets and wildcards"]
N3["Lab — Lab — policy evaluation"]
N4["2.3 Lab result"]
N5["2.4 Why this structure"]
N6["2.5 Proving properties"]
N7["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> N6 --> N7 --> Q["EX004"]
[Learning outcomes]
|
v
[2.1 Policies as logic]
|
v
[2.2 Sets and wildcards]
|
v
[Lab — Lab — policy evaluation]
|
v
[2.3 Lab result]
|
v
[2.4 Why this structure]
|
v
[2.5 Proving properties]
|
v
[Synthesis]
|
v
[Worked example] --> [Exercise EX004]
Learning outcomes
You will (1) express access policies as logic and sets; (2) evaluate requests with default deny and explicit deny; (3) reason about policy combinations; (4) test a small evaluator.
2.1 Policies as logic
An access policy is a set of rules, each matching a principal, an action and a resource. A request is allowed if some allow rule matches and no deny rule matches; otherwise it is denied by default. This is a logical formula: allowed = (exists allow match) and not (exists deny match).
Writing the rule as a formula makes its behaviour predictable. Two results follow directly: a request that matches nothing is denied, and a single matching deny beats any number of allows. Elena uses the formula to explain to the platform team why adding another allow rule did not fix a denied request, because a deny elsewhere was still matching it.
2.2 Sets and wildcards
Wildcards describe sets: storage:Get* is the set of all get actions; readings/* is all objects under readings. Reasoning about overlaps between sets explains surprising results, such as a broad allow being overridden by a narrow deny.
Wildcards are convenient but easy to over-grant: storage:* includes deletes and permission changes that the writer may never have intended. Thinking of each pattern as a set, and asking what is inside it, helps spot such over-reach. Overlaps also explain conflicts, since two rules with overlapping sets both match some requests and the combining rule decides the outcome.
Lab — Lab — policy evaluation
"""Evaluate synthetic access requests: default deny, explicit deny overrides allow (stdlib only)."""
from fnmatch import fnmatch
policies = [
("allow", "meter-reader", "storage:Get*", "readings/*"),
("allow", "meter-reader", "storage:*", "readings/raw/*"),
("deny", "*", "storage:Delete*", "readings/*"),
("allow", "ops-admin", "storage:*", "*"),
]
requests = [
("meter-reader", "storage:GetObject", "readings/2026/10.csv"),
("meter-reader", "storage:PutObject", "readings/raw/a.csv"),
("meter-reader", "storage:DeleteObject", "readings/raw/a.csv"),
("ops-admin", "storage:DeleteObject", "readings/old.csv"),
("billing-job", "storage:GetObject", "readings/2026/10.csv"),
]
for who, act, res in requests:
m = [e for e, p, a, r in policies if fnmatch(who, p) and fnmatch(act, a) and fnmatch(res, r)]
d = "DENY (explicit)" if "deny" in m else ("ALLOW" if "allow" in m else "DENY (default)")
print(f"{who:13} {act:21} {res:22} {d}")
Run with python3 lab_policy.py. Verified output:
meter-reader storage:GetObject readings/2026/10.csv ALLOW
meter-reader storage:PutObject readings/raw/a.csv ALLOW
meter-reader storage:DeleteObject readings/raw/a.csv DENY (explicit)
ops-admin storage:DeleteObject readings/old.csv DENY (explicit)
billing-job storage:GetObject readings/2026/10.csv DENY (default)
2.3 Lab result
meter-reader may get readings/2026/10.csv and put readings/raw/a.csv (ALLOW). meter-reader's delete of readings/raw/a.csv is DENY (explicit) because the deny on storage:Delete* for readings/* matches, overriding the broader allow. ops-admin's delete of readings/old.csv is also DENY (explicit): the deny rule applies to everyone. billing-job has no matching allow, so it is DENY (default).
The lab's value is in the reasons as much as the outcomes. Two denials look the same to the caller but come from different causes: one from an explicit guardrail, one from a missing allow. Fixing them needs different actions. For billing-job, an allow must be added if the access is legitimate; for the delete guardrail, the team must decide whether any exception is justified at all.
2.4 Why this structure
Default deny means forgotten cases fail safe. Explicit deny lets a security team set guardrails that application teams cannot override with broad allows. NIST SP 800-210 discusses such policy combination in cloud access control.
Without default deny, a new resource created without a policy would be open until someone noticed. Without explicit deny, any team with permission to write allow rules could widen access beyond what the security team intended. Together they give a predictable floor and ceiling, within which application teams can grant what they need.
2.5 Proving properties
With the formula, Elena can argue properties such as "no principal can delete readings" by showing the deny rule covers every delete action on readings, regardless of allows.
A test checks a few cases; an argument from the formula covers all cases at once. If every delete on readings matches a deny, no allow can change the result, whatever principals or rules are added later. Elena still writes tests for a sample of cases, so a mistake in her reasoning or a change in the rules would be caught.
Worked example
Rosa asks whether ops-admin should be able to delete old readings for retention. Elena shows that, as written, nobody can; a retention job would need a narrower exception, such as excluding a retention prefix from the deny. They decide retention will use storage lifecycle rules instead, keeping the deny absolute.
Synthetic case. Policies and requests are synthetic.
Errors and limits
Real cloud policy languages have more conditions; check the provider's documented evaluation logic.
Exercises
- EX004 — Formula. Write the allow formula. Rubric: 3 = allow match and not deny match; 2 = partial; 1 = vague; 0 = none.
- EX005 — Lab deny reasons. Why were the two deletes denied? Rubric: 3 = explicit deny on Delete* for readings/*; 2 = partial; 1 = vague; 0 = none.
- EX006 — billing-job. Why was billing-job denied? Rubric: 3 = no allow, default deny; 2 = partial; 1 = vague; 0 = none.
Synthesis
Logic makes policy behaviour predictable and provable.
Continue studying — chapter 02 of 50
← Chapter 01 (draft) · Course chapter index · Chapter 03 (draft) →