ADV_SPM.3 Formal TOE security policy model
Dependencies:
ADV_FSP.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:
ADV_SPM.3.1E The evaluator shall confirm that the information provided meets all requirements for content and presentation of evidence.