Complexity and Unwinding for Intransitive Noninterference
This work addresses the problem of efficiently verifying information flow security for researchers and practitioners in computer security, providing concrete complexity results and improved bounds.
The paper analyzes the computational complexity of verifying several intransitive noninterference security definitions for finite-state systems, finding that checking P-security, IP-security, and TA-security is in PTIME, while TO-security and ITO-security are undecidable.
The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable, as is checking ITO-security (van der Meyden). The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also lead to new unwinding proof techniques that are shown to be sound and complete for these notions of security, and enable the algorithms to return simple counter-examples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.