Choose a relational question

The browser scene has three principals: Page, Library, and Attacker. A policy relates a nonce to its trusted root and a loader to the script it loads. The security question asks whether Attacker belongs to the transitive closure of loader edges reachable from a trusted root.

module CspTrust

abstract sig Principal {}
one sig Page, Library, Attacker extends Principal {}

one sig Policy {
  nonce: set Principal,
  loads: Principal -> Principal
}

fun executable[p: Policy]: set Principal {
  p.nonce.*(p.loads)
}

pred buggy[p: Policy] {
  p.nonce = Page
  p.loads = Page -> Library + Library -> Attacker
}

pred fixed[p: Policy] {
  p.nonce = Page
  p.loads = Page -> Library
}

assert FixedPolicyIsSafe {
  all p: Policy | fixed[p] implies Attacker not in executable[p]
}

run BugAdmitsAttacker {
  some p: Policy | buggy[p] and Attacker in executable[p]
} for 3 but exactly 3 Principal, exactly 1 Policy

check FixedPolicyIsSafe for 3 but exactly 3 Principal, exactly 1 Policy

run UsefulScriptCanRun {
  some p: Policy | fixed[p] and Library in executable[p]
} for 3 but exactly 3 Principal, exactly 1 Policy

Run all three commands:

alloy exec CspTrust.als

Read each command by name. BugAdmitsAttacker must be satisfiable. FixedPolicyIsSafe must have no counterexample in the declared scope. UsefulScriptCanRun must remain satisfiable. The last command protects against a useless repair that blocks every script.

Read SAT and UNSAT in context

For a run command, SAT means Alloy found at least one instance satisfying the predicate. For a check command, SAT means Alloy found a counterexample to the assertion. UNSAT means no counterexample exists within the scope and model. Those meanings depend on the command kind.

Connect the graph to CSP

The model isolates one part of Content Security Policy Level 3: trust propagation from nonce- or hash-authorized scripts under strict-dynamic. The real browser also applies parser state, element types, source lists, redirects, module loading rules, and version-dependent behavior. The three-node relation does not replace browser conformance tests.

The graph still earns its keep. A review can ask who creates each script element, which principals can influence its URL or bytes, and whether a trusted loader accepts attacker-controlled input. The model makes an inherited trust edge visible before deployment.

The browser's other CSP, Communicating Sequential Processes, appears in the capstone as a way to describe conversations. The shared acronym does not imply a shared formalism.

Practice

1. Add a second safe library and let Page load both libraries.
2. Add a loader edge from the safe library to Attacker. Predict which command changes verdict.
3. Explain why FixedPolicyIsSafe alone could approve a policy that executes no useful code.

Worked answer

1. Add one principal and one Page -> Library2 edge. Increase the exact principal scope to four.
2. FixedPolicyIsSafe becomes SAT because the new edge creates a trusted path to Attacker.
3. The assertion speaks only about attacker reachability. A policy with an empty nonce set satisfies safety by blocking every script. UsefulScriptCanRun supplies a non-vacuity witness.

Lessons

• Alloy fits questions about relations, reachability, and forbidden shapes.
• run searches for an example; check searches for a counterexample.
• SAT has a different reading for run and check.
• Security checks need usefulness witnesses to resist deny-everything repairs.
• A CSP trust graph complements browser conformance tests; it does not replace them.

References

1. Alloy Project. “Alloy Documentation.” — language, analyzer, and learning material.
2. World Wide Web Consortium. “Content Security Policy Level 3.” W3C. — script authorization and strict-dynamic semantics.