Skip to content
Nenkin
Sign inStart free trial

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.

Explore NenkinTracker to find certified products and compare their assurance levels, including EAL6.

Key facts

  • Assurance families covered: over EAL5, EAL6 promotes ADV_IMP.1 to ADV_IMP.2 (complete mapping of the implementation representation), ADV_INT.2 to ADV_INT.3 (minimally complex internals), ADV_TDS.4 to ADV_TDS.5 (complete semiformal modular design), ALC_CMC.4 to ALC_CMC.5 (advanced support), ALC_DVS.1 to ALC_DVS.2 (sufficiency of security measures), ALC_TAT.2 to ALC_TAT.3 (compliance with implementation standards, all parts), ATE_COV.2 to ATE_COV.3 (rigorous analysis of coverage), ATE_FUN.1 to ATE_FUN.2 (ordered functional testing), and AVA_VAN.4 to AVA_VAN.5 (advanced methodical vulnerability analysis). It also introduces ADV_SPM.1 (formal TOE security policy model). ATE_DPT.3 is unchanged from 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.

Frequently asked questions

What is EAL6?
EAL6 is a Common Criteria assurance level reserved for products that protect very high-value assets. It requires semiformal verification that the design correctly implements the security policy model (ADV_SPM.1), layered TOE internals (ADV_INT.3), strengthened life-cycle controls (ALC_CMC.5, ALC_DVS.2, ALC_TAT.3), and AVA_VAN.5 vulnerability analysis at High attack potential. Cost and timeline are very high.
Why is EAL6 rarely used?
EAL6 demands a formal security policy model, semiformal verification of design correspondence, layered internals, and a hardened development environment. Most high-assurance smart card and HSM products achieve their target attack resistance via EAL5 augmented with AVA_VAN.5 (EAL5+) at lower cost than base EAL6. The increment to EAL6 is substantial and is usually only chosen when a scheme, regulator, or customer explicitly demands it.
What product categories use EAL6?
EAL6 certifications are concentrated in top-tier smart card ICs and smart card operating systems targeting the highest assurance segment, where SOG-IS and now EUCC recognition at the High level requires this rigour. A small number of high-assurance separation kernels, defense components, and embedded trust anchors also reach EAL6. It is essentially absent from general-purpose IT, networking, and enterprise software.
What is the difference between EAL6 and EAL5+/AVA_VAN.5?
Both reach High attack potential via AVA_VAN.5, so the attacker model is the same. The difference is in design assurance: EAL6 adds a formal security policy model (ADV_SPM.1), semiformal verification of correspondence between design and policy, layered internals (ADV_INT.3 versus ADV_INT.2), and stronger development security controls (ALC_DVS.2). EAL6 demands deeper structural evidence; EAL5+ achieves equivalent attack resistance with less design ceremony.
How does EAL6 differ from EAL7?
EAL7 replaces semiformal artifacts with formal ones across the functional specification (ADV_FSP.6), TOE design (ADV_TDS.6), and correspondence between them. The step is from structured precise notation to full mathematical verification. Testing also reaches the implementation representation (ATE_DPT.4 versus ATE_DPT.3 at EAL6). Vulnerability analysis stays at AVA_VAN.5 in both, so the change is about proof, not attacker model.
Does EAL6 require formal verification?
Partially. EAL6 introduces a formal security policy model (ADV_SPM.1) and requires semiformal verification of correspondence between the design and that model. The design itself is documented semiformally, not formally; machine-checkable mathematical proofs of design correctness are an EAL7 requirement. EAL6 sits in the gap between semiformal-only EAL5 and the full formal-methods regime of EAL7.
  • EAL1: Functionally TestedEAL1 is the lowest Common Criteria assurance level: independent confirmation that a product behaves as documented. Suitable when threats are low and trust in the vendor is adequate.
  • EAL2: Structurally TestedEAL2 is the workhorse Common Criteria assurance level: a high-level design review with independent vulnerability analysis, and the CCRA mutual-recognition cap for non-cPP evaluations.
  • EAL3: Methodically Tested and CheckedEAL3 extends EAL2 with development environment security controls, systematic life-cycle definition, and deeper test coverage. Less common than EAL2 or EAL4 in practice.
  • EAL4: Methodically Designed, Tested, and ReviewedEAL4 is the highest assurance level generally achievable on commercial products without re-engineering for assurance. Standard for smart cards, HSMs, and many government-used products.