Case Study: Auditing an Access-Control Condition with Truth Tables

"The most dangerous bugs are the ones that pass every test you thought to write."

Executive Summary

A security review lands on your desk. A single if statement decides who can delete a record in a shared document system, and an auditor suspects it lets the wrong people through. You will treat that condition as a compound proposition, build its truth table to see its behavior on every possible input at once, compare it against the intended policy written as a second proposition, and use logical equivalence to prove exactly where — and why — the code diverges from the spec. No test suite is involved, and that is the point: a four-variable condition has $2^4 = 16$ possible inputs, and the truth table checks all sixteen, whereas the three unit tests in the pull request checked three. This is §1.3 (truth tables) and §1.4 (equivalence) applied to a bug that is invisible to spot-checking but obvious to a truth table.

Skills applied

• Translating an English access-control policy into propositional logic (§1.2).
• Building and reading a truth table for a four-variable condition (§1.3).
• Comparing two propositions column-by-column to locate disagreement (§1.4).
• Using De Morgan's laws and the contrapositive to prove, not guess, what a condition tests (§1.4).
• Connecting logical equivalence to safe refactoring and to short-circuit evaluation (§1.5).

Background

The scenario

A team runs a collaborative document tool. Each record has an owner; the workspace has admins; records can be locked (e.g., during a legal hold); and users have roles. The product spec for who may delete a record reads, verbatim:

"A user may delete a record if they are an admin, or if they are the record's owner — but in no case may a record be deleted while it is locked."

A developer implements it as:

def can_delete(is_admin, is_owner, is_locked):
    """Return True if the user may delete the record."""
    return is_admin or is_owner and not is_locked

# The three tests in the pull request:
print(can_delete(True,  False, False))   # admin, not owner, unlocked -> expect True
print(can_delete(False, True,  False))   # owner, unlocked           -> expect True
print(can_delete(False, False, False))   # nobody special            -> expect False
# Expected output:
# True
# True
# False

All three tests pass, the reviewer approves, and the code ships. The auditor's worry is specific: can an admin delete a locked record? The spec says "in no case … while it is locked." Let us find out — not by adding a test, but by examining every case.

💡 Intuition: A unit test is a single row of a truth table. Three passing tests tell you the function is correct on three of its sixteen inputs. The other thirteen rows are exactly where bugs hide. A truth table is the test suite that leaves no row unchecked.

Why this matters

Authorization logic is where a one-character mistake becomes a breach. The streaming-service bug in §1.1 (a missing pair of parentheses let a twelve-year-old subscriber through an age gate) was the same species of error: a condition that reads like the requirement but evaluates differently because of operator precedence. Here the stakes are deletion of records under legal hold. Getting the logic provably right is not pedantry; it is the job.

Phase 1: Translate the spec into a proposition

We isolate the propositional variables. Let

• $a$ = "the user is an admin,"
• $o$ = "the user is the record's owner,"
• $\ell$ = "the record is locked,"

and let $D$ stand for the policy "the user may delete the record." Read the spec one clause at a time. "An admin, or the owner" is $a \lor o$. "But in no case while it is locked" is an overriding restriction: whatever the first part says, deletion is forbidden when $\ell$ holds. The cleanest way to encode "permission, but never when locked" is to and the permission with $\neg \ell$:

$$D \;\equiv\; (a \lor o) \land \neg \ell.$$

This is the intended policy. Notice the parentheses around $a \lor o$: the lock restriction applies to admins and owners alike, because the spec says "in no case." That word "no case" is doing real work — it tells us the $\neg \ell$ binds to the whole permission, not just to one branch.

🔄 Check Your Understanding In the intended policy $D = (a \lor o) \land \neg \ell$, can an admin ($a = T$) delete a locked record ($\ell = T$)?

Answer

No. With $\ell = T$ we have $\neg \ell = F$, and $\text{anything} \land F \equiv F$ by the domination law (§1.4). So $D = F$ regardless of $a$ and $o$. The lock is an absolute veto — exactly what "in no case" demands.

Phase 2: Translate the code into a proposition

Now read the code, respecting Python's precedence rules from §1.2 ($\neg \succ \land \succ \lor$). The expression is

is_admin or is_owner and not is_locked

Python binds and tighter than or, and not tighter still. So the implicit grouping is

$$C \;\equiv\; a \lor \big(o \land \neg \ell\big),$$

