4.1 Interface ACC-FS


		Annex 1
		4.1 Interface ACC-FS

Contents
1 Characterization of the Interface
2 Example
3 Tool Support
4 Literature

Contents		1 Characterization of the Interface 2 Example 3 Tool Support 4 Literature

1 Characterization of the Interface

The interface corresponds to the type "information transmission in sequential order".

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).

2 Example

SRM matrix (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].

Objects Subjects
S1 S2 S3 S4
O1 m r - -
O1 r,m - - m
O1 - - r,m r,m

Objects	Subjects
S1	S2	S3	S4
O1	m	r	-	-
O1	r,m	-	-	m
O1	-	-	r,m	r,m

Figure 4.2: Example SRM-Matrix

In this example inadmissible information flow (according to Bell La Padula) is possible exactly when the security level of S[1] dominates the security level of S[2] (via object O[1]), when the security level of S[4] dominates the security level of S[1] (via object O[2]), when the security level of S[4] dominates the security level of S[3] (via object O[3]) or when the security level of S[3] dominates the security level of S[4] (via object O[3]).

Remark:
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.

Example:
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.

Example:
(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:

An assignment "b := e" is secure exactly when e ( b is valid (the information flows from b to e);

A sequence "S1;S2" is secure exactly when S1 and S2 are secure;

A branch "if e then S" and a loop "while e do S" is secure exactly when S is secure and e ( bj is valid for all variables bj out of S which may be modified in S (information may flow from e to S).

3 Tool Support

Since the analysis may become quite extensive in a very short time, the tool support is urgently required.

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.

4 Literature

/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