Assurance Levels and Assurance Practices
Assurance levels, or more formally an Evaluation Assurance Level (EAL), represents a numerical grade assigned by a lab certified by the National Information Assurance Partnership (NIAP) to a product or system following the completion of a Common Criteria security evaluation in accordance with ISO/IEC 15408, the International Common Criteria. The Common Criteria establishes the following seven assurance levels: EAL 1 – Functionally Tested; EAL 2 – Structurally Tested; EAL 3 – Methodically Tested and Checked; EAL 4 – Methodically Designed , Tested and Reviewed; EAL 5 – Semi-formally Designed and Tested; EAL 6 – Semi-formally Verified Design and Tested; and EAL 7 – Formally Verified Design and Tested.
Assurance practices fall within two general areas: argumentation and computation.
Argumentation, based on Stephen Toulmin’s Uses of Argument [T 1958], is a body of evidence that a claim is sound. Assurance cases, alternatively called dependability or safety cases, like use cases, provide textual and graphical evidence supporting a claim given grounds, warrants, backing, qualifiers and rebuttals. What constitutes evidence in assurance cases is not standardized [AK 2009] leading some to consider the evidence available from argumentation less conclusive than computation. Assurance cases have the advantage that most if not all team members can understand, evaluate and share the evidence. Conversely, the definitions of EAL 5, 6 & 7 contain the terms “formal” and “verified.” Formal and verified imply automated or semi-automated independent proof that a program implements the properties in the specification according to which it is designed. Even where Goal Structuring Notation and the Structured Assurance Case Metamodel are used we would expect an approach based exclusively in argumentation not to satisfy the formal and verified requirements of EAL 7.
Computation implies the execution of computer instructions verified according to the laws of math and logic. Verification of a type safe program requires that it exhibit two properties: progress and preservation. [P 2002] Progress is defined according to the following rule: “A well-typed term is not stuck (either it is a value or it can take a step according to the evaluation rules).” And preservation as: “If a well-typed term takes a step of evaluation, then the resulting term is also well typed.” The type checker enforces progress and preservation along with the detailed evaluation rules. Think something much more than a spell checker. The evaluation rules are derived from well-known elements of math and logic. Well-typed programs don’t get stuck because they don’t get compiled.
An informal analysis of emerging capabilities in the DARPA OpenCatalog indicates that type safety is a common requirement for increased assurance levels. Increasing assurance levels through type safety allows for achieving the highest evaluation assurance level, EAL 7, because a type safe approach to assurance is computational. The section below on type safety and software verification describes type checking at compile-time as an example of early verification. Common requirements associated with emerging capabilities are especially relevant to planning and architecture. To introduce type safety early we need a life cycle to frame type safety within the sequencing of activities.