where $C$ is the coded condition. This is not the same as the intended $D = (a \lor o) \land \neg \ell$. The difference is exactly one pair of parentheses — the lock restriction in the code applies only to the owner branch, leaving the admin branch unguarded. The auditor's suspicion now has a precise shape. But "looks different" is not "is different"; two differently parenthesized expressions can still be equivalent (we will see one in Phase 5). We must compare them on every input.

⚠️ Common Pitfall: Do not eyeball precedence and move on. The whole streaming bug of §1.1 came from trusting that the code "reads like" the spec. The reliable move is to make the grouping explicit ($a \lor (o \land \neg \ell)$) and then check it, not assume it.

Phase 3: Build both truth tables side by side

Three variables means $2^3 = 8$ rows. We compute the intended policy $D = (a \lor o) \land \neg \ell$ and the coded condition $C = a \lor (o \land \neg \ell)$ in one table, with helper columns, using the chapter's convention ($T$ before $F$, counting down).

Now compare the two output columns, $D$ and $C$, row by row. They agree in six rows. They disagree in exactly two:

• Row 1 ($a=T, o=T, \ell=T$): an admin who is also the owner, on a locked record. $D = F$ (forbidden), but $C = T$ (the code allows it).
• Row 3 ($a=T, o=F, \ell=T$): an admin who is not the owner, on a locked record. $D = F$ (forbidden), but $C = T$ (the code allows it).

The pattern is unmistakable: the two disagreements are precisely the rows where the user is an admin and the record is locked ($a = T, \ell = T$). On those inputs, the code grants deletion of a locked record. That is the vulnerability — and it is exactly the case the auditor named and the case none of the three unit tests exercised.

💡 Intuition: Reading a truth table is detective work: line up the "what we wanted" column next to the "what we got" column and look only at the rows where they differ. Those rows are the bug report, stated as concrete inputs you can reproduce.

