Symbolic algorithmic verification of intransitive generalized noninterference  

作　　者：ZHOU CongHua LIU ZhiFeng WU HaiLing CHEN Song JU ShiGuang 

机构地区：[1]School of Computer Science and Telecommunication Engineering,Jiangsu University Zhenjiang 212013,China

出　　处：《Science China(Information Sciences)》2012年第7期1650-1665,共16页中国科学（信息科学）（英文版）

基　　金：supported by National Natural Science Foundation of China (Grant Nos. 60773049, 61003288);PhD Programs Foundation of Ministry of Education of China (Grant No. 20093227110005);Natural Science Foundation of Jiangsu Province (Grant No. BK2010192);People with Ability Foundation of Jiangsu University(Grant No. 07JDG014);Fundamental Research Project of the Natural Science in Colleges of Jiangsu Province(Grant No. 08KJD520015)

摘　　要：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 re- duced 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.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 re- duced 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.

关 键 词：intransitive generalized noninterference quantified Boolean satisfiability symbolic verification multi-level security 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构] O436.1[自动化与计算机技术—计算机科学与技术]