Modeling and justification of the store and forward protocol: Covert channel analysis

In an environment where two networks with different security levels are allowed to communicate, a covert channel is created. The paper aims at calculating the probability of establishing a covert channel between the high security network and the low security network using Markov Chain Model. The communication between the networks follows the Bell-LaPadula (BLP) security model. The BLP model is a "No read up, No write down" model where up indicates an entity with a high security level and down indicates an entity with a low security level. In networking, the only way to enforce the BLP model is to divide a network into separate entities, networks with a low security level, and others with a high security level. This paper discusses our analysis of the Store and Forward Protocol that enforces the BLP security model. The Store and Forward Protocol (SAFP) is a gateway that forwards all data from a low security network to a high security network, and it sends acknowledgments to the low security network as if they were sent from the high security network; thereby achieving reliability of the communication in this secure environment. A timing covert channel can be established between the two networks by using the times of the acknowledgments to signal a message from the high security network to the low security network. A high security network may send acknowledgments immediately or with some delay where the time of the acknowledgments arrival is used to convey the message. The covert channel probability is found to be equal to the blocking probability of the SAFP buffer when analyzing the problem using Markov Chain Model. Increasing the size of the buffer at the SAFP decreases the covert channel probability. Carefully determining the size of the buffer of the SAFP ensures minimizing the covert channel probability.