EAL6 — Semiformally Verified Design and Tested

EAL6 is a Common Criteria assurance level reserved for products protecting very high-value assets. It requires semiformal verification that the design correctly implements the Security Target, layered internal structure, and vulnerability analysis at High attack potential.

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

Key facts

  • Assurance families covered: adds ADV_INT.3 (layered TOE internals), ADV_SPM.1 (formal security policy model), ALC_CMC.5, ALC_DVS.2 (sufficient development security), ALC_TAT.3, ATE_DPT.3, AVA_VAN.5 over EAL5.
  • Typical product categories: top-tier smart card ICs and operating systems, selected high-assurance separation kernels, defense and national-security components.
  • Relative cost/time: very high; requires formal security policy modelling, semiformal design verification, and hardened development processes.
  • Attack potential resisted: High.

What this level tests

Evaluators verify semiformal correspondence between the design and the security policy model, and check that the TOE internals are layered in a way that supports minimization of the trusted computing base (ADV_INT.3). ALC_DVS.2 demands evidence that development security measures are sufficient, not merely present. AVA_VAN.5 analyzes for High-potential attackers with expert knowledge, specialized equipment, and extended time.

Typical product categories

EAL6 certifications are concentrated in smart card ICs and smart card operating systems targeting the highest-assurance market segments, where SOG-IS and now EUCC recognition at the ‘high’ level requires this rigor. Beyond smart cards, EAL6 appears in a small number of high-assurance separation kernels and similar embedded trust anchors.

Common misconceptions

EAL is an assurance level, not a security-strength rating. EAL6 means the evaluator has very high confidence that the TOE implements its Security Target correctly under High-potential attack. It does not mean the product is secure against threats outside that Security Target, nor that its operational environment can be ignored. Deployment still matters.

EAL6 is not required just because “EAL5+/VAN.5” looks similar. Many smart card certifications are issued at EAL5 augmented with AVA_VAN.5 (EAL5+), not EAL6. The increment from EAL5+/VAN.5 to EAL6 is substantial and is usually only chosen when the scheme or customer explicitly demands it.

Comparison to adjacent levels

  • vs. EAL5: EAL6 adds a formal security policy model, layered internals (ADV_INT.3), stronger life-cycle controls (ALC_CMC.5, ALC_DVS.2, ALC_TAT.3), and raises vulnerability analysis to AVA_VAN.5.
  • vs. EAL7: EAL7 requires formally verified design, a formal TOE design notation (ADV_TDS.6), and formal correspondence to the security policy model — the step into full mathematical verification.

See the EAL Levels overview and the glossary.