title: On the verification of intransitive noninterference in mulitlevel security.
abstract: We propose an algorithmic approach to the problem of verification of the property of intransitive noninterference (INI), using tools and concepts of discrete event systems (DES). INI can be used to characterize and solve several important security problems in multilevel security systems. In a previous work, we have established the notion of iP-observability, which precisely captures the property of INI. We have also developed an algorithm for checking iP-observability by indirectly checking P-observability for systems with at most three security levels. In this paper, we generalize the results for systems with any finite number of security levels by developing a direct method for checking iP-observability, based on an insightful observation that the iP function is a left congruence in terms of relations on formal languages. To demonstrate the applicability of our approach, we propose a formal method to detect denial of service vulnerabilities in security protocols based on INI. This method is illustrated using the TCP/IP protocol. The work extends the theory of supervisory control of DES to a new application domain.
authors.affiliation: CRISTAL Laboratory, Department of Applied Computer Sciences, National School of Information Sciences, University of Manouba, Tunisia. nejib.benhadjalouane@ensi.rnu.tn
authors.forename: Nejib
authors.initials: N
authors.lastname: Ben Hadj-Alouane
authors.forename: Stéphane
authors.initials: S
authors.lastname: Lafrance
authors.forename: Feng
authors.initials: F
authors.lastname: Lin
authors.forename: John
authors.initials: J
authors.lastname: Mullins
authors.forename: Mohamed Moez
authors.initials: MM
authors.lastname: Yeddes
mesh_terms: D000465:Algorithms; D001185:Artificial Intelligence; D003195:Computer Communication Networks; D016494:Computer Security; D016247:Information Storage and Retrieval / Q000379:methods*; D010363:Pattern Recognition, Automated / Q000379:methods*