Formal Methods experimental

Formal Methods Specifying systems, proving them correct, and producing the evidence a Common Criteria evaluation expects Foundations of formal reasoning. Propositional and predicate logic, invariants, the safety and liveness distinction, and the temporal logics the course reasons in.. Model a system property precisely in temporal logic.. Classify a property as safety or as liveness.. Identify both linear (LTL) and branching (CTL) temporal formulas.. Logic and invariants, Safety versus liveness, Linear temporal logic (LTL), Branching temporal logic (CTL) Foundations of formal reasoning Formal methods rest on a small set of ideas used with unusual precision: a system is a set of states and transitions, a specification is a formula some or all states and runs must satisfy, and verification is either exhaustive search over the state space or a logical proof. Every technique in this course, from an assertion checked by the model checker Simple Promela INterpreter (SPIN) to a Common Criteria evidence package, reduces to that same triple: states, a specification over them, and a method for deciding whether the specification holds. This lesson lays the propositional and temporal groundwork the rest of the course depends on. The vocabulary introduced here, invariants, safety, liveness, and the two dominant temporal logics, recurs unchanged through every later module, so precision now saves ambiguity later. Logic and invariants Propositional logic gives connectives (negation, conjunction, disjunction, implication) to combine boolean facts about one state: 'the lock is free'. Predicate logic adds quantifiers (for all, there exists) over a domain, so we can state 'for every process p, p is enabled or blocked' without naming processes. A system's behaviour is a Kripke structure: states, an initial-state predicate, and a transition relation. An invariant is a predicate holding in every state reachable from an initial state, not merely the initial state itself. Proving an invariant by induction on run length is the workhorse of this course: show it holds initially (initiation), then that if it holds in a state and a step is taken, it holds next (consecution). Both must be discharged, since an invariant merely true of every observed state is not yet known true of every reachable one. A predicate checked only against a handful of test runs offers no such guarantee, which is precisely the gap induction closes. Safety versus liveness Lamport's slogans become precise once formalised: a safety property says 'nothing bad ever happens'; a liveness property says 'something good eventually happens'. Alpern and Schneider (1985) proved this exhaustive: every property over infinite behaviours is the intersection of a safety and a liveness property. Safety is refuted by a finite prefix: once two processes are simultaneously in a critical section, no continuation undoes it, so a finite counterexample suffices, exactly what bounded model checking and invariant proofs catch. Liveness can never be refuted by a finite prefix, since the good event might still occur later; its counterexample is an infinite lasso (a stem followed by a repeating cycle) in which the event never occurs. This is why liveness needs fairness assumptions and demands different proofs and counterexample shapes than safety. Classifying a property correctly before attempting to check it therefore matters as much as the checking technique chosen afterward. Linear temporal logic (LTL) LTL, brought into computer science by Amir Pnueli (1977; 1996 Turing Award), reasons over a single infinite linear run. Its operators: G p (globally, p holds in every state), F p (eventually, p holds now or later), X p (p holds next), and p U q (p holds until q does). A safety property is typically G(safe_condition); a liveness property typically involves F, as in G(request => F response). A model satisfies an LTL formula only if every one of its runs does. Because LTL quantifies implicitly over all runs, checking an LTL property against a model with any nondeterminism means checking it against every interleaving the model admits. Branching temporal logic (CTL) CTL reasons over the branching tree of futures from a state; every temporal operator follows a path quantifier: A (all paths) or E (some path). 'All paths, Globally' (AG) p means p holds everywhere on every path (safety); 'there Exists a path, Finally' (EF) p means p is reachable on some path; 'on All paths, Finally' (AF) p means p is unavoidable on every path (strong liveness). CTL and LTL are incomparable: some LTL fairness-style properties have no CTL equivalent, and EF p has no LTL equivalent. SPIN works in the LTL tradition via never claims and Buchi automata; symbolic checkers favoured CTL for its binary decision diagram (BDD)-friendly fixpoint semantics. Knowing which logic a tool speaks bounds what it can express, and later modules return to this choice whenever a specification language commits to one tradition over the other. Modules 05 through 09 apply this same rigour where the Common Criteria's Evaluation Assurance Levels (EAL) require it. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Model checking with PROMELA and SPIN. Processes, channels, assertions and never claims, and the state-explosion problem that bounds exhaustive checking.. Model a small concurrent protocol in PROMELA.. Read a SPIN counterexample trail and explain the fault.. Describe state explosion and one technique that mitigates it.. Processes and channels, Assertions and never claims, Running SPIN, State explosion Model checking with PROMELA and SPIN SPIN, or Simple Promela INterpreter (SPIN), developed by Gerard Holzmann at Bell Labs, is an explicit-state model checker for concurrent and distributed systems; it takes a model written in PROMELA (Process Meta Language) and a temporal property, and either proves the property holds over every interleaving of the model's processes or produces a concrete counterexample. It is the paradigm example of model checking as exhaustive automatic search rather than proof by hand. Where module 00 introduced invariants and temporal logic as ideas, this module puts them to work against a real, runnable model, so the payoff of the earlier formalism becomes concrete. Processes and channels A PROMELA model is a fixed number of proctype processes running asynchronously; each has its own local variables and program counter, and the model also has global variables. Processes communicate chiefly through channels: chan c = [N] of { byte } is a bounded first-in-first-out (FIFO) queue of capacity N; c!msg sends and c?msg receives, and a channel of capacity 0 is a rendezvous, forcing sender and receiver to synchronise on the same step. Shared global variables are also possible, but channels are preferred whenever the model reflects message passing, since they make the communication topology explicit and checkable. Every statement is implicitly guarded: it is executable only when it can proceed without blocking, and SPIN's exploration considers, at each step, every process whose next statement is currently executable, interleaving them in every possible order. That interleaving semantics, not any single process's local control flow, is what makes concurrent models hard to reason about by inspection alone. Assertions and never claims The simplest correctness statement is assert(condition); if SPIN's exhaustive search ever reaches that statement with the condition false, it has found a genuine violation, since the search visits every reachable interleaving. Assertions check local, state-based (safety) conditions. To check properties spanning a whole run, PROMELA uses a never claim: a process, typically generated from a linear temporal logic (LTL) formula (SPIN negates the desired property into a Buchi automaton), designed to accept only on executions violating the property. SPIN searches for any interleaving accepted by the never claim; finding one means finding a violation, including liveness violations that manifest as an accepting cycle (a lasso) rather than a single bad state. An assertion alone cannot express that pattern, since a lasso is a property of an infinite run, not of any single state. Running SPIN SPIN has two modes. Simulation executes one interleaving at a time (randomly, interactively, or guided), useful for exploration but proving nothing. Verification compiles the model into a specialised C program that performs an exhaustive depth-first search, checking every assertion and the never claim on every path. When it finds a violation it produces a trail: a concrete, replayable sequence of steps from the initial state to the violating state, which SPIN can replay statement by statement. Reading that trail, identifying which interleaving produced the fault, is the central diagnostic skill, and what distinguishes a counterexample from a mere test failure: it is reproducible and complete. State explosion Reachable global states grow combinatorially, roughly the product of each process's local states, channel contents, and shared-variable values, so one more process or bounded integer can multiply the state space many times over. This state-explosion problem is the central obstacle to exhaustive checking. Practitioners mitigate it with partial-order reduction (exploring one representative ordering of independent, commuting statements), bitstate or hash-compaction search (hashing visited states into a bit array, trading completeness for memory), and symbolic representation with binary decision diagrams (BDDs), the technique introduced by McMillan circa 1990, the line of work for which Clarke, Emerson and Sifakis received the 2007 Turing Award. Choosing among these, and knowing when none suffices, is a skill this course returns to, since module 04 revisits decomposition and abstraction as complementary remedies to the same underlying problem. The same exhaustive-search discipline becomes a compliance requirement at the higher Evaluation Assurance Levels (EAL) modules 05 through 09 introduce. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Specifying systems with TLA+. Describing a system as a state machine in temporal logic: the next-state relation, invariants and PlusCal.. Write a state machine as a TLA+ next-state action.. State an invariant of a specification.. Use PlusCal to express an algorithm and translate it to TLA+.. State machines as actions, The next-state relation, Invariants, PlusCal Specifying systems with TLA+ TLA+ is built on the Temporal Logic of Actions (TLA), the logic of module 00 extended with the '+' layer of ordinary set-theoretic mathematics (sets, functions, records) needed to describe real data. Leslie Lamport designed it as a language for describing systems as mathematics: not pseudocode, not a diagram, but a logical formula whose models are exactly the allowed behaviours of the system. This lesson introduces actions, the next-state relation, invariants, and the PlusCal notation that compiles down to them. Each of these pieces reappears in module 03's model checking and proof, so the notation fixed here is used, not just introduced. State machines as actions In TLA+, a system is a state machine: a set of possible states (assignments of values to variables) and a rule describing which states may follow which. An action is a formula relating a current state to a next state, written with ordinary variables (x, y, ...) for current values and primed variables (x', y', ...) for next-state values. For example, Increment == x' = x + 1 relates any current x to a next value one greater. Actions are just predicate-logic formulas over an unprimed and a primed copy of the state, which is what makes them checkable: a step from state s to state t is legal exactly when the action is satisfied by substituting s for the unprimed and t for the primed variables. Nothing about an action is executable code; it is a formula that a state pair either satisfies or does not. The next-state relation A specification composes actions (Increment, Decrement, Reset) into a next-state relation Next, their disjunction: Next == Increment \/ Decrement \/ Reset. With an initial-state predicate Init, the canonical shape is Spec == Init /\ [][Next]_vars, where [][Next]_vars means 'in every step, either Next holds or vars are left unchanged (a stuttering step)'. Allowing stuttering is deliberate: it makes refinement well-behaved, since an implementation may take extra internal steps invisible to a more abstract specification. Fairness conditions (weak or strong, on selected actions) are conjoined to Spec whenever liveness properties must be established, ruling out runs that stutter forever on an enabled action. Module 03 returns to fairness only when a liveness property specifically requires it; most invariant work never needs it. Invariants An invariant in TLA+ is the module 00 notion made concrete: a state predicate, in the same language as Init and Next, that the TLA+ model checker (TLC) or the TLA+ Proof System (TLAPS) must show holds in every reachable state, not merely the initial one. TypeOK, a typical first invariant, asserts every variable lies in its intended domain (x \in Nat), catching basic modelling errors early. A Next relation that under-constrains some variable, leaving it free to take arbitrary values, typically shows up immediately as a TypeOK or safety-invariant violation, one of the most common and instructive classes of specification bug. Catching that class of error here, before a check ever runs against a larger model, is exactly why TypeOK is worth writing first. PlusCal Writing Next as a raw disjunction is precise but unwieldy for algorithms with sequential control flow. PlusCal, also by Lamport, looks like pseudocode with labelled steps, while, if, and process blocks, and translates mechanically into the underlying TLA+ Init and Next. The translation exposes exactly the state machine the algorithm implies, so everything modules 03 and 04 do with TLC and TLAPS applies unchanged. PlusCal is often the fastest route to a first specification; hand-written TLA+ actions suit specifications where the state machine, not an imperative algorithm, is the natural description. Engineers at Amazon Web Services reported (Newcombe et al., 2015) using this combination to find subtle concurrency bugs in core distributed systems before a line of production code was written. That same TLA+ discipline becomes mandatory evidence at the higher Evaluation Assurance Levels (EAL) modules 05 through 09 examine. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Checking and proving. Model checking a specification with TLC, strengthening an invariant until it is inductive, refinement, and an introduction to TLAPS proofs.. Apply TLC to check a specification's invariants.. Strengthen an invariant until it is inductive.. Explain refinement as one specification implementing another.. Model checking with TLC, Inductive invariants, Refinement, An introduction to TLAPS Checking and proving A TLA+ specification, built on the Temporal Logic of Actions (TLA), can be verified in two complementary ways: model checking it against a bounded instance with the TLA+ model checker (TLC), or proving properties of it deductively, for arbitrary parameter sizes, with the TLA+ Proof System (TLAPS). This lesson develops the technique bridging the two, the inductive invariant, and situates model checking and proof on a soundness-versus-scope trade-off. Which of the two a specifier reaches for first is rarely arbitrary: it follows directly from how large the state space is and how much of it must be covered. Model checking with TLC TLC is the explicit-state model checker for TLA+: given a specification and a configuration fixing parameter sizes (three processes rather than unbounded many), it enumerates every reachable state of that bounded instance and checks every declared invariant against all of them. When TLC reports no counterexample, the honest conclusion is precisely: the invariant held in every state of that bounded instance, no violation exists within the configured bounds. It is not a proof for every parameter value; a bug only manifesting with five processes will not appear when TLC runs with three. When TLC does find a violation, it delivers a counterexample as a finite trace from an initial state to the offending one, often the fastest way to discover a Next relation permits an unintended behaviour. That speed, seconds to a concrete counterexample, is why TLC is nearly always the first check run against a new specification, before any proof is attempted. Inductive invariants An inductive invariant can be verified locally, one step at a time, rather than by inspecting all reachable states directly: it has two obligations, initiation (Init => Inv) and consecution (Inv /\ Next => Inv', if Inv holds and a step is taken, Inv holds in the result). Discharging both by ordinary predicate logic establishes, by induction on run length, that Inv holds in every reachable state for every parameter size, a guarantee bounded model checking cannot give. Often a property is true of every reachable state but not itself inductive: consecution fails from some state satisfying Inv but not actually reachable. The remedy is to strengthen the invariant, conjoining conditions that exclude such pre-states, and recheck consecution; this strengthen-and-recheck cycle is the core discipline here. A solver-backed tactic can sometimes suggest the missing conjunct automatically, but confirming it is genuinely inductive remains the specifier's responsibility. Refinement Refinement is the relation in which one specification (typically lower-level) implements another (typically a more abstract statement of intent): every behaviour of the lower-level spec, mapped onto the abstract variables, is also allowed by the higher-level spec. This is why stuttering steps are permitted in TLA+'s [][Next]_vars form: an implementation may take extra internal steps invisible at the abstract level, appearing there as stuttering. Refinement lets a designer verify a small abstract specification thoroughly, then argue separately that a more detailed one refines it, rather than re-verifying every property at every level of detail. Module 07 gives this same relation its Common Criteria name, representation correspondence, once the abstract and concrete levels are evaluation deliverables rather than TLA+ modules. An introduction to TLAPS TLAPS, the TLA+ Proof System, supports machine-checked deductive proofs: rather than enumerating a bounded state space, a TLAPS proof is a structured argument decomposed into steps, each discharged by a backend prover (Isabelle, Zenon, satisfiability modulo theories (SMT) solvers) or further decomposition. A TLAPS proof of an inductive invariant states initiation and consecution as above and proves each as a first-order argument valid for every parameter value, not merely a bounded instance. The trade-off: TLC is push-button automatic with an instant counterexample on failure, at the cost of bounded scope; TLAPS covers unbounded parameters but demands human proof-structuring effort. Mature practice uses both: TLC to explore cheaply and catch non-inductive invariants, TLAPS to promote a validated invariant into a proof holding for every instance size. This TLC/TLAPS split becomes a compliance question, not just an engineering one, once Evaluation Assurance Levels (EAL) enter the picture in module 05. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Formal methods at scale and in the pipeline. Decomposition and abstraction, deciding when to model-check and when to prove, and running checks in continuous integration.. Decompose a large model so it stays checkable.. Choose between model checking and deductive proof for a given property.. Explain how a specification check integrates into a continuous-integration step.. Decomposition and abstraction, Model-check or prove, Specifications in CI, Keeping specifications honest Formal methods at scale and in the pipeline A specification technique that only works on toy examples is not useful engineering practice. Real systems have state spaces no engineer can review by hand, so the discipline this course has built so far must survive contact with genuine scale. This lesson addresses whether formal methods scale: how to decompose a model so it stays checkable, how to choose between model checking and proof, how to run checks continuously, and how to keep specifications from drifting from the systems they describe. Each of the four questions maps onto one of this module's four sections, in order. Decomposition and abstraction State explosion and unbounded parameter spaces both push toward the same remedy: do not verify the whole system as one monolithic model. Decomposition splits a system into components, each verified against explicit assumptions about its environment (assume-guarantee reasoning): a component is checked assuming its neighbours meet their own specifications, and when composed, those mutual assumptions are discharged against each other's guarantees, so no single check faces the full product state space. Abstraction complements this by replacing fine-grained detail with a coarser model preserving the properties of interest, for instance abstracting an unbounded queue to 'empty, one element, or more than one', sometimes turning an infinite-state system into a finitely checkable one. Over-abstraction can introduce a spurious counterexample, a trail through the abstract model with no concrete counterpart, because the abstraction erased a distinction the property depended on; the standard response is counterexample-guided abstraction refinement: inspect the spurious trail, restore the erased distinction, and recheck. Model-check or prove The choice between TLC-style model checking and proof in the TLA+ Proof System (TLAPS), built on the Temporal Logic of Actions (TLA), is governed by the state space's shape. Model checking is push-button automatic and, on failure, produces an instant counterexample, but its scope is bounded to the configured instance, so it cannot certify a property for every parameter value. Deductive proof suits an unbounded or too-large state space, since discharged obligations hold for arbitrary sizes, at the cost of human effort structuring lemmas. Underlying both is a hard limit: Turing's proof (1936) that the halting problem is undecidable, generalised by Rice's theorem to state that every non-trivial semantic property of an arbitrary program is undecidable, means no algorithm decides every interesting property of every system. Specifications in CI A specification checked once at design time and never again decays: nothing enforces that it and the implementation still agree as code evolves. Running the TLA+ model checker (TLC) or the Simple Promela INterpreter (SPIN) in continuous integration (CI) keeps the model in step with the design, catching regressions automatically the moment a change breaks a previously-established property. This is straightforward wherever the checker runs headlessly and returns pass/fail with a machine-readable trace on failure. A specification check that only ever runs by hand, at the author's discretion, provides none of this protection, since nothing forces it to run before a regression ships. Keeping specifications honest Because a specification is a separate artefact from the code, the two can drift: a spec may still pass while the system's behaviour has changed, or still describe removed features. Dijkstra's dictum that testing shows only the presence, not absence, of bugs is why formal methods matter, but that value evaporates once the model no longer describes the real system: a proof about a stale model proves nothing about the deployed one. The disciplined response is to reconcile them, updating the specification (or the system) and re-running the checks, so the guarantees again describe what actually runs in production. Treating the specification as a living artefact, reviewed and updated alongside the code it describes, is what keeps its guarantees meaningful. The same discipline becomes a certification obligation once Evaluation Assurance Levels (EAL) require it, from module 05 onward. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Common Criteria foundations. The Target of Evaluation, the Security Target and Protection Profile, functional and assurance requirements, and the seven Evaluation Assurance Levels.. Define the TOE, ST and PP and how they relate.. Distinguish Security Functional Requirements from Security Assurance Requirements.. Assess and place the seven EALs on the assurance ladder and locate the European scheme (EUCC).. TOE, ST and PP, SFRs and SARs, The EAL ladder, The EUCC scheme Common Criteria foundations The Common Criteria for Information Technology Security Evaluation, standardised internationally by the International Electrotechnical Commission (IEC) jointly with ISO as ISO/IEC 15408, is the framework under which the mathematics of the preceding modules becomes evidence in a formal product evaluation. Everything proved with TLA+, built on the Temporal Logic of Actions (TLA), or checked with the Simple Promela INterpreter (SPIN) in earlier modules only counts here if it is expressed in this framework's own vocabulary. This lesson sets out its vocabulary: what is evaluated, what is claimed, what is required, and how rigour is graded. Modules 06 through 09 build directly on these four terms, so precise definitions now avoid confusion later. TOE, ST and PP The Target of Evaluation (TOE) is the specific product, or defined part of a product, together with its guidance documentation, actually subject to evaluation: a concrete artefact with a stated boundary, not a whole company or product line. A Security Target (ST) states the security problem, the security objectives, and the security requirements claimed for that one specific TOE: the contract against which the evaluation is conducted. A Protection Profile (PP) is a related but distinct document: an implementation-independent requirement set for a product class (a firewall PP, a smart-card PP), so multiple vendors' STs can claim conformance to the same PP and be compared on a common baseline. An ST may claim conformance to one or more PPs, inheriting their requirements while adding TOE-specific detail, and every evaluation is conducted against an ST, whether or not a PP stands behind it. SFRs and SARs The requirements catalogue splits into two kinds. Security Functional Requirements (SFRs) describe what the TOE must do: enforce access control, authenticate users, generate audit records; they are drawn from a standard catalogue (Part 2) so evaluations use comparable, precisely worded requirements rather than ad hoc prose. Security Assurance Requirements (SARs) describe how confidently the evaluator must be convinced the TOE meets its SFRs: they govern design-documentation depth, testing rigour, vulnerability-analysis extent, and, at the highest levels, the use of formal methods. An ST always selects both an SFR set (what is claimed) and a SAR package (how hard the claim is checked). The EAL ladder The Common Criteria defines seven Evaluation Assurance Levels (EAL), numbered Evaluation Assurance Level 1 (EAL1) through Evaluation Assurance Level 7 (EAL7), each a predefined SAR package of increasing depth and rigour. A higher EAL denotes greater depth and rigour of evaluation, not a guarantee of greater absolute security or more features: a poorly designed product evaluated at EAL7 is still poorly designed, the EAL states only how convincingly that has been checked. The formal-methods content of this course becomes mandatory only at the top: Evaluation Assurance Level 6 (EAL6) and above require increasingly formal representations of the TOE's design, and, as the next module details, a formal Security Policy Model at EAL7. That threshold, not the lower levels, is why this course exists: EAL6 and EAL7 are where mathematics stops being optional and becomes the evidence itself. The EUCC scheme The European Common Criteria-based cybersecurity certification scheme (EUCC) was adopted under the EU Cybersecurity Act (Regulation (EU) 2024/482) to give ISO/IEC 15408 legal standing and mutual recognition across the EU, superseding the older, non-binding Senior Officials Group (SOG) arrangement on Information Systems security (SOG-IS) among a subset of European nations. EUCC certificates are issued by national cybersecurity certification authorities and recognised across all member states, giving vendors one evaluation portable across the internal market. It is the scheme in which the assurance ladder, the Development assurance class (ADV), and the vulnerability-resistance requirements of later modules are currently operated in Europe, and the scheme the capstone's evidence package is framed against. Module 08 returns to EUCC specifically for vulnerability resistance, once the AVA_VAN family has been introduced. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) The ADV class and security policy models. The development assurance class, the formal Security Policy Model required at the top of the ladder, and the classical access-control models behind it.. Name the ADV families and what each documents.. State at which EALs a formal Security Policy Model (ADV_SPM) is required.. Express a small access-control policy as a formal model.. The ADV families, ADV_SPM at EAL6 and EAL7, Bell and LaPadula, Clark and Wilson The ADV class and security policy models Development (ADV) is the Common Criteria assurance class concerned with the design documentation of the Target of Evaluation (TOE): where the evaluator learns, at ever-increasing formality as the Evaluation Assurance Level (EAL) rises, exactly what the TOE is and how it works. This lesson surveys the ADV families, pinpoints where a formal model becomes mandatory, and introduces the two classical access-control models most often chosen to fill that role. Both models predate the Common Criteria itself, and both reappear later as worked examples of what a formal Security Policy Model actually looks like. The ADV families ADV is organised into families, each documenting a facet or abstraction level of the design. ADV_ARC documents the security architecture: how self-protection, non-bypassability and domain separation are achieved. ADV_FSP is the functional specification: the TOE's security-relevant external interfaces and their behaviour. ADV_TDS is the TOE design: decomposition into subsystems and modules realising the functional specification. ADV_IMP covers the implementation representation, effectively the source code, at the highest levels. ADV_INT addresses well-structured internals (modularity, layering, minimised complexity). ADV_SPM, the formal Security Policy Model, is this lesson's focus: a mathematical model of the security policy the TOE enforces, with a demonstrated correspondence to the functional specification. ADV_SPM at EAL6 and EAL7 A formal Security Policy Model is not required at every EAL; it becomes mandatory only at Evaluation Assurance Level 6 (EAL6), the level styled Semiformally Verified Design and Tested, and at Evaluation Assurance Level 7 (EAL7), styled Formally Verified Design and Tested, where the methodology demands increasingly rigorous representations of the design and its security policy. At EAL6 the ADV deliverables generally use semiformal notation (structured but not fully mathematical), while EAL7 requires fully formal representation of the security policy model and formal or semiformal proof of correspondence to the functional specification, precisely the toolkit of temporal logic, PROMELA and the Simple Promela INterpreter (SPIN), and the Temporal Logic of Actions (TLA) built earlier. At the highest levels, prose and diagrams are judged too imprecise, so the requirements themselves force formal methods, converting earlier techniques into a compliance obligation. Bell and LaPadula The Bell-LaPadula model (1973), developed for the US Department of Defense, is the archetypal confidentiality security policy model: it assigns security levels to subjects and objects and enforces simple security (no read up: no reading a higher classification) and the star property (no write down: no writing to a lower classification), preventing high-classification information flowing to low-classification subjects via reading or writes. It is a lattice-based mandatory access control model, expressed as a state machine with a precisely stated invariant, a natural fit for module 03's inductive-invariant techniques: initiation and consecution can be stated and discharged directly. Writing the no-read-up and no-write-down rules as a single state predicate is usually the first exercise in turning Bell-LaPadula into an ADV_SPM-style model. Clark and Wilson Where Bell-LaPadula targets confidentiality, the Clark-Wilson model (1987) targets integrity in commercial systems: data (constrained data items) may be manipulated only through well-formed transactions certified to preserve a valid state, and every transaction must be attributable to an authenticated, authorised user (separation of duty). Its certify-then-enforce structure mirrors the Common Criteria's own scheme-level structure: a security policy model is certified once (evaluated) and enforced continuously. Bell-LaPadula and Clark-Wilson together give two contrasting templates, confidentiality- and integrity-oriented, for the formal security policy model ADV_SPM requires. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) From model to evidence. Representation correspondence, semiformal versus formal representation, and the documentation the evaluation methodology actually checks.. Explain representation correspondence across the ADV deliverables.. Distinguish semiformal from formal representation.. Construct a mapping from a TLA+ or SPIN artefact onto evidence an evaluator accepts.. Representation correspondence, Semiformal versus formal, What the CEM checks, Packaging the evidence From model to evidence A proof about a model is only assurance evidence if an evaluator can see, and check, that the model actually describes the product. Every technique built in modules 00 through 04, and every model this course has checked, only becomes Common Criteria evidence once it clears the bar this module sets. This lesson addresses the connective tissue of a Common Criteria evaluation: representation correspondence between ADV deliverables, the semiformal-versus-formal distinction, and what the evaluation methodology concretely inspects. Each of the three sections below answers one of those three questions in turn. Representation correspondence The Development (ADV) deliverables form a chain of decreasing abstraction: the Security Policy Model (ADV_SPM), the functional specification (ADV_FSP), the design of the Target of Evaluation (TOE), formally ADV_TDS, and, at the highest levels, the implementation representation (ADV_IMP). Representation correspondence is the requirement, and evaluator activity, of demonstrating each representation is a faithful refinement of the one above: every security-relevant behaviour in the functional specification is accounted for by the security policy model, the TOE design realises the functional specification, and so on down to the implementation. This is the Common Criteria's own name for module 03's refinement relation: a lower-abstraction specification implementing another, with no behaviour appearing below that is not sanctioned above. Without demonstrated correspondence, an elegant proof about an abstract policy model says nothing about whether the shipped specification, let alone the implementation, honours it. Semiformal versus formal The Common Criteria distinguishes informal (unrestricted natural language), semiformal (a restricted, defined notation, such as structured pseudocode, finite-state diagrams with fixed interpretation, or the Unified Modeling Language (UML) with specified semantics, reducing ambiguity without full mathematical rigour), and formal (a notation with well-defined mathematical syntax and semantics, such as TLA+, built on the Temporal Logic of Actions (TLA), PROMELA, linear temporal logic (LTL), or Z) representation. Which level is required, and for which deliverable, is fixed by the target Evaluation Assurance Level (EAL): Evaluation Assurance Level 6 (EAL6) generally requires the TOE design and architecture to be at least semiformal, while Evaluation Assurance Level 7 (EAL7) requires the security policy model itself, and its correspondence demonstration, to be formal. The distinction is not stylistic: a semiformal diagram can still hide ambiguity a reader resolves unconsciously, whereas a formal representation, by construction, has no such gaps. What the CEM checks The Common Evaluation Methodology (CEM) accompanies the standard, translating each Security Assurance Requirement (SAR) into concrete evaluator work units: specific, auditable actions to perform and document. For ADV_SPM, the CEM does not simply ask whether a model exists; it directs the evaluator to check the model is internally consistent, actually covers the security policy claimed in the Security Target (ST), that the correspondence to the functional specification is complete and accurate (every behaviour traceable both ways), and that any proof or model-checking result genuinely establishes what it claims, at the rigour the EAL demands. A TLA+ specification or SPIN run, however elegant, is not itself the evidence: the evidence is the documented package showing the model, its checked properties, and its traced correspondence, exactly what the CEM's work units audit. An evaluator reading that package should be able to reconstruct why the check is trustworthy without re-running it. Packaging the evidence Turning formal-methods artefacts into evidence means assembling, for each ADV deliverable, the model itself, the properties checked (with results, the TLA+ model checker (TLC) configuration, or TLA+ Proof System (TLAPS) proof scripts), and an explicit correspondence argument connecting it to the deliverables above and below. A TLA+ invariant proof becomes evidence for ADV_SPM only alongside a stated correspondence to ADV_FSP's security behaviours; a Simple Promela INterpreter (SPIN) verification becomes evidence only when the modelled protocol is shown to be the one the TOE design implements. Packaging is as much traceability discipline as mathematics, exactly the skill the capstone exercises: a small but complete package an evaluator could actually assess. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Resistance, schemes and composition. Vulnerability analysis and attack potential, the EUCC scheme, assurance continuity and composition, and the honest gap between a proof and the running system.. Explain AVA_VAN and how attack potential sets the bar.. Summarise what the EUCC scheme changed relative to SOG-IS.. Reason about the limit of a proof about a model versus the deployed system.. Vulnerability analysis (AVA_VAN), The EUCC scheme, Assurance continuity and composition, The model-to-implementation gap Resistance, schemes and composition A correctness proof establishes that a model has no flaws of the kind it was designed to check for; it says nothing directly about an attacker's ingenuity, about certifying products built from other certified products, or about the deployed system versus the model. This lesson closes the gap between formal assurance and real-world resistance, and states honestly where formal methods stop. Everything proved so far in this course describes a model; this module is about what that leaves out. Vulnerability analysis (AVA_VAN) AVA_VAN (Vulnerability Analysis) is the assurance family concerned with whether the Target of Evaluation (TOE), as built, resists penetration attacks, independent of whatever correctness has been established for its design. The evaluator, or an independent penetration tester, searches for exploitable vulnerabilities and, where one is found, rates the attack potential required to exploit it: elapsed time, specialist expertise, knowledge of the TOE, window of opportunity, and equipment needed. Each AVA_VAN level (AVA_VAN.1 through AVA_VAN.5) sets a bar of attack potential the TOE must resist, from basic opportunistic attack up to a highly skilled, well-resourced adversary at AVA_VAN.5, typically demanded at Evaluation Assurance Level 6 (EAL6) and Evaluation Assurance Level 7 (EAL7). This is a deliberately adversarial complement to the Development (ADV) class's deductive and model-checked evidence: a verified security policy model can still sit atop an implementation with an exploitable buffer overflow the model never represented, and AVA_VAN is aimed at finding that class of gap. The EUCC scheme The European Common Criteria-based cybersecurity certification scheme (EUCC), established under the EU Cybersecurity Act (Regulation (EU) 2024/482), gives the Common Criteria legal standing and mutual recognition across the EU, superseding the earlier Senior Officials Group (SOG) arrangement on Information Systems security (SOG-IS) among a subset of European states. For vulnerability resistance specifically, it formalises attack-potential rating and AVA_VAN-style penetration testing within an EU-wide governance structure, with certificates issued by national authorities and overseen for consistency by ENISA, so an AVA_VAN rating earned in one member state carries the same meaning across the internal market. That EU-wide consistency is precisely what the earlier SOG-IS mutual-recognition arrangement lacked. Assurance continuity and composition Real products are rarely evaluated as a monolith; they are often built by composing an already-certified platform (a smart-card chip, an Operating System (OS) kernel) with additional software, and updated after certification. Composition allows the certification of the composed product to reuse the platform's certified evidence rather than re-evaluating from scratch, provided the composition is analysed for new vulnerabilities at the interface. Assurance continuity addresses change after certification: rather than a full re-evaluation for every patch, a maintenance process assesses whether a change is minor enough to preserve the certificate or substantial enough to require fresh evaluation, particularly fresh AVA_VAN analysis if security-relevant code changed. Both mechanisms mirror module 04's decomposition: verify components and changes against explicit, bounded assumptions rather than re-verifying everything. The model-to-implementation gap This module closes by naming precisely what a formal proof does and does not establish. A TLA+ (built on the Temporal Logic of Actions (TLA)) or Simple Promela INterpreter (SPIN) proof establishes properties of a model, an abstraction at a level of detail the specifier judged sufficient. It says nothing directly about a compiler bug, a hardware fault, a side-channel leak, or any detail abstracted away in modelling; representation correspondence and AVA_VAN's independent testing exist because these gaps are real. Honest formal-methods practice states the model's scope explicitly, argues correspondence as rigorously as the Evaluation Assurance Level (EAL) demands, and relies on non-formal evidence to cover what the model does not: that is the difference between a rigorous evaluation and a false sense of security purchased with an impressive-looking proof. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/) Capstone: specify, check, and evidence a small TOE. Specify a small Target of Evaluation, model-check its key security properties, and assemble an ADV_SPM-style evidence package graded against evaluator criteria.. Define and produce a small but well-formed Security Target.. Model-check the security properties the ST claims.. Assemble and defend an ADV_SPM-style evidence package.. Scoping the TOE, Specifying and checking, Building the evidence package, Defending the analysis Capstone: specify, check, and evidence a small TOE The capstone asks you to run the whole pipeline this course has built, end to end, on a small but genuine example: scope a Target of Evaluation (TOE), specify and check its key security properties formally, and assemble the resulting artefacts into an ADV_SPM-style evidence package that could actually withstand an evaluator's scrutiny under the Common Evaluation Methodology (CEM). Every module before this one supplied one piece of that pipeline: temporal logic and invariants from module 00, model checking from modules 01 and 03, TLA+ and proof from modules 02 and 03, Common Criteria vocabulary from modules 05 through 08, including the Evaluation Assurance Levels (EAL) that set how much of this the evaluation methodology requires. This module asks you to run all of them together, once, on one small system. Scoping the TOE Every real evaluation begins by drawing a boundary: deciding exactly what the TOE is, what is inside it and what is assumed about its environment, and what security problem it is meant to solve. Scope deliberately small: a single access-control mechanism, a small authentication protocol, or a minimal mutual-exclusion service is large enough to carry a genuine security policy and small enough to specify and check exhaustively. State the TOE boundary explicitly, the environmental assumptions, and the specific security properties (a Security Functional Requirement (SFR)-like statement) the Security Target (ST) would claim; covering too much produces a model too large to check and a package too diffuse to defend. A boundary drawn too generously is the single most common reason a first attempt at this exercise stalls. Specifying and checking With the TOE scoped, produce a formal model, in TLA+ (built on the Temporal Logic of Actions (TLA)), PROMELA, or both, capturing its state machine and security-relevant next-state relation: who can perform which action, under what guard, and what state results. State the properties as invariants (safety) and, where relevant, temporal liveness properties, and check them: with the TLA+ model checker (TLC) against the TLA+ specification, or the Simple Promela INterpreter (SPIN) against a PROMELA model and its never claims. Where an invariant is not initially inductive, strengthen it and recheck; where the state space is too large, decompose or abstract it, and be explicit about the choice made. The output is not just 'checks pass': it is the model, the exact properties checked, and, for any invariant central to the argument, a demonstration that it is inductive. Building the evidence package A proof is not evidence until packaged with a stated correspondence to the deliverable above and below it. This means producing an ADV_SPM-style package: the formal or semiformal security policy model itself; a statement of which classical access-control pattern, if any, it resembles (Bell-LaPadula or Clark-Wilson); the model-checking or proof results as an evaluator's evidence trail would show them; and a correspondence argument mapping the model's states and actions onto a sketched functional specification of the TOE's external interface. Treat this as the CEM would: the evaluator's work units check consistency, coverage of the claimed policy, and completeness of correspondence, so the package should make all three checkable, not merely assert them. A package that only asserts completeness, without showing the trace that establishes it, would not survive a real evaluator's review. Defending the analysis The capstone closes with an honest statement of scope and limitation: what the model represents, what it deliberately abstracts away, and what an AVA_VAN-style analysis or implementation review would still need to examine that the model cannot speak to (timing channels, the actual code, deployment configuration). A strong defence names the model-to-implementation gap explicitly rather than overselling the proof, states which properties were established by exhaustive model checking (bounded scope, concrete counterexamples if found and fixed) versus deductive argument (broader scope, dependent on stated lemmas), and shows, in miniature, the discipline a real evaluation at Evaluation Assurance Level 6 (EAL6) or Evaluation Assurance Level 7 (EAL7) requires: a formal model, checked properties, a traced correspondence, and an honest account of what remains outside the model's reach. Related CCI capabilities Mirage: See what matters. Touch nothing. Safety-in-the-Middle mediation. (https://www.cambridgecyberinternational.com/en/roadmap/). Common Criteria EAL Certification Support: (https://www.cambridgecyberinternational.com/en/services/). Safety-in-the-Middle Mediation (Concept): You can never really touch what you see. (https://www.cambridgecyberinternational.com/en/roadmap/)