Objectives
The correspondence between the various TSF representations (i.e. TOE summary specification, functional specification, high-level design, low-level design, implementation representation) addresses the correct and complete instantiation of the requirements to the least abstract TSF representation provided. This conclusion is achieved by step-wise refinement and the cumulative results of correspondence determinations between all adjacent abstractions of representation.
Component levelling
The components in this family are levelled on the basis of the required level of formality of the correspondence between the various TSF representations.
Application notes
The developer must demonstrate to the evaluator that the most detailed, or least abstract, TSF representation provided is an accurate, consistent, and complete instantiation of the functions expressed as functional requirements in the ST. This is accomplished by showing correspondence between adjacent representations at a commensurate level of rigour.
This family of requirements is not intended to address correspondence relating to the TSP model or the TSP. Rather, as shown in Figure 10.2, it is intended to address correspondence between various TSF representations (i.e. the TOE summary specification, functional specification, high-level design, low-level design, and implementation representation) that are provided.
The ADV_RCR.*.1C elements refer to "all relevant security functionality" in defining the scope of what must be refined between an adjacent pair of TSF representations. For the refinements between the TOE summary specification and the functional specification, this element requires only that the TOE security functions in the TOE summary specification be refined in the functional specification, and does not require that the functional specification contain any details regarding assurance measures (which are presented in the TOE summary specification). Where the implementation representation is only provided for a subset of the TSF (as in ADV_IMP.1), the required refinements between the low-level design and the implementation representation are limited to the security functionality that is presented in the implementation representation. In all other cases, this element requires that all parts of the more abstract TSF representation be refined in the less abstract TSF representation.
In the context of the level of formality for correspondence between adjacent TSF representations, informal, semiformal and formal are considered to be hierarchical in nature. Thus, ADV_RCR.2.2C and ADV_RCR.3.2C may be met with a formal proof of correspondence, and in the absence of any requirements on its level of formality, a demonstration of correspondence may be informal, semiformal or formal.