A method of identifying covert storage channels in secure systems is based on analysis of source code. The method is illustrated with examples taken from an analysis of Secure Xenix.

The method is based on identifying all directly and indirectly visible and alterable kernel variables. It addresses and resolves the aliasing of kernel variables to determine their indirect alterability, and uses information flow analysis to determine the indirect visibility of kernel variables. The use of the variables by kernel primitives is then performed before applying the nondiscretionary secrecy or integrity rules to identify the channels.

The interesting aspect of this paper is that it deals with the code associated with the secure system rather than just formal top-level specification. In particular, the paper makes the point that a significant amount of implementation code and variables (such as those of many kernel processes) has no correspondent formal specifications, and this code may contain storage channels.

The authors claim that the methods described apply to other implementation languages, not just C. They also speculate on the covert channels that can arise at the hardware interface using as an example the status, position, and movement of a disk arm, but make no claims for their method to detect shared variables and flows of hardware or microcode specifications.

The paper is moderately abstract, but is readable by anyone who is interested enough to do so. It is recommended to anyone interested in the identification of covert channels in trusted code.