The development class encompasses four families of requirements for representing the TSF at various levels of abstraction from the functional interface to the implementation representation. The development class also includes a family of requirements for a correspondence mapping between the various TSF representations, ultimately requiring a demonstration of correspondence from the least abstract representation through all intervening representations to the TOE summary specification provided in the ST. In addition, there is a family of requirements for a TSP model, and for correspondence mappings between the TSP, the TSP model, and the functional specification. Finally, there is a family of requirements on the internal structure of the TSF, which covers aspects such as modularity, layering, and minimisation of complexity.
Figure 10.1 shows the families within this class, and the hierarchy of components within the families.
Figure 10.1 - Development class decomposition
The paradigm evident for these families is one of a functional specification of the TSF, decomposing the TSF into subsystems, decomposing the subsystems into modules, showing the implementation of the modules, and demonstration of correspondence between all decompositions that are provided as evidence. The requirements for the various TSF representations are separated into different families, however, to allow the PP/ST author to specify which subset of the TSF representations are required.
Figure 10.2 - Relationships between TOE representations and requirements
Figure 10.2 indicates the relationships between the various TSF representations and the objectives and requirements that they are intended to address. As the figure indicates, the APE and ASE classes define the requirements for the correspondence between the functional requirements and the security objectives as well as between the security objectives and the TOE's anticipated environment. Class ASE also defines requirements for the correspondence between both the security objectives and functional requirements and the TOE summary specification.
The requirements for all other correspondence shown in Figure 10.2 are defined in the ADV class. The ADV_SPM family defines the requirements for correspondence between the TSP and the TSP model, and between the TSP model and the functional specification. The ADV_RCR family defines the requirements for correspondence between all available TSF representations from the TOE summary specification through the implementation representation. Finally, each assurance family specific to a TSF representation (i.e. ADV_FSP, ADV_HLD, ADV_LLD and ADV_IMP) defines requirements relating that TSF representation to the functional requirements, the combination of which helps to ensure that the TOE security functional requirements have been addressed. The traceability analysis is always to be performed from the highest-level TSF representation down through each of the TSF representations that are provided. The CC captures this traceability requirement via dependencies on the ADV_RCR family. The ADV_INT family is not represented in this figure, as it is related to the internal structure of the TSF, and is only indirectly related to the process of refinement of the TSF representations.
Application notes
The TOE security policy (TSP) is the set of rules that regulate how resources are managed, protected and distributed within a TOE, expressed by the TOE security functional requirements. The developer is not explicitly required to provide a TSP, as the TSP is expressed by the TOE security functional requirements, through a combination of security function policies (SFPs) and the other individual requirement elements.
The TOE security functions (TSF) are all the parts of the TOE that have to be relied upon for enforcement of the TSP. The TSF includes both functions that directly enforce the TSP, and also those functions that, while not directly enforcing the TSP, contribute to the enforcement of the TSP in a more indirect manner.
Although the requirements within the ASE_TSS family and within several families of this class call for several different TSF representations, it is not absolutely necessary for each and every TSF representation to be in a separate document. Indeed, it may be the case that a single document meets the documentation requirements for more than one TSF representation, since it is the information about each of these TSF representations that is required, rather than the resulting document structure. In cases where multiple TSF representations are combined within a single document, the developer should indicate which documents meet which requirements.
Three types of specification style are mandated by this class: informal, semiformal and formal. The functional specification, high-level design, low-level design and TSP models will be written using one or more of these specification styles. Ambiguity in these specifications is reduced by using an increased level of formality.
An informal specification is written as prose in natural language. Natural language is used here as meaning communication in any commonly spoken tongue (e.g. Dutch, English, French, German). An informal specification is not subject to any notational or special restrictions other than those required as ordinary conventions for that language (e.g. grammar and syntax). While no notational restrictions apply, the informal specification is also required to provide defined meanings for terms that are used in a context other than that accepted by normal usage.
A semiformal specification is written in a restricted syntax language and is typically accompanied by supporting explanatory (informal) prose. The restricted syntax language may be a natural language with restricted sentence structure and keywords with special meanings, or it may be diagrammatic (e.g. data-flow diagrams, state transition diagrams, entity-relationship diagrams, data structure diagrams, and process or program structure diagrams). Whether based on diagrams or natural language, a set of conventions must be supplied to define the restrictions placed on the syntax.
A formal specification is written in a notation based upon well-established mathematical concepts, and is typically accompanied by supporting explanatory (informal) prose. These mathematical concepts are used to define the syntax and semantics of the notation and the proof rules that support logical reasoning. The syntactic and semantic rules supporting a formal notation should define how to recognise constructs unambiguously and determine their meaning. There needs to be evidence that it is impossible to derive contradictions, and all rules supporting the notation need to be defined or referenced.
Significant assurance can be gained by ensuring that the TSF can be traced though each of its representations, and by ensuring that the TSP model corresponds to the functional specification. The ADV_RCR family contains requirements for correspondence mappings between the various TSF representations, and the ADV_SPM family contains requirements for a correspondence mapping between the TSP model and the functional specification. A correspondence can take the form of an informal demonstration, a semiformal demonstration, or a formal proof.
When an informal demonstration of correspondence is required, this means that only a basic correspondence is required. Correspondence methods include, for example, the use of a two-dimensional table with entries denoting correspondence, or the use of appropriate notation of design diagrams. Pointers and references to other documents may also be used.
A semiformal demonstration of correspondence requires a structured approach at the analysis of the correspondence. This approach should lessen ambiguity that could exist in an informal correspondence by limiting the interpretation of the terms included in the correspondence. Pointers and references to other documents may be used.
A formal proof of correspondence requires that well-established mathematical concepts be used to define the syntax and semantics of the formal notation and the proof rules that support logical reasoning. The security properties need to be expressible in the formal specification language, and these security properties need to be shown to be satisfied by the formal specification. Pointers and references to other documents may also be used.
The ADV_RCR.*.1C elements require that the developer provide evidence, for each adjacent pair of TSF representations, that all relevant security functionality of the more abstract TSF representation is refined in the less abstract TSF representation. The ADV_FSP.*.2E, ADV_HLD.*.2E, ADV_LLD.*.2E and ADV_IMP.*.2E elements each require the evaluator to determine that the TSF represented by that family of requirements is an accurate and complete instantiation of the TOE security functional requirements. In order to determine that a TSF representation is an accurate and complete instantiation of the TOE security functional requirements, it is intended that the evaluator use the evidence provided by the developer in ADV_RCR.*.1C as an input to this determination. By establishing a correspondence between the TOE security functional requirements and each of successive TSF representations down the chain, this step-wise process will ultimately provide more assurance that the least abstract TSF representation corresponds to the TOE security functional requirements, which is the ultimate goal of this class. If the evaluator makes no correspondence determinations back to the TOE security functional requirements for intermediate TSF representations, then trying to determine the correspondence from the least abstract TSF representation back to the TOE security functional requirements may represent too large a step to be accurately performed. Finally, depending on the set of TSF representations that are required, it is quite possible that the low-level design, high-level design, or even the functional specification might be the least abstract TSF representation that is provided.