Formal Methods
State security requirements or policy as a set of constraints
Negations of the constraints form primitives
Rationale: vulnerabilities are violations of policy, e.g., policy constraints
Needed: a technique to rigorously perform the breakdown from constraints to primitives