Symbolic algorithmic verification of intransitive generalized noninterference |
| |
Authors: | ZHOU CongHua LIU ZhiFeng WU HaiLing CHEN Song & JU ShiGuang |
| |
Affiliation: | School of Computer Science and Telecommunication Engineering,Jiangsu University Zhenjiang 212013,China |
| |
Abstract: | 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. |
| |
Keywords: | intransitive generalized noninterference quantified Boolean satisfiability symbolic verification multi-level security |
本文献已被 CNKI 等数据库收录! |
|