OpenCyber AcademyLesson map
Lesson 01 published. Map, example, EX001.
flowchart TD
N0["Learning outcomes"]
N1["1.1 Statements and quantifiers"]
N2["1.2 Proof techniques"]
N3["1.3 Functions and vectors"]
N4["1.4 Optimisation"]
N5["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5
N5 --> EX["Worked example"]
EX --> Q["Exercise EX001"]
Logical drawing
flowchart LR
N0["Learning outcomes"]
N1["1.1 Statements and quantifiers"]
N2["1.2 Proof techniques"]
N3["1.3 Functions and vectors"]
N4["1.4 Optimisation"]
N5["Synthesis"]
N0 --> N1 --> N2 --> N3 --> N4 --> N5 --> Q["EX001"]
[Learning outcomes]
|
v
[1.1 Statements and quantifiers]
|
v
[1.2 Proof techniques]
|
v
[1.3 Functions and vectors]
|
v
[1.4 Optimisation]
|
v
[Synthesis]
|
v
[Worked example] --> [Exercise EX001]
Learning outcomes
You will (1) read and write precise mathematical statements; (2) use proof techniques (direct, contradiction, counterexample) to reason about security claims; (3) work with functions, vectors and simple optimisation; and (4) see why a single counterexample defeats a universal security claim.
1.1 Statements and quantifiers
Security claims are mathematical statements in disguise. "Ask Lumen never reveals another patient's appointment" means: for all inputs and for all users, the output contains no other patient's data. A universal statement ("for all") is refuted by one counterexample; an existential statement ("there exists an attack") is proved by exhibiting one. This asymmetry explains why attackers have an advantage: they need one working input, while defenders must cover all.
Writing the claim out exposes what must be checked: every user, every input, every route by which data reach the output, including retrieved documents and tool results.
1.2 Proof techniques
Direct proof derives the conclusion from assumptions. Proof by contradiction assumes the opposite and derives an impossibility. Proof by counterexample refutes a universal claim. In AI security, proofs are rare for whole systems but common for components: "if the policy service denies every tool call without a valid token, then no unauthenticated booking occurs" is a direct proof from a design property.
The design-property proof is only as good as its assumption: if any path reaches the booking system without passing the policy service, the conclusion fails. Checking that assumption is an architecture task, which later chapters automate with graph search.
1.3 Functions and vectors
A model is a function from inputs to outputs. Inputs such as images or feature records are vectors; distance between vectors (for example Euclidean distance or the maximum absolute difference) formalises "small change". Many attacks search for a nearby vector that produces a different output (Szegedy et al., arXiv:1312.6199).
The choice of distance matters. Under the maximum absolute difference, every feature may change by up to a fixed amount at once; under Euclidean distance, a large change in one feature uses up the whole budget. The evasion lab later uses the first kind, so its perturbation size eps bounds the change in each coordinate separately. A claim of robustness means nothing until the distance and its size are stated.
1.4 Optimisation
Training minimises a loss function; attacks maximise it (or minimise distance subject to a changed output). Both are optimisation problems, which is why the same mathematical tools — gradients, constraints, search — appear on both sides.
The evasion lab shows both sides in a few lines. Training adjusts the weights against the gradient of the loss to reduce error; the attack moves each test point along the sign of the same gradient with respect to the input to increase error. At eps of 0.5 the toy model's accuracy falls from 0.985 to 0.840, which shows how little effort a gradient-guided search needs when the model is simple.
1.5 Worked example (synthetic LCH case)
LCH's vendor claimed: "NoShow cannot be manipulated by patients." Rina rewrote it as a universal statement: for all patients and all values of the fields patients control (contact preferences, stated reason for visit), the prediction does not change in a way the patient prefers. She then found a counterexample on a synthetic record: changing "reason" from "follow-up" to "urgent" lowered the predicted no-show risk from 0.42 to 0.18, which could move a patient up a reminder list. The claim was false as stated; the vendor revised it.
1.6 Errors and limits
- Accepting universal claims tested on a few examples.
- Confusing "no attack found" with "no attack exists".
- Vague notions of "small change" with no distance measure.
The NoShow example shows all three. The vendor's claim was tested on ordinary records only; nobody had looked for a field change that patients control; and "manipulated" had no stated measure. Rina's counterexample, a change from 0.42 to 0.18 caused by one field, settled the question at once. A revised claim would name the fields, the size of change considered acceptable and how it was tested.
Exercises
- EX001 — Quantifiers. Write "the filter blocks all injection attempts" with explicit quantifiers and say what refutes it. Rubric: 3 = ∀ inputs in class, blocked; one unblocked instance refutes; 2 = partial; 1 = vague; 0 = none.
- EX002 — Counterexample. Why did one record refute the vendor's claim? Rubric: 3 = universal claim falsified by one instance; 2 = partial; 1 = vague; 0 = wrong.
- EX003 — Distance. For x = (1, 2, 3) and y = (1.5, 2, 2), compute Euclidean and max-absolute distances. Rubric: 3 = √(0.25 + 0 + 1) ≈ 1.118 and 1; 2 = one; 1 = method; 0 = none.
Synthesis
Mathematical reasoning makes security claims precise. Universal claims need strong evidence; one counterexample is enough to refute them; "small" needs a distance.