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 of applicable policies of the TSP in the TSP model and to ensure that the TSP model 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, ADV_SPM.1.1C may also be met with either a semiformal or formal TSP model, and ADV_SPM.2.1C may also be met with a formal TSP model. Furthermore, ADV_SPM.2.5C and ADV_SPM.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.