Extend the semantics of the information flow security mechanism in Section 15.2.1 for records (structures).
15.2.1:
For our discussion, we assume that the allowed flows are supplied to the checking
mechanisms through some external means, such as from a file. The specifications of
allowed flows involve security classes of language constructs. The program involves
variables, so some language construct must relate variables to security classes. One
way is to assign each variable to exactly one security class. We opt for a more liberal
approach, in which the language constructs specify the set of classes from which
information may flow into the variable. For example,
x: integer class { A, B }
states that x is an integer variable and that data from security classes A and B may
flow into x. Note that the classes are statically, not dynamically, assigned. Viewing
the security classes as a lattice, this means that x’s class must be at least the least
upper bound of classes A and B—that is, lub{A, B} ≤ x.
Two distinguished classes, Low and High, represent the greatest lower bound
and least upper bound, respectively, of the lattice. All constants are of class Low.
Information can be passed into or out of a procedure through parameters.
We classify parameters as input parameters (through which data is passed into
the procedure), output parameters (through which data is passed out of the procedure), and input/output parameters (through which data is passed into and out
of the procedure). (* input parameters are named is; output parameters, os; *)
(* and input/output parameters, ios, with s a subscript *)
proc something(i1, ..., ik; var o1, ..., om, io1, ..., ion);
var l1, ..., lj; (* local variables *)
begin
S; (* body of procedure *)
end;
The class of an input parameter is simply the class of the actual argument:
is: type class { is }
Let r1, ..., rp be the set of input and input/output variables from which information
flows to the output variable os. The declaration for the type must capture this:
os: type class { r1, ..., rp }
(We implicitly assume that any output-only parameter is initialized in the procedure.)
The input/output parameters are like output parameters, except that the initial value
(as input) affects the allowed security classes. Again, let r1, ..., rp be defined as
above. Then:
ios: type class {r1, ..., rp, io1, ..., iok }
EXAMPLE: Consider the following procedure for adding two numbers.
proc sum(x: int class { x };
var out: int class { x, out });
begin
out := out + x;
end;
Here, we require that x ≤ out and out ≤ out (the latter holding because ≤ is reflexive).
The declarations presented so far deal only with basic types, such as integers,
characters, floating point numbers, and so forth. Nonscalar types, such as arrays,
records (structures), and variant records (unions) also contain information. The rules
for information flow classes for these data types are built on the scalar types.
Consider the array
a: array 1 .. 100 of int;
First, look at information flows out of an element a[i] of the array. In this case,
information flows from a[i] and from i, the latter by virtue of the index indicating which element of the array to use. Information flows into a[i] affect only the value
in a[i], and so do not affect the information in i. Thus, for information flows from
a[i], the class involved is lub{ a[i], i }; for information flows into a[i], the class
involved is a[i].
Trending now
This is a popular solution!
Step by step
Solved in 2 steps
