Case Study: Auditing an Access-Control Policy with Quantifiers

"A specification is a promise about every possible run, not a story about one."

Executive Summary

A security team hands you an English access-control policy for an internal tool and asks a deceptively simple question: does the current set of permissions actually satisfy the policy? You'll do this the way a careful engineer should — not by clicking around and "trying a few accounts," but by translating each policy rule into a quantified statement over the domains of users, roles, and resources, then evaluating each statement against the real permission data and negating the ones that fail to read off exactly what is broken. This is §2.1–§2.6 in one sitting: predicates and domains (§2.1), universal and existential quantifiers with the right restriction idiom (§2.2), nested quantifiers where order is meaning (§2.3), negation to extract a counterexample (§2.4), the all()/any() evaluation of those quantifiers over finite domains (§2.5), and the realization that the policy is a specification — a precondition the live system must satisfy (§2.6).

The lesson is theme two of the book, in the language of this chapter: clicking around verifies one conjunct of a giant $\land$; auditing the policy checks the whole $\forall$.

Skills applied

• Translating English policy rules into predicate logic, identifying each predicate and its domain.
• Choosing the correct restriction connective ($\forall$ with $\rightarrow$, $\exists$ with $\land$).
• Reading and writing nested quantifiers, and seeing how reordering changes a security requirement.
• Negating a failed universal to produce the exact counterexample an auditor reports.
• Evaluating each quantified rule over finite domains with all() / any(), with hand-derived output.

Background

The scenario

"Helpdesk Console" is an internal web app. Three things matter:

• a set of users (people with accounts),
• a set of roles each user holds (e.g. viewer, agent, admin),
• a set of resources (e.g. tickets, billing, audit-log), each guarded by a required role.

The permission data is stored as plain dictionaries. We model it exactly as the chapter models a domain: the lists you loop over are the domains of discourse.

# Domains of discourse.
users     = ["alice", "bob", "carol", "dan", "erin"]
roles_of  = {                       # which roles each user holds
    "alice": {"admin", "agent"},
    "bob":   {"agent"},
    "carol": {"viewer"},
    "dan":   set(),                 # dan holds NO roles (a new hire, not yet provisioned)
    "erin":  {"agent", "viewer"},
}
required_role = {                   # role needed to access each resource
    "tickets":   "agent",
    "billing":   "admin",
    "audit-log": "admin",
}
resources = list(required_role)     # ["tickets", "billing", "audit-log"]

The core predicate is "user $u$ may access resource $r$." A user may access a resource exactly when they hold the role that resource requires:

def can_access(u, r):
    """Predicate Can(u, r): user u may access resource r.
    True iff u holds the role required by r."""
    return required_role[r] in roles_of[u]

print(can_access("alice", "billing"))   # alice is admin; billing needs admin
print(can_access("bob", "billing"))     # bob is only agent; billing needs admin
# Expected output:
# True
# False

can_access is the predicate $\text{Can}(u, r)$ from §2.1 rendered as a boolean-valued function — a function from a pair of objects to a truth value. Everything below quantifies this predicate over the domains users and resources.

💡 Intuition: Before writing a single quantifier, notice what the domains are. "For every user" ranges over users; "for some resource" ranges over resources. The chapter's recurring move — name the domain first — is the whole discipline of a correct audit. A rule that doesn't say over what is not yet a checkable rule.

Why this matters

Access-control bugs are among the most expensive bugs there are: a single over-permissive rule is a data breach, and a single under-permissive rule is an outage. Real systems (AWS IAM, Kubernetes RBAC, SQL GRANTs) are, underneath, exactly this — predicates over users and resources — and the policies that govern them are quantified statements. Learning to read a policy as logic is learning to audit it at all.

Phase 1: Translate the policy into quantified statements

Here is the policy, verbatim from the security team, and its faithful translation. Watch the restriction idioms from §2.2 — the single most common place audits go wrong.

Rule R1 (no orphans). "Every user can access at least one resource."

$$\forall u\,\exists r\, \text{Can}(u, r).$$

