Skip to content
Nenkin
Sign inStart free trial

EAL5: Semiformally Designed and Tested

EAL5 is a Common Criteria assurance level for products designed with assurance in mind from the outset. It introduces semiformal design notation, raises the test depth to the modular design, and mandates covert channel analysis for TOEs enforcing information-flow policies.

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

Key facts

  • Assurance families covered: adds ADV_FSP.5 (complete semi-formal functional specification with additional error information), ADV_INT.2 (well-structured internals), ADV_TDS.4 (semiformal modular design), ALC_CMS.5 (development tools CM coverage), ALC_TAT.2 (compliance with implementation standards), ATE_DPT.3 (testing: modular design), and AVA_VAN.4 (methodical vulnerability analysis at Moderate) over EAL4. ADV_IMP.1, ALC_CMC.4, ALC_DVS.1, and ALC_LCD.1 carry over from EAL4. ADV_IMP.2 (complete mapping) is an EAL6 increment, not an EAL5 one.
  • Typical product categories: smart card integrated circuits, smart card operating systems, high-assurance separation kernels, certain hypervisors.
  • Relative cost/time: high; requires assurance-oriented design, semiformal specifications, and extensive documentation beyond commercial engineering norms.
  • Attack potential resisted: Moderate (EAL5 baseline); High when augmented with AVA_VAN.5 (EAL5+).

What this level tests

Evaluators review a subset of the implementation representation (ADV_IMP.1, the same component that applies at EAL4); the step to complete mapping (ADV_IMP.2) does not occur until EAL6. The functional specification and TOE design must be presented in semiformal notation (ADV_FSP.5, ADV_TDS.4), with internal structure shown to be well-structured (ADV_INT.2). Testing depth reaches the modular description (ATE_DPT.3). AVA_VAN.4 raises vulnerability analysis to Moderate attack potential.

Covert channel analysis becomes relevant at EAL5 for TOEs that enforce information-flow policies, since evaluators expect the developer to identify and assess channels that could bypass the stated flow controls.

Typical product categories

EAL5 is strongly concentrated in smart card ICs and associated operating systems, where certification ecosystems under SOG-IS (and now EUCC) historically demanded high assurance combined with High attack potential (EAL5+ with AVA_VAN.5). High-assurance separation kernels used in defense and aerospace are another category where EAL5 or EAL5+ evaluations appear.

Common misconceptions

EAL is an assurance level, not a security-strength rating. EAL5 means the TOE was designed and documented in a way that makes deeper evaluator review tractable. It does not mean EAL5 products are invulnerable. Even at EAL5+/AVA_VAN.5, the evaluator analyzes against High attack potential, not unlimited resources.

“Semiformal” is not the same as formal. EAL5 requires a semiformal notation: structured and precise but not necessarily mathematically provable. Only EAL6 and EAL7 introduce formal verification components.

Comparison to adjacent levels

  • vs. EAL4: EAL5 adds semiformal functional specification (ADV_FSP.5), semiformal modular design (ADV_TDS.4), well-structured internals (ADV_INT.2), broader CM coverage (ALC_CMS.5), tighter implementation-standards compliance (ALC_TAT.2), and AVA_VAN.4 at Moderate attack potential. ADV_IMP.1 is unchanged.
  • vs. EAL6: EAL6 promotes implementation-representation review to ADV_IMP.2 (complete mapping), adds a formal security policy model (ADV_SPM.1), layered internals (ADV_INT.3), AVA_VAN.5 at High attack potential, and stronger development-environment controls (ALC_DVS.2, ALC_CMC.5, ALC_TAT.3).

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

Frequently asked questions

What is EAL5?
EAL5 is a Common Criteria assurance level for products designed with assurance in mind from the outset. It requires a semiformal functional specification (ADV_FSP.5), semiformal modular design (ADV_TDS.4), well-structured internals (ADV_INT.2), modular-design test depth (ATE_DPT.3), and AVA_VAN.4 vulnerability analysis at Moderate attack potential. Implementation-representation review stays at ADV_IMP.1 (the same component used at EAL4); the step to complete mapping (ADV_IMP.2) does not occur until EAL6. Covert channel analysis is expected for TOEs that enforce information-flow policies.
What does semiformal design mean at EAL5?
Semiformal means the design is expressed in a structured and precise notation, typically with defined syntax and restricted vocabulary, but not in a fully mathematical or machine-checkable form. It sits between informal narrative (used at lower EALs) and formal specification (introduced at EAL6 and required throughout EAL7). The aim is precise, unambiguous design documentation that supports systematic evaluator analysis without requiring mathematical proof.
What product categories typically target EAL5?
EAL5 is heavily concentrated in smart card integrated circuits and smart card operating systems, where certification ecosystems under SOG-IS and now EUCC historically demanded high assurance combined with High attack potential (EAL5+ with AVA_VAN.5). High-assurance separation kernels used in defense and aerospace are another category where EAL5 or EAL5+ evaluations appear. Few general-purpose commercial products reach this level.
What is the difference between EAL5 and EAL5+?
Base EAL5 includes AVA_VAN.4 vulnerability analysis at Moderate attack potential. EAL5+ is shorthand for EAL5 augmented with one or more specific components, most often AVA_VAN.5, which raises the attacker model to High potential (expert knowledge, specialized equipment, extended time). For smart card ICs in European markets, EAL5+ AVA_VAN.5 is common because the deployment threat model assumes well-resourced physical attackers.
How does EAL5 differ from EAL4?
EAL4 reviews a subset of the implementation representation (ADV_IMP.1) and uses AVA_VAN.3 at Enhanced-Basic attack potential. EAL5 keeps ADV_IMP.1, upgrades the functional specification to semiformal (ADV_FSP.5), upgrades design documentation to semiformal modular (ADV_TDS.4), adds well-structured internals (ADV_INT.2), expands CM coverage to development tools (ALC_CMS.5), tightens implementation- standards compliance (ALC_TAT.2), increases test depth to the modular description (ATE_DPT.3), and raises vulnerability analysis to AVA_VAN.4 at Moderate attack potential. The step to complete implementation-representation mapping (ADV_IMP.2) is an EAL6 increment, not an EAL5 one.
Why are smart cards typically evaluated at EAL5+?
Smart card ICs and operating systems face well-resourced physical attackers (side-channel analysis, fault injection, microprobing) that require High attack potential resistance. EAL5's semiformal design, well-structured internals, and modular-design test depth give evaluators the visibility needed to assess such attacks systematically, and AVA_VAN.5 augmentation supplies the matching attacker model. SOG-IS legacy and EUCC High-level recognition both reflect this historical tooling.
  • 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.