Раздел: Документация
0 ... 40 41 42 43 44 45 46 ... 73 10.6 Representation correspondence (ADV RCR) 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 ADVIMP.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, ADVRCR.2.2C and ADVRCR.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. ADV RCR.1 Informal correspondence demonstration Dependencies: No dependencies. adv rcr.1.1d The developer shall provide an analysis of correspondence between all adjacent pairs of TSF representations that are provided. Content and presentation of evidence elements: adv rcr.1.1c For each adjacent pair of provided TSF representations, the analysis shall demonstrate that all relevant security functionality of the more abstract TSF representation is correctly and completely refined in the less abstract TSF representation. Evaluator action elements: adv rcr.1.1e The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence. ADV RCR.2 Semiformal correspondence demonstration Dependencies: No dependencies. Developer action elements: adv rcr.2.1d The developer shall provide an analysis of correspondence between all adjacent pairs of TSF representations that are provided. Content and presentation of evidence elements: adv rcr.2.1c For each adjacent pair of provided TSF representations, the analysis shall demonstrate that all relevant security functionality of the more abstract TSF representation is correctly and completely refined in the less abstract TSF representation. adv rcr.2.2c For each adjacent pair of provided TSF representations, where portions of both representations are at least semiformally specified, the demonstration of correspondence between those portions of the representations shall be semiformal. Evaluator action elements: adv rcr.2.1e The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence. ADV RCR.3 Formal correspondence demonstration Application notes The developer must either demonstrate or prove correspondence, as described in the requirements below, commensurate with the level of rigour of presentation style. For example, correspondence must be proven when corresponding representations are formally specified. Dependencies: No dependencies. Developer action elements: adv rcr.3.1d The developer shall provide an analysis of correspondence between all adjacent pairs of TSF representations that are provided. adv rcr.3.2d For those corresponding portions of representations that are formally specified, the developer shall prove that correspondence. Content and presentation of evidence elements: adv rcr.3.1c For each adjacent pair of provided TSF representations, the analysis shall prove or demonstrate that all relevant security functionality of the more abstract TSF representation is correctly and completely refined in the less abstract TSF representation. adv rcr.3.2c For each adjacent pair of provided TSF representations, where portions of one representation are semiformally specified and the other at least semiformally specified, the demonstration of correspondence between those portions of the representations shall be semiformal. adv rcr.3.3c For each adjacent pair of provided TSF representations, where portions of both representations are formally specified, the proof of correspondence between those portions of the representations shall be formal. Evaluator action elements: adv rcr.3.1e The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence. adv rcr.3.2e The evaluator shall determine the accuracy of the proofs of correspondence by selectively verifying the formal analysis. 0 ... 40 41 42 43 44 45 46 ... 73
|
