Existing assurance standards: FIPS 140 and CC

A small niche of computer systems need high assurance of correctness. A system may in fact be free of bugs, but if it is not known whether it is, then any risk analysis must make a worst case assumption that bugs may be present. Assurance has a role in evaluating the risk associated with deploying systems. Risks can be social (voting machines, data protection), life threatening (automobile software, medical equipment) or commercial (secure digital rights management, financial processing).

There are various standards offering a spectrum of degrees of assurance, with the highest levels requiring formal methods. For example, Level 4 assurance is described in Section 4.10.3 of the FIPS 140-2 as follows:

• Documentation shall specify a formal model that describes the rules and characteristics of the cryptographic module security policy. The formal model shall be specified using a formal specification language that is a rigorous notation based on established mathematics, such as first order logic or set theory.

• Documentation shall specify a rationale that demonstrates the consistency and completeness of the formal model with respect to the cryptographic module security policy.

• Documentation shall specify an informal proof of the correspondence between the formal model and the functional specification.

• For each cryptographic module hardware, software, and firmware component, the source code shall be annotated with comments that specify (1) the preconditions required upon entry into the module component, function, or procedure in order to execute correctly and (2) the postconditions expected to be true when execution of the module component, function, or procedure is complete. The preconditions and postconditions may be specified using any notation that is sufficiently detailed to completely and unambiguously explain the behavior of the cryptographic module component, function, or procedure.

• Documentation shall specify an informal proof of the correspondence between the design of the cryptographic module (as reflected by the precondition and postcondition annotations) and the functional specification.

A standard that is more general than FIPS 140, because it applied to all security IT products not just encryption, is the Common Criteria (CC), whose highest level is Evaluation Assurance Level 7 (EAL7). This is somewhat weaker than FIPS level 4, but does require some formal analysis of the Target of Evaluation (TOE). Section 5.9 of Part 3: Security Assurance Requirements (v2.2) of the Common Criteria requirements says:

Evaluation assurance level 7 (EAL7) - formally verified design and tested

Objectives

EAL7 is applicable to the development of security TOEs for application in extremely high risk situations and/or where the high value of the assets justifies the higher costs. Practical application of EAL7 is currently limited to TOEs with tightly focused security functionality that is amenable to extensive formal analysis.

Assurance components

EAL7 provides assurance by an analysis of the security functions, using a functional and complete interface specification, guidance documentation, the high-level and low-level design of the TOE, and a structured presentation of the implementation, to understand the security behaviour. Assurance is additionally gained through a formal model of the TOE security policy, a formal presentation of the functional specification and high-level design, a semiformal presentation of the low-level design, and formal and semiformal demonstration of correspondence between them, as appropriate. A modular, layered and simple TOE design is also required.

The analysis is supported by independent testing of the TOE security functions, evidence of developer testing based on the functional specification high-level design, low-level design and implementation representation, complete independent confirmation of the developer test results, strength of function analysis, evidence of a developer search for vulnerabilities, and an independent vulnerability analysis demonstrating resistance to penetration attackers with a high attack potential. The analysis also includes validation of the developer's systematic covert channel analysis.

EAL7 also provides assurance through the use of a structured development process, development environment controls, and comprehensive TOE configuration management including complete automation, and evidence of secure delivery procedures.

This EAL represents a meaningful increase in assurance from EAL6 by requiring more comprehensive analysis using formal representations and formal correspondence, and comprehensive testing.

Assurance standards like FIPS 140 and CC are sometimes criticised for delivering results that are misleading. A vendor may procure an evaluator who will give an easy ride, and the organisation that licenses the evaluator may be reluctant to punish abuse in case that brings the whole evaluation system into disrepute. There is a good discussion in Chapter 23 of the textbook Security Engineering by Ross Anderson.