This is the nested form of §2.3: for each user (outer $\forall$), there is some resource (inner $\exists$) they can reach — and the resource is allowed to depend on the user. Alice's resource need not be Carol's.

Rule R2 (a common landing page). "There is a resource that every user can access."

$$\exists r\,\forall u\, \text{Can}(u, r).$$

Compare R1 and R2 carefully: the quantifiers are reordered. R2 is strictly stronger — it demands a single resource $r$ that works for everyone at once. As §2.3 proved in the abstract, $\exists r\,\forall u$ implies $\forall u\,\exists r$, but not conversely. The security team wrote both; part of our job is to check whether the system meets the strong one or only the weak one.

Rule R3 (least privilege on the audit log). "Only admins can access the audit log." Equivalently: "every user who can access the audit log is an admin." This is a restricted universal, so it uses $\rightarrow$:

$$\forall u\,\big(\text{Can}(u, \texttt{"audit-log"}) \rightarrow \text{Admin}(u)\big),$$

where $\text{Admin}(u)$ = "admin $\in$ roles_of[u]." Note we did not write $\forall u\,(\text{Can}(u,\texttt{"audit-log"}) \land \text{Admin}(u))$ — that would claim every user can reach the audit log and is an admin, which is not the rule (§2.2's pitfall).

Rule R4 (billing is reachable). "Some user can access billing." A restricted existential — but here the "restriction" is just the resource being fixed, so it is a plain $\exists$ over users:

$$\exists u\, \text{Can}(u, \texttt{"billing"}).$$

⚠️ Common Pitfall: R3 and R4 look symmetric in English ("only admins…", "some user…") but take different connectives. R3 is a $\forall$ constraining which users qualify, so it needs $\rightarrow$. R4 is an $\exists$ asserting a qualifying witness exists, so it needs (implicitly) $\land$ — here the conjunction is trivial because there is no extra qualifier beyond "can access billing." Always classify the quantifier first; the connective follows from it.

🔄 Check Your Understanding Rule R2 is $\exists r\,\forall u\,\text{Can}(u,r)$. Write, in plain English, what $\forall r\,\exists u\,\text{Can}(u,r)$ would say instead, and explain why it is a completely different policy.

Answer

$\forall r\,\exists u\,\text{Can}(u,r)$ says "every resource is accessible to at least one user" — i.e., no resource is locked away from everybody. That is about resources having reachers, whereas R2 is about users having a common resource. The domains the quantifiers range over are swapped, and so is the meaning entirely.

Phase 2: Evaluate each rule over the finite domains

Each rule is a quantified statement over finite domains, so — exactly as §2.5 says — we evaluate it with all() (for $\forall$) and any() (for $\exists$). We write each check to mirror its logical form structurally, so the code is the formula.

def is_admin(u):
    return "admin" in roles_of[u]

# R1:  forall u. exists r. Can(u, r)
R1 = all(any(can_access(u, r) for r in resources) for u in users)

# R2:  exists r. forall u. Can(u, r)
R2 = any(all(can_access(u, r) for u in users) for r in resources)

# R3:  forall u. ( Can(u, "audit-log") -> Admin(u) )
R3 = all((not can_access(u, "audit-log")) or is_admin(u) for u in users)

# R4:  exists u. Can(u, "billing")
R4 = any(can_access(u, "billing") for u in users)

print(R1, R2, R3, R4)
# Expected output:
# False True True True

Let's hand-derive each value from the definitions — this is the part you must be able to do without running anything, because in a real audit you are reasoning about why, not just whether.

R1 — $\forall u\,\exists r\,\text{Can}(u,r)$ — hand trace. For each user, does some resource admit them?

The outer all(...) is a big $\land$ over the last column; it hits its first False at carol and short-circuits to False. (Recall §2.5: all is entitled to stop at the first failing conjunct.) So $R1$ is False — there exist users who can access nothing.

R2 — $\exists r\,\forall u\,\text{Can}(u,r)$ — hand trace. For each resource, can every user reach it?

Every resource fails the inner all(...), so the outer any(...) finds no witness and $R2$ is… False? But the expected output above says R2 is True. Stop — this is exactly the kind of mismatch a careful auditor must resolve, not paper over.

🐛 Find the Error: The hand trace above concludes $R2$ is False, but the predicted program output is True. One of them is wrong. Before reading on, recompute: is there any resource that every one of alice, bob, carol, dan, erin can access?

Answer

The hand trace is correct and the earlier "Expected output" line was wrong on purpose. No resource is reachable by all five users (tickets needs agent, which carol and dan lack; billing and audit-log need admin, which only alice has). So the inner all(...) is False for every resource, the outer any(...) returns False, and $R2$ is False. The corrected output line is: # Expected output: / # False False True True. The lesson: when the trace and the prediction disagree, re-derive from the definitions — do not trust the prediction. We continue with the corrected value $R2 = \textbf{False}$.

With $R2$ corrected, the true evaluation is:

print(R1, R2, R3, R4)
# Expected output (corrected):
# False False True True

R3 — $\forall u\,(\text{Can}(u,\texttt{audit-log}) \rightarrow \text{Admin}(u))$ — hand trace. Using $a \rightarrow b \equiv \neg a \lor b$, the body is (not can_access(u,"audit-log")) or is_admin(u).

Every row is True, so $R3$ is True. Notice §2.2's vacuous-truth idiom doing real work: non-admins who cannot reach the audit log satisfy the implication automatically, because the hypothesis is false. R3 only "bites" on a user who can reach the audit log; the rule is "no non-admin reaches it," and none does.

R4 — $\exists u\,\text{Can}(u,\texttt{billing})$ — hand trace. Walk users until one can reach billing: alice is admin, so can_access("alice","billing") is True on the first element, and any short-circuits to True. $R4$ holds.

Phase 3: Negate the failures to report exact findings

A boolean "R1 failed" is useless to whoever has to fix it. The value of the negation laws (§2.4) is that they tell you exactly what object to report. Negate the failed rule and the witness falls out.

R1 was $\forall u\,\exists r\,\text{Can}(u,r)$ and it is false. Push the negation all the way in, flipping each quantifier as it passes (§2.4):

$$ \neg\,\forall u\,\exists r\,\text{Can}(u,r) \;\equiv\; \exists u\,\neg\,\exists r\,\text{Can}(u,r) \;\equiv\; \exists u\,\forall r\,\neg\,\text{Can}(u,r). $$

Read the result: there is a user who cannot access any resource. That is precisely the audit finding — and the negation even tells us its shape: report a user, and certify that for all resources they are denied. The finder is the existential mirror of §2.4's counterexample:

def first_orphan(users, resources):
    """Witness to  exists u. forall r. not Can(u, r):
    the first user who can access no resource at all, or None."""
    for u in users:
        if all(not can_access(u, r) for r in resources):   # forall r. not Can(u, r)
            return u
    return None

print(first_orphan(users, resources))
# Expected output:
# carol

carol is returned: walking users, alice/bob have access, but carol (a viewer only) is denied tickets, billing, and audit-log, so the inner all(not ...) is True and she is the first witness. She is the executable form of the $\exists u$ in the negation. (dan is also an orphan, but any/the loop stop at the first one — to list them all, drop the early return and collect.)

Likewise R2's failure, negated, is $\neg\,\exists r\,\forall u\,\text{Can}(u,r) \equiv \forall r\,\exists u\,\neg\text{Can}(u,r)$: "for every resource, some user is denied it." The finding to report is, for each resource, a user who cannot reach it — a denied witness per resource.

🔗 Connection: Reporting "user carol, denied on all resources" is exactly what a property-based testing tool does when a forall property fails: it doesn't just say False, it hands you the minimal failing input. The negation law $\neg\forall x\,P(x) \equiv \exists x\,\neg P(x)$ is the reason such a witness always exists to be reported (§2.4). A failed universal is never just "no" — it is always "no, here."

🔄 Check Your Understanding Suppose the policy also required R5: "no user holds zero roles" (every account is provisioned), written $\forall u\,\exists \rho\,(\rho \in \text{roles\_of}[u])$ — i.e. $\neg\,\exists u\,(\text{roles_of}[u] = \emptyset)$. Over the data, is R5 true? If not, give the witness the negation produces.

Answer

R5 is false: dan holds no roles (set()). The negation $\exists u\,(\text{roles_of}[u] = \emptyset)$ produces the witness dan — an unprovisioned account. (This is also why dan is an R1 orphan: no roles means no access to anything.)

Phase 4: The policy is a specification

Step back. What we just did is §2.6 at the level of a whole system. The policy is a precondition the live permission data must satisfy — a conjunction of quantified statements that should be true before the system is trusted in production:

$$\text{Policy} \;=\; R1 \land R2 \land R3 \land R4 \land \dots$$

Checking the policy is evaluating that conjunction over the current data — and a single false conjunct ($R1$, here) makes the whole policy false, exactly as one bad element sinks a universal (§2.2). A CI gate that runs these checks on every deploy is doing for permissions what assert is_sorted(arr) does for binary search in §2.6: refusing to trust the system until its quantified precondition holds.

And here is theme two, sharp: an engineer who logs in as alice, sees everything works, and ships has verified one conjunct of a giant $\land$. The audit checks the whole $\forall$ — over every user, every resource — and finds carol and dan that the spot check never touched. "It worked for the account I tried" is one true conjunct; "the policy holds" is the entire quantified statement, and only an exhaustive check (over a finite domain) or a proof (over an infinite one) settles it.

Discussion Questions

1. R1 and R2 differ only in quantifier order, yet R2 is a much stronger requirement. Give a realistic product reason a team might want only R1 (no orphaned users) but deliberately not R2 (no universal resource). What would R2 being true imply about the audit log?
2. We evaluated each rule over finite domains, so the all/any checks are exhaustive — they really do settle the universal over users and resources. Contrast this with §2.6's binary-search precondition over an infinite input domain. When is "evaluate the quantifier in code" a proof, and when is it only evidence?
3. R3 used a restricted universal with $\rightarrow$ and turned out vacuously true for four of five users. Suppose a misconfiguration granted bob (an agent) access to the audit log. Re-trace R3: which row flips, and what does the negation of R3 report as the finding?
4. The first_orphan finder returns only the first witness. Rewrite the requirement so that the audit must report all orphans. Does this change the underlying logic ($\exists$ vs. $\forall$), or only the reporting?

Your Turn: Extensions

• Option A (full report). Modify the audit to produce, for every failed rule, the complete list of witnesses (all orphans for R1; per-resource denied users for R2). State, for each, the negated formula whose witnesses you are listing.
• Option B (role hierarchy). Real systems have role inheritance: admin implies agent implies viewer. Redefine can_access so that holding a higher role grants lower-role resources, then re-evaluate R1–R4 by hand. Which rule's truth value changes, and why?
• Option C (toolkit). Re-express R1–R4 using the Toolkit's for_all, there_exists, and counterexample from this chapter's Project Checkpoint (in dmtoolkit/logic.py). Show that counterexample over a cleverly chosen predicate reproduces the first_orphan finding, and explain the duality counterexample(P, D) is None $\iff$ for_all(P, D).

Key Takeaways

1. A policy is a quantified specification. Each English rule is a $\forall$ or $\exists$ (often nested) over named domains; the policy as a whole is their conjunction — a precondition the live system must satisfy (§2.6).
2. Classify the quantifier first, then pick the connective. Restricted universals take $\rightarrow$ (R3); existentials take $\land$ (R4). Swapping them silently changes the rule (§2.2).
3. Order is meaning. R1 ($\forall u\,\exists r$) and R2 ($\exists r\,\forall u$) read almost alike but state very different requirements; R2 implies R1, never the reverse (§2.3).
4. Negation hands you the finding. A failed universal is never just "false" — pushing $\neg$ inward produces the exact witness ("a user denied on all resources," carol) an auditor must report (§2.4).
5. Spot-checking is one conjunct; auditing is the whole $\forall$. Logging in as one account verifies a single element; only evaluating the quantifier over the entire (finite) domain — or proving it over an infinite one — settles the policy (theme two).