Related Experiment Videos
On the verification of intransitive noninterference in mulitlevel security
Nejib Ben Hadj-Alouane1, Stéphane Lafrance, Feng Lin
1CRISTAL Laboratory, Department of Applied Computer Sciences, National School of Information Sciences, University of Manouba, Tunisia. nejib.benhadjalouane@ensi.rnu.tn
Summary
This study introduces a new algorithmic method for verifying intransitive noninterference (INI) in multilevel security systems using discrete event systems (DES). The approach offers a direct way to check INI properties for systems with any number of security levels.
Area of Science:
- Computer Science
- Cybersecurity
- Formal Methods
Background:
- Intransitive noninterference (INI) is crucial for multilevel security systems.
- Previous work established iP-observability for INI verification in systems with up to three security levels.
Purpose of the Study:
- To generalize the verification of intransitive noninterference (INI) for systems with any finite number of security levels.
- To develop a direct algorithmic method for checking iP-observability.
Main Methods:
- Utilizing tools and concepts from discrete event systems (DES).
- Developing a direct method for checking iP-observability based on the left congruence property of the iP function on formal languages.
- Applying the method to detect denial of service vulnerabilities in security protocols.
Main Results:
- A generalized algorithm for verifying INI in systems with multiple security levels.
- Demonstrated applicability through the detection of denial of service vulnerabilities in TCP/IP protocols.
Conclusions:
- The proposed method provides a direct and generalized approach to INI verification.
- Extends the theory of supervisory control of DES to a new application domain in cybersecurity.