A practical method for the identification of covert storage channels is presented and its application to the source code of the Secure Xenix kernel is illustrated. The method is based on the identification of all visible/alterable kernel variables by using information-flow analysis of language code. The method also requires that, after the sharing relationships among the kernel primitives and the visible/alterable variables are determined, the nondiscretionary access rules implemented by each primitive be applied to identify the potential storage channels. The method can be generalized to other implementation languages, and has the following advantages: it helps discover all potential storage channels is kernel code, thereby helping determine whether the nondiscretionary access rules are implemented correctly; it helps avoid discovery of false flow violations and their unnecessary analysis; and it helps identify the kernel locations where audit code and time-delay variables need to be placed for covert-channel handling.>

A Markov model for bandwidth computation and its application to Secure Xenix are presented. The model can be used for computing the bandwidth of both individual channels and aggregated channels (i.e. serial and parallel aggregation). Using this model, a tool has been built and experiments conducted to determine the factors that affect the bandwidth of covert storage channels (noise, scheduling delays, load, etc.). The tool can be used to compute the minimum delays for each channel under various loads and program behavior. Thus, it allows the placement of dynamically adjustable delays in multiprogrammed systems, which guarantees minimum performance impact.>

A formal method for the identification of covert storage channels is presented and its application to the source code of the Secure Xenix* kernel is illustrated. The method is based on the identification of all visible/alterable kernel variables by using information flow analysis of language code (e.g., C language code). The method also requires that, after the sharing relationships among the kernel primitives and the visible/ alterable variables are determined, the non-discretionary access rules implemented by each primitive be applied to identify the covert storage channels. The method can be generalized to other implementation languages, and has the following advantages: (1) it leads to the discovery of all storage channels in kernel implementations, (2) it helps determine whether the non-discretionary access rules are implemented correctly, and (3) it can be automated. An additional important aspect of applying this method to a kernel interface is the discovery of all kernel variables that are modified directly or indirectly through that interface. The analysis of the modification scenarios provides the necessary conditions for all kernel penetration. This implies that, in any kernel that enforces both a non-discretionary security and an integrity policy, penetration instances are the dual of covert storage channels instances.