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, requires full implementation representation in the evaluation evidence, and mandates covert channel analysis.

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

Key facts

  • Assurance families covered: adds ADV_IMP.2 (complete implementation representation), ADV_INT.2 (well-structured internals), ADV_TDS.4 (semiformal design), ALC_CMC.4, ALC_CMS.5, ALC_DVS.1, ALC_LCD.1, ALC_TAT.2, ATE_DPT.3, AVA_VAN.4 over EAL4.
  • 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 examine the complete implementation representation (ADV_IMP.2) rather than a subset. Design must be presented in a semiformal notation, 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” ≠ 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 design, full implementation representation, structured internals (ADV_INT.2), and raises vulnerability analysis to AVA_VAN.4.
  • vs. EAL6: EAL6 requires semiformal verification of design correspondence, layered internals (ADV_INT.3), AVA_VAN.5 High attack potential by default, and stronger development-environment controls.

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