|4.1 Interface ACC-FS|
The specifications done with FS - Formal Specification and programs are investigated for covert channels by ACC - Analysis of Covert Channels. While only storage channels can be detected with the Information Flow Analysis it is also possible to perform an analysis with regard to time channels with Shared Resource Methodology (SRM).Shared Resource Methodology): A matrix with the subjects and objects is to be generated. The items of the matrix contain the access authorizations of the subject to the object (- (no access right), r (read), m (modify)). When laying down the Bell La Padula model an inadmissible information flow is possible if a subject S[i] may modify an object O[j] and a second subject S[k] may read this object O[j], but S[k] possesses a "lower" security level than S[i].
In this example inadmissible information flow (according to Bell La Padula) is possible exactly when the security level of S dominates the security level of S (via object O), when the security level of S dominates the security level of S (via object O), when the security level of S dominates the security level of S (via object O) or when the security level of S dominates the security level of S (via object O).
It is sufficient only to investigate direct accesses. The "transitive hull" must not be considered because every inadmissible indirect access is only possible by a way possessing also a direct inadmissible access.
Information Flow Analysis (/Denning, 1982/, p. 293 ff.): Every program statement and every variable is investigated whether there is an information flow between two variables and whether this only is admissible.
In "x := y+2" information flows from the variable y to the variable x, i. e. the security level of y has to dominate the one of x.
For every programming construct a rule has to be stated in order to detect whether the security requirements were violated.
(see /Denning, 1982/, section 5.4.2)
Is x a variable then x means the security level of this variable. An order (() exists on these security levels. The Bell La Padula model forms the basis for the following rules:
There are tools helping to generate and evaluate the SRM matrix. Since the subjects and objects have, generally, to be set up by hand, the success very much depends on a suitable selection of subjects and objects.
Note: If the variables of the program are considered as subjects and objects, the information flow analysis can be handled in this matrix.
|/Denning, 1982/||Training book for crypography and data security, especially the information flow analysis|
|/Kemmerer, 1983/||Description of the Shared Resource Methodology|
|GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster|