Symbolic Algorithmic Verification of Generalized Noninference

In multi-level security systems the leakage of confidential data, is in essence, the illegal flow of information. Generalized noninference characterizes the legal information flow between subjects with different security levels. Before the security system is applied, verifying whether it satisfies generalized noninference can eliminate all kinds of hidden data leakage and protect the confidentiality of data. At present the traditional verification approach for generalized noninference, i.e.“unwinding”, only checks a sufficient and non-neccessary condition making generalized noninference hold. Therefore the traditional approach is not complete. A complete verification approach for generalized noninference is proposed. It verifies generalized noninference by searching for counterexamples step by step. In order to guarantee the completeness of the approach, the double construction of finite state transition system is given, and based on the graph structure theory an approximate computation of the shortest counterexample is given. Further in order to increase the efficiency of the approach, the search of counterexamples and computation of the threshold are reduced to the quantified Boolean formula satisfiability problem. Then a symbolic verification procedure is established by a quantified Boolean formula solver. Finally, how to apply the approach to search for illegal information flow is explained by a case study of the disk-arm covert channel.