A Divide Algorithm Based On Information-flow Chart Build Forest And Design Information-flow On The PVS

With the importance of information exchange, Covert-Channels' hazards become more and more prominent in today. Covert-Channels agreed encoding with higher and lower (H and L) level security user or process in Multi-level security system first. Then, Covert-Channels use H to change the properties of shared resources. And L could read the changes of shared resources. At last, Covert-Channels could transfer the message which breach system security strategy from H to L. Thus, the security model does not preclude Covert-Channels steal confidential information. In other words, security Model is powerless to prevent the information attack from Covert-Channels.Information-flows of mains and objects in a Multi-Level Security System could be used to describe an information-flow chart. This information-flow chart is the important basis of Covert-Channels' research. But the information-flow chart in big system is intricately. The workload is very large if we analysis and search Covert-Channels in information-flow chart. In order to improve the efficiency of search and analysis the Covert-Channels, we made a new segmentation algorithm which builds information-flow forest from information-flow chart. Firstly, a father tree was arbitrarily selected in the algorithm. Then the branch can be replaced by the arc from cut set. Theoretically, information-flow forest could be inherited information from information-flow chart correctly by the segmentation algorithm. Thus, the entire information-flow chart can be replaced according to analysis the information-flows in every tree. So we could search and analysis the Covert-Channels in these trees. And it could effectively lower the analysis of the complexity of the problem.The PVS (Prototype Verification System) was introduced in the second step. Based on the PVS, the Covert-Channels in Information-flow tree will be analyzed. Firstly, the logic of the Information-flow tree was described into the PVS languages, lemmas and theorems. Then, the author used the PVS to prove weather the Information-flow tree has Covert-Channels or not. In our research, if an Information-flow tree has Covert-Channels, it couldn't pass all the PVS proves. Otherwise, if an Information-flow tree hasn't Covert-Channels, it could pass all the PVS proves.Two examples were used to formulate the Information-flow forest and to incarnate the whole work of this research. It shows that algorithmic and PVS source programs could reduce the human workload greatly via our model.