SAT-based Algorithmic Verification of Noninterference

In this paper we propose an algorithmic verification technique to check noninterference for deterministic finite state systems. Our technique integrates the counterexamples search strategy and window induction proof strategy. This integration generates counterexamples of minimal length faster. We further show how Boolean decision procedures can perform searching for counterexamples and the induction proof. Since our technique translates the search of counterexamples of increasing length into a sequence of propositional satisfiability checks, we also exploit the similarity of these SAT instances by conflict-driven learning during conflict analysis from one instance to the next.