OpenCyber AcademyLearning outcomes
You will (1) express security policies as logical statements; (2) test a policy with a truth table; (3) spot contradictions and gaps in written rules.
1.1 The case and logic
Lucas Haddon is a first-year student on a four-year bachelor's programme at the fictional Ashgrove University, tutored by Dr Marco Bellini. From the second year he also works part-time at the fictional Fernway Outdoor Co-operative, a member-owned retailer with an online shop, a warehouse and two stores, under its IT security lead Hannah Osei. Every person, organisation and figure here is synthetic. Dr Bellini starts with logic because security policies are logical statements. A rule such as staff may issue refunds if they are store managers or the amount is under twenty pounds and a receipt exists can be written with AND, OR and NOT, and then checked precisely.
1.2 Truth tables for policy
Lucas writes the refund rule as a formula with three conditions: M for manager, S for small amount and R for receipt. The English sentence is ambiguous: does the receipt requirement apply to managers too? He writes both readings, M OR (S AND R) and (M OR S) AND R, and builds a truth table for each. The lab below prints both tables and the rows where they disagree. Those rows are real cases, such as a manager refunding without a receipt, where staff following different readings would act differently. Logic exposes ambiguity before it becomes an argument at a till.
Lab — Two readings of a refund rule
# Truth tables for two readings of a refund policy (M manager, S small amount, R receipt).
from itertools import product
a = lambda M, S, R: M or (S and R)
b = lambda M, S, R: (M or S) and R
diff = 0
print(" M S R | A B")
for M, S, R in product([0, 1], repeat=3):
x, y = int(a(M, S, R)), int(b(M, S, R)); diff += x != y
print(f" {M} {S} {R} | {x} {y}{' <- differ' if x != y else ''}")
print("rows that differ:", diff)
Run with python3 lab_truth.py. Verified output:
M S R | A B
0 0 0 | 0 0
0 0 1 | 0 0
0 1 0 | 0 0
0 1 1 | 1 1
1 0 0 | 1 0 <- differ
1 0 1 | 1 1
1 1 0 | 1 0 <- differ
1 1 1 | 1 1
rows that differ: 2
1.3 Gaps and contradictions
Policies also contain gaps, where no rule applies, and contradictions, where two rules give opposite answers. Fernway's draft remote-access policy says contractors must use the VPN and that warehouse scanners never use the VPN; it is silent about contractors maintaining scanners. Lucas lists the combinations systematically and finds that case. Systematic enumeration is a simple mathematical habit, but it catches the situations that informal reading misses. He recommends adding an explicit rule and a default: anything not explicitly permitted is denied, the fail-safe default of Saltzer and Schroeder (1975).
Worked example
Lucas formalises a refund rule two ways, finds the rows where readings disagree and identifies an uncovered contractor-scanner case in a remote-access policy.
Synthetic case. Ashgrove University, Fernway Outdoor Co-operative, Lucas, Hannah and Dr Bellini are invented; Saltzer and Schroeder (1975) is real.
Errors and limits
Real policies include context that formulas omit, such as emergencies. Enumeration grows quickly with many conditions.
Exercises
- EX001 — Two readings. Write the two readings of the refund rule in logic.
Show marking criteria
Rubric: 3 = M OR (S AND R) and (M OR S) AND R;; 2 = one;; 1 = vague;; 0 = none. - EX002 — Disagreeing rows. According to the lab, in how many rows do the readings disagree, and what do they share?
Show marking criteria
Rubric: 3 = 2 rows, both a manager without a receipt;; 2 = count and pattern;; 1 = vague;; 0 = none. - EX003 — Policy gap. What gap did Lucas find in the remote-access policy?
Show marking criteria
Rubric: 3 = contractors maintaining warehouse scanners;; 2 = case;; 1 = vague;; 0 = none.
Synthesis
Writing policies as logic reveals ambiguity, gaps and contradictions before they cause inconsistent decisions.