Logic structuring for security code
Advanced logic structuring that makes security code correct by construction and easy to review: state machines, decision tables, invariants, pure decision functions, parse-don't-validate, fail-closed totality and property tests, and how to hand that structure to an AI.
01State machines and decision tables
- Model security behaviour as an explicit state machine and decision table
- Write invariants and separate pure decisions from I/O
- Use parse, don't validate types and fail-closed total functions
- Check the structure with property-based tests, and prompt an AI with it
Most security bugs are logic bugs: a state the author did not think about, a combination of flags nobody tested, a branch that falls through to "allow". The fix is to make the logic explicit and enumerable. If every state and every transition is written down, the gaps are visible in review instead of in an incident.
Take an account lockout flow. Implicit version: a handful of booleans (locked, mfaPending, failedCount > 5) scattered across handlers. Explicit version: a state machine where illegal transitions cannot be expressed.
| State | Event | Next state | Side effect |
|---|---|---|---|
| active | login_fail (count < 5) | active | increment counter |
| active | login_fail (count = 5) | locked | emit lockout alert |
| active | login_ok | mfa_pending | send challenge |
| mfa_pending | mfa_ok | authenticated | issue session, reset counter |
| mfa_pending | mfa_fail | active | increment counter |
| locked | admin_unlock | active | audit log |
| locked | any other | locked | none (deny) |
A decision table does the same for policy: every combination of inputs mapped to an outcome. If a row is missing, the table shows it. If two rows conflict, the table shows that too. Authorisation, alert routing and response playbooks all fit decision tables well.
- ACTOR
- SERVICE
- DATA
- STREAM
- Live flow
- Lookup / async
02Invariants, pure decisions and parsed types
An invariant is a statement that must always be true: "a session never exists for a locked account", "every alert belongs to exactly one tenant", "a token is never accepted after its expiry". Write them down; they become assertions, tests and review questions.
Then separate decisions from I/O. The function that decides whether an action is allowed should be pure: data in, decision out, no database calls, no clock reads, no logging. Pure functions are trivially testable, and the I/O shell around them is thin enough to review line by line.
// Parse, don't validate: untrusted input becomes a type that cannot be invalid.
type TenantId = string & { readonly __brand: "TenantId" };
type Role = "viewer" | "analyst" | "admin";
type Action = "alert.read" | "alert.close" | "rule.edit" | "host.isolate";
interface Principal { userId: string; tenantId: TenantId; role: Role }
interface Resource { tenantId: TenantId; kind: "alert" | "rule" | "host" }
type Decision = { allow: true } | { allow: false; reason: string };
function parseTenantId(raw: unknown): TenantId | null {
return typeof raw === "string" && /^t_[a-z0-9]{12}$/.test(raw) ? (raw as TenantId) : null;
}
// The decision table, as data. Anything not listed is denied.
const GRANTS: Record<Role, readonly Action[]> = {
viewer: ["alert.read"],
analyst: ["alert.read", "alert.close"],
admin: ["alert.read", "alert.close", "rule.edit", "host.isolate"],
};
// Pure and total: every input yields a decision, the default is deny.
export function decide(p: Principal, action: Action, r: Resource): Decision {
if (p.tenantId !== r.tenantId) return { allow: false, reason: "cross-tenant" };
if (!GRANTS[p.role].includes(action)) return { allow: false, reason: "role" };
return { allow: true };
}Parse, don't validate means turning untrusted input into a narrower type exactly once, at the boundary. After parseTenantId succeeds, the rest of the code holds a TenantId and never re-checks it, and nothing can pass a raw string where a TenantId is expected. Validation that returns a boolean and keeps the raw string is easy to forget on the next code path.
03Fail closed, handle every case, test properties
A total function handles every possible input. In TypeScript, a discriminated union plus an exhaustiveness check makes the compiler enforce it: add a new case and every switch that forgot it stops compiling.
type Verdict = "malicious" | "suspicious" | "benign" | "unknown";
function assertNever(x: never): never {
throw new Error("unhandled case: " + String(x));
}
function responseFor(v: Verdict): "isolate" | "ticket" | "close" {
switch (v) {
case "malicious": return "isolate";
case "suspicious": return "ticket";
case "unknown": return "ticket"; // fail closed: unknown is never auto-closed
case "benign": return "close";
default: return assertNever(v); // a new Verdict breaks the build here
}
}Fail closed means the default outcome, on error or on an unexpected input, is the safe one: deny access, keep the alert open, refuse the request. A catch block that returns true, or an else that allows, is the classic fail-open bug.
Property-based tests check invariants over thousands of generated inputs rather than a few hand-picked examples. They are where invariants pay off.
import fc from "fast-check";
const role = fc.constantFrom<Role>("viewer", "analyst", "admin");
const action = fc.constantFrom<Action>("alert.read", "alert.close", "rule.edit", "host.isolate");
const tenant = fc.stringMatching(/^t_[a-z0-9]{12}$/).map((s) => s as TenantId);
test("never allows a cross-tenant action", () => {
fc.assert(fc.property(role, action, tenant, tenant, (ro, a, t1, t2) => {
fc.pre(t1 !== t2);
const d = decide({ userId: "u", tenantId: t1, role: ro }, a, { tenantId: t2, kind: "alert" });
return d.allow === false;
}));
});
test("viewers can never change state", () => {
fc.assert(fc.property(action, tenant, (a, t) => {
const d = decide({ userId: "u", tenantId: t, role: "viewer" }, a, { tenantId: t, kind: "alert" });
return a === "alert.read" || d.allow === false;
}));
});The compiler proves every case is handled, not that each case is handled well. Mapping unknown to close compiles fine. The decision table and its review are still where correctness lives.
04Pseudocode to spec to code, and prompting with structure
Work in three steps. Pseudocode to agree the shape with yourself or a colleague. Spec: types, state table, decision table and invariants. Code: the smallest implementation that satisfies the spec and its tests. AI is most useful at the last step and as a critic of the second; it is least useful when asked to invent the first two from a vague sentence.
Implement decide(p: Principal, action: Action, r: Resource): Decision in TypeScript.
Types (do not change): <paste Principal, Resource, Action, Decision>
Decision table: <paste GRANTS>
Invariants:
1. If p.tenantId !== r.tenantId the result is deny with reason "cross-tenant".
2. Any (role, action) pair not in the table is denied.
3. The function is pure: no I/O, no Date.now(), no logging, no exceptions.
Constraints: default deny; exhaustive over Role; no new dependencies.
Also: list any input for which the spec is ambiguous instead of guessing.The last line matters. Asking the model to surface ambiguity rather than resolve it silently turns it into a spec reviewer, which is one of the things it does well.
"For security logic I write the structure before any code: the types, the state or decision table, and the invariants. The decision is a pure, total function that defaults to deny, the boundary parses untrusted input into narrow types, and property tests check the invariants. When I use an assistant, I give it that structure, not a vague request, and I ask it to flag ambiguity."
In an authorisation decision function, the `catch` block around a policy lookup returns `{ allow: true }` so that users are not blocked by outages. What is the problem?
Q1Why keep the decision function pure?+
It can be tested exhaustively and with properties, reviewed in isolation, and reused in batch jobs or simulations. The I/O shell around it is small enough to check by eye.
Q2What is the benefit of branded types like TenantId?+
A raw string cannot be passed where a TenantId is expected, so the only way to get one is through the parser at the boundary. Forgetting to validate becomes a compile error.
Q3When is a state machine overkill?+
When there are two states and one transition. Once you have more than a couple of flags that interact, or any security consequence of an illegal transition, make it explicit.