Search Optimization, Capacity Calculation And Mitigation Of Covert Channel By Noninterference Analysis

Nowdays, due to our country and society widespread dependence on computer and network technology, information security is more and more valued. Standard security mechanisms such as access control are essential components for proctecting the confidentiality and integrity of data. But even in a secure system which has been implemented Mandatory Access Control mechanism, a high-level process can signal information to a low-level process by using covert channel. Information flow control can provide such guarantees.In information flow control, the security policy is often formalized as noninterference polices, which requires that confidential inputs not affect the publicly visible outputs. In this respect, our thesis uses noninterference model, and focuses the following three interralated aspects.Existing algorithmic approaches to verifying noninterference suffer from the state explosion problem. In order to make these approaches more practical, we proposed an abstraction technique which attempts to decrease the size of the security system by focusing on variables and local transitions of the system related with noninterference. In this way, noninterference is preserved, but the size of the model that needs to be verified becomes smaller. We futher showed how the technique can be applied in verifying the programming language IMP. Our technique also can be extended to verify intransitive noninterference smoothly.A method based on information entropy to analyze the capacity of covert channels was proposed. Built upon noninterference, the method is firstly used to calculate the covert channel capacity, then to analyze the factors that have an impact on this quantity. Finally an example is given of the capacity calculation for covert channels.A capacity using covert channel mitigation method was proposed. This method uses capacity as metric for channel danger measure according to trusted computer system evaluation criteria (TCSEC). The algorithms of channel's capacity measure and policy's parameter computing are also presented. The method implements the restriction criterion on channel's capacity effectively and accurately, and it also decreases the influence of restriction operation on system performance.