EAL7 — Formally Verified Design and Tested

EAL7 is the highest assurance level defined by Common Criteria (ISO/IEC 15408-3). It requires formal mathematical verification that the TOE design implements the security policy, and applies only to TOEs that are small and simple enough for such proof to be feasible.

See the list of certified products at EAL7 tracked in NenkinTracker.

Key facts

  • Assurance families covered: adds ADV_FSP.6 (formal functional specification), ADV_TDS.6 (formal TOE design), ADV_SPM.1 (formal security policy model), ADV_INT.3, ATE_DPT.4 (testing: implementation representation), AVA_VAN.5 over EAL6.
  • Typical product categories: small, security-critical components such as cryptographic kernels, separation kernels, and very focused embedded trust anchors.
  • Relative cost/time: extreme; formal methods work is measured in years of specialist effort.
  • Attack potential resisted: High.

What this level tests

Evaluators check a formal functional specification (ADV_FSP.6), a formal TOE design (ADV_TDS.6), and a formal security policy model (ADV_SPM.1), together with formal correspondence between them. Testing reaches the implementation representation (ATE_DPT.4). Vulnerability analysis remains at AVA_VAN.5 with High attack potential.

Because EAL7 assurance depends on complete formal verification, TOE scope is deliberately minimized. A typical EAL7 TOE covers a small, well-defined module — not an entire product family.

Typical product categories

EAL7 evaluations are very rare. They appear for small, formally tractable components such as separation kernels and focused cryptographic TOEs. Vendors usually ship a larger product in which an EAL7 TOE is embedded; the certificate applies to the TOE boundary, not the whole system.

Common misconceptions

EAL is an assurance level, not a security-strength rating. EAL7 means the TOE has been formally proven to implement a specific security policy under the assumptions of the Security Target. It does not mean the product is “unbreakable” — it means that, within the Security Target’s scope and assumptions, the design has been mathematically verified to implement the modeled policy. Flaws in the model, or outside the TOE boundary, are not covered.

Very few products reach EAL7. The overwhelming majority of high-assurance commercial certifications stop at EAL5+/VAN.5 or EAL6. EAL7 is specialized and often tied to defense, aerospace, or critical infrastructure programmes that mandate formal methods.

Comparison to adjacent levels

  • vs. EAL6: EAL7 replaces semiformal artifacts with formal ones across the functional specification, TOE design, and correspondence — the substantive leap is full mathematical verification.
  • vs. EAL beyond 7: CC defines no level above EAL7. Assurance higher than EAL7 is not expressible in the standard.

See the EAL Levels overview and the glossary for SAR vocabulary.