A flow can be represented by (S,-->), where S is a given set of security classes and --> is a flow relation specifying permissible flows between pairs of classes. Each storage object x - e.g. constant, scalar variable, array, or file - is assigned (bound) to a security class, denoted #x. The notation x-->#y thus means that a flow from object x to object y is permissible in the flow policy. We will suppose the binding of each object to a security class is static and can be determined from the declarations contained in the program.
Under the reasonable assumptions that there is a finite number of security classes, that the flow relation is reflexive(i.e. #x-->#x is always permissible), and that the flow relation is transitive (i.e. #x-->#y-->#z implies #x-->#z), we may supppose that (S,-->) is a lattice. This means that, corresponding to any pair of classes, there are unique upper and lower bound classes. If (S,-->) is not a lattice, it may be transformed into one by adding new classes as necessary without changing the flows among the original classes. The lattice properties are exploited to construct an efficient certification mechanism.
The symbols + and * denote, respectively, the associative and commutative least upper bound and greatest lower bound operators of the lattice (S,-->). The least upper bound is defined so that #xi-->#y for i=1,..,m is equivalent to the relation #x1+...+#xm-->y. It can be envisaged as requiring that flows from various operand classes must pass through a single common class en route to a given result class. The greatest lower bound is defined so that #x-->#yj for j=1,..,n is equivalent to the relation #x-->#y1*...*#yn. It can be envisaged as requiring that flows from a given operand class must pass through a single common class en route to various result classes. There is a highest class H, which is the least upper bound of all classes, and a least class L, which is the greatest lower bound of all classes.
All unnamed programming languages constants are members of L. This assumption is reasonable since the flow of an ordinary constant, say "99", into a variable, say x, puts in x no information about any other object. Only when "99" is known to be the value of an object y for which #y-/->#x must its flow be prevented; but this is done by resticting the flow form y, not from "99".
Figures 1 and 2 illustrate lattices that arise frequently in
practice.
Figure 1 is a linear "priority lattice" on n classes 0,1,...,n-1, where L=0 and H=n-1. This
lattice applies to the simple confinement problem with classes nonconfidential (0) and confidential
(1) and to the common military security problem with classes unclassified (0), confidential (1),
secret (2), and top secret (3).
Figure 2 shows a more complex "property lattice" representing the immediate inclusions among all 2^n subsets of n=3 properties represented as bit vectors. It generalizes easily to any valu of n and is used in systems where information may flow only to a security class having at least the same properties as the originating class.
Information flows from object x to object y, denoted x => y, whenever information stored in x is transferred to, or used to derive information transferred to, y. A program statement specifies a flow x => y if execution of the statement could result in a flow x => y.
Flows are explicit or implicit. An explicit flow x => y occurs whenever the
operations generating it are independent of the value of x. Assignment statements, I/O statements,
and value-returning procedure calls generate explicit flows. An implicit flow x => y occurs whenever a statement specifies a flow from some arbitrary z to y, but execution depends on the value of
x. Consider, for example, the statements
y := 1; if x = 0 then y :=0,
where x is either 0 or 1. On termination of these statements, x =y whether or not the then clause was executed. hence the if statement causes an implicit flow x => y. In general, all
conditional structures generate implicit flows.
It should be noted that the relation => is transitive, that is, x => y => z implies x=> z. If x => y because some function having x as an operand stores its result in y, the flow is direct; otherwise it is indirect. An assignment "y := f(...,x,...)" thus causes flow x => y directly, while the pair "z := f(...,x,...); y := f(...,z,...)" causes flow x => y indirectly.
A program p is secure if and only if no execution of p results in a flow x => y unless #x-->#y. A necessary and sufficient condition for the security of [ is then
x => y for some execution of p only if #x-->#y. (1)
Unfortunately condition (1) is generally undecidable. Any procedure purported to decide it could be applied to the statement
if f(x) halts then y :=0
and thus provide a solution to the halting problem for an arbitrary recursive function.
The undecidability is removed if we replace (1) with the security condition
x => y is specified by p only if #x-->#y. (2)
The previous if statement can clearly be tested for this condition. However, security condition (2) gives less precision in program certification than (1). For example, consider the program
if x=0 then if x <> 0 then y := z
and a flow relation that disallows only z => y. This program is secure by (1) since no execution of it can result in z => y, but it will not be certified by a mechanism based on (2) since it specifies
z => y.
When the security classes of the variables are declared in a program and are static, it is easy to incorporate the certification process into the analysis phase of a compiler. The mechanism will be
presented in the form of When external objects, such as files and separately compiled procedures, are bound to a program, the linker must verify that the actual security class of each such object corresponds properly to the
security class declared formally for it in the program. This must be done before a program is exectuted.
The certification mechanism exploits lattice properties for efficiency. The transitive flow relation implies that sequences of secure direct flows are secure and hence the semantics need only certify
the direct flows implied by each syntactic type. The least upper and greatest lower bound properties greatly simplify the amount of information needed to track the origins and destinations of flows.
Suppose x1,...xm are sources of information for some receiving object y, as in assignment "y := f(x1,...,xm)" or in an output statement "output x1,...,xm to y". Rather than certify
#xi-->#y for each i, the compiler may form A = #x1 + ... + #xm as the source objects are recognized, and verify simply A-->#y -only a single internal variable representing the maximal class of the source
objects is needed. Now, suppose y1,...,yn are to receive information derived from some source object x, as in an input statement "input y1,...,yn from x", or in a structure generating
implicit flows from an object x in a conditional expression to objects yj in that structure's scope. Rather than certify #x-->#yj separately for each j, the compiler may form B = #y1 * ... * #yn as the
receiving objects are being recognized and verify simply #x-->B -only a single internal variable representing the minimal class of the receiving objects is needed.
A universally bounded lattice is a structure consisting of a finite partially ordered set together with least upper and greatest lower bound operators on the set.
Lattice Structure
To show that (S,-->,+,*) forms such a lattice, you need to prove the following properties:
(1) (S,-->) is a partial ordered set.
(2) S is finite.
(3) S has a lower bound L such that L-->A for all A in S.
(4) + is a least upper bound operator on S.
These assumptions then imply the existence of a greatest lower bound operator on S, which we denote by "*". This in turn implies the existence of a unique upper bound H. Therefore, the structure
(S,-->,+,*) is a lattice with lower bound L and upper bound H.
The least upper bound operator is defined in the following manner:
For all a and b in S there exists a unique class c = a+b, c in S, such that :
- a-->c V b-->c, and
for all d in S :: (a-->d V b-->d) => c-->d.
The greatest lower bound operator is defined in the following manner:
For all a and b in S there exists a unique class c = a*b, c in S, such that :
- c-->a V c-->b, and
for all d in S :: (d-->a V d-->b) => d-->c.
Go back
References