Phase 4: Prove the divergence (don't just observe it)

A truth table shows the disagreement; the algebra of §1.4 explains it and lets us name the bug precisely. Compute the proposition "$C$ is true but $D$ is false" — the set of inputs where the code over-permits:

$$C \land \neg D.$$

Substitute and simplify. With $C = a \lor (o \land \neg\ell)$ and $D = (a \lor o) \land \neg\ell$, first negate $D$ using De Morgan and the negated-conjunction rule:

$$ \begin{aligned} \neg D &\equiv \neg\big((a \lor o) \land \neg \ell\big) \\ &\equiv \neg(a \lor o) \lor \neg(\neg \ell) && \text{(De Morgan's law)}\\ &\equiv (\neg a \land \neg o) \lor \ell && \text{(De Morgan again, and double negation)}. \end{aligned} $$

So $\neg D \equiv (\neg a \land \neg o) \lor \ell$: the policy is violated either when nobody is authorized or when the record is locked. Now intersect with $C$. We are after the part of $C$ that $D$ forbids, and the term that matters is the $\ell$ disjunct (the lock). Focus on inputs with the admin branch active, $a = T$:

$$ \begin{aligned} C \land \neg D &\equiv \big(a \lor (o \land \neg\ell)\big) \land \big((\neg a \land \neg o) \lor \ell\big). \end{aligned} $$

Rather than expand all of it, read off the dangerous slice directly: take $a = T$ and $\ell = T$. Then $C = T \lor (\dots) = T$ (the admin branch fires, ignoring the lock), while $\neg D = (\dots) \lor T = T$ (the lock makes the policy violated). So $C \land \neg D = T$ on *every* row with $a = T, \ell = T$ — both values of $o$. That is rows 1 and 3 of the table, derived now by algebra rather than read off by eye. Two methods, one answer (theme four): the table computed the disagreement on all eight rows; the algebra proved which rows and why — the admin branch was never guarded by $\neg \ell$.

🔗 Connection. We just used the De Morgan laws of §1.4 to push a negation through a conjunction and a disjunction, flipping each connective as it moved inward. This is the single most common manipulation in reasoning about access control: "when is the policy violated?" is the negation of "when is it satisfied?", and De Morgan is how you compute it cleanly.

Phase 5: The fix, and proving the fix is right

The repair is the parentheses the spec implied all along:

def can_delete(is_admin, is_owner, is_locked):
    return (is_admin or is_owner) and not is_locked

This encodes $D = (a \lor o) \land \neg \ell$ exactly. But before we trust it, notice a subtler question a careful reviewer would ask: is there a different-looking but equivalent way to write it that reads better? The lock is an absolute veto, so a reviewer proposes the "guard-first" form:

def can_delete(is_admin, is_owner, is_locked):
    if is_locked:
        return False
    return is_admin or is_owner

Is this provably the same as $D$? The early return says: if $\ell$, the answer is $F$; otherwise the answer is $a \lor o$. As a proposition that is $\neg \ell \land (a \lor o)$ — which, by the commutative law (§1.4), is $(a \lor o) \land \neg \ell = D$. So the guard-first version is logically equivalent to the corrected condition; both are correct, and either may ship. This is §1.5's lesson in miniature: an equivalence proves a refactor is safe, where "the tests still pass" only suggests it.

🔗 Connection — short-circuit evaluation. The guard-first form has a practical edge that pure logic cannot see (§1.5). If checking the lock is cheap but checking ownership requires a database call, testing is_locked first and returning early avoids that call on locked records. Logically $\neg \ell \land (a \lor o) \equiv (a \lor o) \land \neg \ell$, but in code the order of evaluation changes how much work runs. Equivalence governs truth values; it does not govern cost or side effects.

🐛 Find the Error: A teammate "simplifies" the corrected condition to is_admin or is_owner and not is_locked — claiming "it's the same connectives, so it's the same condition." Which specific row of the Phase 3 table refutes them, and which law explains why dropping the parentheses is not allowed here?

Answer

Row 1 (or row 3): $a=T, o=T, \ell=T$ (resp. $a=T, o=F, \ell=T$) gives $D=F$ but the unparenthesized form $C = T$. The error is treating $\lor$ and $\land$ as freely regroupable; they are not — there is no associative law across different connectives. Only the distributive law relates $\land$ and $\lor$, and $(a \lor o)\land\neg\ell$ distributes to $(a\land\neg\ell)\lor(o\land\neg\ell)$, which is not $a \lor (o \land \neg\ell)$.

Discussion Questions

1. The bug was an over-permission (the code said yes where the spec said no). Construct a different one-parenthesis edit to the original buggy line that instead produces an under-permission (denies someone the spec allows). Which rows of a truth table would reveal it?
2. We modeled "in no case while locked" as $\land \neg \ell$ applied to the whole permission. Suppose the spec instead read "admins may delete even locked records; owners may not." Rewrite $D$, and identify which of the two functions in Phase 5 (if either) now matches.
3. The corrected condition has $2^3 = 8$ rows. If we added a fourth factor — say "the workspace is not in read-only mode," $r$ — how many rows would the table have, and write the new $D$.
4. The auditor found this by reasoning about cases, not by testing. Argue, using the numbers in this case study, why a test suite would need to be unusually thorough to catch this class of bug, and why a truth table is the natural tool instead. (Tie this to theme two: "it passed the tests" is not "it is correct.")
5. In Phase 4 we computed $\neg D$ to find where the policy is violated. Explain why "the set of inputs a buggy condition wrongly allows" is always $C \land \neg D$, and "the set it wrongly denies" is always $\neg C \land D$.

Your Turn: Extensions

• Option A (full equivalence check in code). Using the chapter's equivalent(f, g, n) from the Project Checkpoint, write the few lines that confirm the original buggy can_delete and the corrected one are not equivalent (and that the corrected one and the guard-first one are). State the expected True/False outputs by hand, and explain what a False from equivalent tells you that a passing test does not.
• Option B (a four-variable policy). Add the read-only-mode factor $r$ from Discussion Question 3. Write can_delete(is_admin, is_owner, is_locked, read_only), build the $16$-row truth table for the corrected policy, and verify by inspection that deletion is forbidden in every row where $\ell$ or $r$ holds.
• Option C (negation as a policy report). Write a proposition for "the record is protected" — i.e., no one may delete it — and simplify it with De Morgan. (Hint: "protected" is $\neg D$ holding for all users, which reduces to a statement about $\ell$ alone once you treat $a$ and $o$ as "some user is an admin/owner." Discuss what assumption that requires.)

Key Takeaways

1. A condition is a proposition; a unit test is one of its rows. Three passing tests certified three of sixteen inputs. The truth table certified all sixteen — and the bug lived in a row no test touched.
2. Precedence bugs hide in plain sight. $a \lor (o \land \neg\ell)$ and $(a \lor o) \land \neg\ell$ differ by one pair of parentheses and disagree on exactly the locked-admin rows. Make grouping explicit, then verify it.
3. De Morgan turns "when is it satisfied?" into "when is it violated?" Computing $\neg D$ — and the over-permission set $C \land \neg D$ — is the standard way to prove where a guard leaks.
4. Equivalence is what makes a refactor safe. The guard-first rewrite was provably the same policy by the commutative law; that is a guarantee no test can give. And short-circuit evaluation can make one equivalent form cheaper than another — logic settles truth, not cost.