|
|
 |
| |
|
|
|
Algorithmic Verification of Intransitive Noninterference for 3-domain Security Policies with a SAT Solver |
|
|
|
PP: 1825-1835 |
|
|
|
Author(s) |
|
|
|
Liu Zhifeng,
Zhou Conghua,
Ge Yun,
Zhang Dong,
|
|
|
|
Abstract |
|
|
| In this paper we propose an automated verification approach to checking intransitive noninterference for deterministic
finite state systems. Our approach is based on the counterexamples search verification strategy, and is conducted in gradual manner. It
produces counterexamples of minimal length. Further, we reduce the counterexamples search to propositional satisfiability. For the case
that there are no counterexamples, we also introduce the window induction proof method in order to avoid considering unnecessary
iterations, and show that the induction proof can be performed by the boolean decision procedure. In addition, based on graph-theoretic
properties of systems we propose an over-approximation to the length of the smallest counterexample, and the over-approximation can
also be checked by the boolean decision procedure. |
|
|
|
|
|
|
|
