Symbolic algorithmic verification of generalized noninterference
Conghua Zhou · 2009
In this paper we propose an algorithmic verification technique to check generalized noninterference. Our technique is based on the counterexamples search strategy mainly which generating counterexamples of minimal length. In order to make the verification procedure terminate as soon as possible we also discuss how to integrate the window induction proof strategy in our technique. We further show how to reduce counterexamples search and induction proof to quantified propositional satisfiability. This reduction enables us to use efficient quantified propositional decision procedures to perform generalized noninterference checking. Keywords:Generalized noninterference; Quantified propositional satisfiability; Multilevel security I.