On the Decidability of Model-Checking Information Flow Properties

Current standard security practices do not provide substan- tial assurance about information flow security: the end-to-end behav- ior of a computing system. Noninterference is the basic semantical con- dition used to account for information flow security. In the literature, there are many definitions of noninterference: Non-inference, Separabil- ity and so on. Mantel presented a framework of Basic Security Predicates (BSPs) for characterizing the definitions of noninterference in the litera- ture. Model-checking these BSPs for finite state systems was shown to be decidable in (4). In this paper, we show that verifying these BSPs for the more expressive system model of pushdown systems is undecidable. We also give an example of a simple security property which is undecidable even for finite-state systems: the property is a weak form of non-inference called WNI, which is not expressible in Mantel’s BSP framework.