Symbolic algorithmic verification of intransitive generalized noninterference

Generalized noninterference can be used to formulate transitive security policies, but is unsuitable for intransitive security policies. We propose a new information flow security property, which we call intransitive generalized noninterference, that enables intransitive security policies to be specified formally. Next, we propose an algorithmic verification technique to check intransitive generalized noninterference. Our technique is based on the search for counterexamples and on the window induction proof, and can be used to verify generalized noninterference. We further demonstrate that the search of counterexamples and induction proof can be reduced to quantified Boolean satisfiability. This reduction enables us to use efficient quantified Boolean decision procedures to perform the check of intransitive generalized noninterference. It also reduces spatial requirement by representing the space compactly, and improves the efficiency of the verification procedure.