This technical paper contains the results of an application of two covert channel analysis techniques to the Honeywell Secure Ada Target (SAT) design. The two techniques are the non-interference model of Goguen and Meseguer and the shared-resource method of Kemmerer. The Gypsy specification method is used to produce a high-level design for the SAT. This design is then analyzed by the non-interference and shared-resources methods.
The finite state machine is used as the SAT abstract model. Security is defined as a global state, which contains all the dynamic data structures of the model. The security policy is an access mediation policy, with additional constraint relations to the SAT-type enforcement mechanism.
The minimum criteria for a storage channel are as follows:
(1) The sending and receiving processes must have access to the same shared entity.
(2) The sending process must be capable of forcing the shared entity to change.
(3) The receiving process must be capable of detecting a change in the shared entity.
(4) There must be a mechanism for initiating communication and for synchronizing the sending and receiving processes.
For a timing channel, the minimum criteria are as follows:(1) The sending and receiving processes must have access to the same shared entity.
(2) The sending and receiving processes must have access to a time reference.
(3) The sender must be capable of altering the amount of time it takes the receiver to detect a change in the shared entity.
(4) There must be a mechanism for initiating communication and for synchronizing the sending and receiving processes.
Both methods are applied successfully. The non-interference approach detects the channel in violation of the non-interference version of multi-level security. The shared-resource matrix method detects both channels in violation of the SAT mandatory security and tape enforcement policies. The authors (rightly) conclude that neither method is comprehensive by itself. They theorize that a combination of the two methods could be comprehensive in detecting covert channels.
The authors characterize the designable properties of such a method:
(1) It should identify regions where no channels exist to reduce the scope of the analysis task as much as possible.
(2) It should positively identify all channels that are present.
(3) It should identify the vehicles used for the transfer of information both in terms of the objects and the attributes of the objects affected.
(4) It should facilitate analysis of the channels found to determine characteristics such as bandwidth and signal to noise ratios.
(5) It should be parameterizable to a particular security or more general information flow policy. (The SAT type enforcement is an example of the latter.)
Future research directions are set. Both methods will be used on lower-level specifications and extended per the above properties. The paper is well written and contains adequate references. It will be of interest to those involved in security research. It will also be of interest to those following the development of Ada software. The early results are promising, and the follow-up work should be of interest as well.
