Раздел: Документация
0 ... 41 42 43 44 45 46 47 ... 73 10.7 Security policy modeling (ADV SPM) Objectives It is the objective of this family to provide additional assurance that the security functions in the functional specification enforce the policies in the TSP. This is accomplished via the development of a security policy model that is based on a subset of the policies of the TSP, and establishing a correspondence between the functional specification, the security policy model, and these policies of the TSP. Component levelling The components in this family are levelled on the basis of the degree of formality required of the TSP model, and the degree of formality required of the correspondence between the TSP model and the functional specification. Application notes While a TSP may include any policies, TSP models have traditionally represented only subsets of those policies, because modeling certain policies is currently beyond the state of the art. The current state of the art determines the policies that can be modeled, and the PP/ST author should identify specific functions and associated policies that can, and thus are required to be, modeled. At the very least, access control and information flow control policies are required to be modeled (if they are part of the TSP) since they are within the state of the art. For each of the components within this family, there is a requirement to describe the rules and characteristics ofapplicable policies of the TSP in the TSPmodel and to ensure that the TSPmodel satisfies the corresponding policies of the TSP. The "rules" and "characteristics" of a TSP model are intended to allow flexibility in the type of model that may be developed (e.g. state transition, non-interference). For example, rules may be represented as "properties" (e.g. simple security property) and characteristics may be represented as definitions such as "initial state", "secure state", "subjects" and "objects". In the context of the level of formality of the TSP model and the correspondence between the TSP model and the functional specification, informal, semiformal and formal are considered to be hierarchical in nature. Thus, ADVSPM.1.1C may also be met with either a semiformal or formal TSP model, and ADVSPM.2.1C may also be met with a formal TSP model. Furthermore, ADVSPM.2.5C and ADVSPM.3.5C may be met with a formal proof of correspondence. Finally, in the absence of any requirements on its level of formality, a demonstration of correspondence may be informal, semiformal or formal. ADV SPM.1 Informal TOE security policy model Dependencies: ADVFSP.1 Informal functional specification Developer action elements: adv spm.1.1d The developer shall provide a TSP model. adv spm.1.2d The developer shall demonstrate correspondence between the functional specification and the TSP model. Content and presentation of evidence elements: adv spm.1.1c The TSP model shall be informal. adv spm.1.2c The TSP model shall describe the rules and characteristics of all policies of the TSP that can be modeled. adv spm.1.3c The TSP model shall include a rationale that demonstrates that it is consistent and complete with respect to all policies of the TSP that can be modeled. adv spm.1.4c The demonstration of correspondence between the TSP model and the functional specification shall show that all of the security functions in the functional specification are consistent and complete with respect to the TSP model. Evaluator action elements: adv spm.1.1e The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence. ADV SPM.2 Semiformal TOE security policy model Dependencies: ADV FSP.1 Informal functional specification Developer action elements: adv spm.2.1d The developer shall provide a TSP model. adv spm.2.2d The developer shall demonstrate correspondence between the functional specification and the TSP model. Content and presentation of evidence elements: adv spm.2.1c The TSP model shall be semiformal. adv spm.2.2c The TSP model shall describe the rules and characteristics of all policies of the TSP that can be modeled. adv spm.2.3c The TSP model shall include a rationale that demonstrates that it is consistent and complete with respect to all policies of the TSP that can be modeled. adv spm.2.4c The demonstration of correspondence between the TSP model and the functional specification shall show that all of the security functions in the functional specification are consistent and complete with respect to the TSP model. adv spm.2.5c Where the functional specification is at least semiformal, the demonstration of correspondence between the TSP model and the functional specification shall be semiformal. Evaluator action elements: adv spm.2.1e The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence. ADV SPM.3 Formal TOE security policy model Dependencies: ADVFSP.1 Informal functional specification Developer action elements: adv spm.3.1d The developer shall provide a TSP model. adv spm.3.2d The developer shall demonstrate or prove, as appropriate, correspondence between the functional specification and the TSP model. Content and presentation of evidence elements: adv spm.3.1c The TSP model shall be formal. adv spm.3.2c The TSP model shall describe the rules and characteristics of all policies of the TSP that can be modeled. adv spm.3.3c The TSP model shall include a rationale that demonstrates that it is consistent and complete with respect to all policies of the TSP that can be modeled. adv spm.3.4c The demonstration of correspondence between the TSP model and the functional specification shall show that all of the security functions in the functional specification are consistent and complete with respect to the TSP model. adv spm.3.5c Where the functional specification is semiformal, the demonstration of correspondence between the TSP model and the functional specification shall be semiformal. adv spm.3.6c Where the functional specification is formal, the proof of correspondence between the TSP model and the functional specification shall be formal. Evaluator action elements: 0 ... 41 42 43 44 45 46 47 ... 73
|
