Paper Info
Title
Automated Verification of Noninterference Property.
Abstract
Noninterference is an important information flow model that is widely applied in building secure information systems. Although the noninterference model itself has been thoroughly investigated, verifying the noninterference property in an efficient and automated manner remains an open problem. In this study, we explore the noninterference verification problem from the perspective of the state-equivalence relations between two automata running synchronously. Our results are as follows. (1) To the best of our knowledge, we are the first to propose a recursive form of the necessary and sufficient condition of noninterference. We also for the first time disclose the fact that Rushby’s definition of noninterference model can also be formalized as a bi-simulation (over two automata) (2) We present an automated noninterference verification algorithm. The algorithm can finish the verification within ( O(|S|^{2} *|D|) ), where ( |D| ) is the number of security domains and ( |S| ) is the number of states. The time-complexity of our algorithm is the best among other existing studies.
Year
Venue
Field
2018
ICICS
Information system,Information flow (information theory),Open problem,Computer science,Automaton,Theoretical computer science,Recursion,Distributed computing
DocType
Citations 
PageRank 
Conference
0
0.34
References 
Authors
16
6
Name
Order
Citations
PageRank
Fan Zhang100.34
Cong Zhang214926.42
Mingdi Xu3254.91
Xiaoli Liu401.01
Fangning Hu541.36
Han-Chieh Chao62502214.00