Research On The Computational Aspect Of Covert Channels

As an important guideline, both TCSEC and CC, which from U.S. Department of Defense and ISO respectively, have the clear requirement for covert channels, i.e. the different intense of covert channel analysis are required for software that apply for B2, EAL5 or above certifications. Covert channel analysis consists of three stages: search, audit and handling. After the booming era in 80s and 90s at last century, covert channel and related research progress slowly. An explanation for that is the disjunction lies between application and fundamental researches. Since there are no complete formal description system and related mathematical tools for covert channel, application research can not progress rapidly. The most important work of this dissertation is present a kind of formal definition and introduce mathematical tool for covert channels, moreover, the characteristics are deduced and analysis work is conducted based on that, which are critical parts of fundamental research of covert channels.The main works of this dissertation can be summarized as two parts: (1) Research on the computational aspect of covert channels; (2) Application research which based on (1).Firstly, this dissertation presents a kind of formal definition of covert channel by analyze the related factors of trusted system and the working principle of covert channels; therefore we deduce the general characteristics, computational characteristics and the minimum requirement of covert channels. Moreover, an algebra system is given via introduce binary operation relationships into the set of covert channels. According to topology evolution of covert channels, the changes of computational characteristics can be calculated by this algebra system.Secondly, a new audit criterion is presented to mediate the drawbacks of TCSEC's audit criteria for covert channels that have been observed in our practice. This new criterion, i.e.α-IA, integrates bandwidth, security level weight difference, working time and sensitive parameter. This new criterion not only can compatible with the ones in TCSEC, but also can evaluate the threats of covert channels from different point of view by the users' requirements. Moreover, the calculating methods in this criterion are discussed in detail under the algebra system mentioned above.Thirdly, based on the minimum requirement of covert channels that has been proved on the research of computational aspects, the static search and elimination methods of covert channels are analyzed from the view of taxonomy. The basic idea and succinct procedure is summarized, moreover, both advantages and disadvantages of each method are discussed. Furthermore, the dynamic method is presented to overcome the drawbacks of static method. Not like the static method that based on system top-level specification or source code analysis, this kind of new method conducts under operating environment, nowadays, it can be used as either an independent method or the complement of static method. Generally, the cost of dynamic method is lower than that of static. Search is the foundation of audit and handling, for the importance of search, the general auto covert channels searching is discussed in this dissertation, therefore proved it's a kind of undecidable problem, i.e. there is not an algorithm can distinguish whether an arbitrary program includes any covert channels within finite time. This tells us that we can't count on a single program to solve covert channels detection thoroughly.Finally, according to the formal definition given under the research on the computational aspect and emulate the working principle of covert channels, a simulation system of covert channels is developed. By design and use different communication protocols, the simulation tests are conducted roundly, which includes bandwidth, anti-interference performance, etc. At simulation, some phenomena that cannot be awared under static analysis are observed, furthermore, the causes of that is analyzed. In the final section, we propose that semantic analysis of covert channels is one of the most promising research areas in the near future.The main contributions of this dissertation are as follows:(1) The formal definition of covert channels is presented, moreover, based on it, the characteristics are deduced and an algebra system is introduced for covert channels. These provide the theory foundation and mathematical tool for covert channels formal research.Generally, researchers provided specific methods for given covert channels problems at early time, so these methods seem independent to each other and lack of necessary theory foundation. Under this situation, not only can't covert channel research conduct from formal method level, but also depend on experiment and observation to find the new attributes and test the correctness of related handle methods of covert channel only.(2) A new criterion for covert channels auditing is defined, which not only can compatible with the related ones in TCSEC, but also can evaluate the threats of covert channels from different point of views by users' requirement.TCSEC uses bandwidth as unique parameter to audit the threat of covert channels, therefore the higher bandwidth has, the bigger threat get. The drawback of this method is it overlook the others attributes of cover channel can also harm the security of system. For instance, there are two covert channels with bandwidth 200 bits/s each, one leaks the sensitive information from Top Secret to Public, and the other leaks the same information from Top Secret to Secret only. It's clearly that these two covert channels do not have the same negative influence to the security of system. Moreover, if one of them only worked one second and the other worked one hour, how to evaluate the threat of them? TCSEC not provide answers for these questions.(3) Propose the dynamic methods for covert channels detection and elimination.Static search and elimination methods for covert channels are based on system top-levelspecification or source code analysis. It's prone to find some pseudo illegal information flow while at operating. Eliminate these pseudo illegal information flows not only can decrease the efficiency unnecessarily, but also consume the limited human and material resources.Dynamic search and elimination methods are utilize the minimum requirement that we have deduced on the research of computational aspect of covert channel to search or eliminate covert channels under the running environment of system. Because this kind of method is operate in running circumstance, so compare with static method, it checks the reality information flows within the running system only instead of checks the legality of each possible information flows, therefore it decrease the complexity of analysis work and improve the efficiency.