A logical analysis of authorized and prohibited information flows

In reasoning about security policy based on information flow control, two different points of view can be adopted depending on whether explicit permissions or explicit prohibitions are being dealt with. In both cases, an epistemic and deontic logic is used to formally define information a subject is permitted to know. Then it is shown that the causality property can be derived from the explicit permissions point of view and that the noninterference and non-deducibility properties can be derived from the explicit prohibition point of view. However, it is argued that the prohibitions enforced by non-interference or non-deducibility are generally too rigid and lead to too strong security properties. On the other hand, the causality properly only handles internal information flow controls and it must be completed to ensure that the security policy is consistently defined. Hence, the consistency problem is discussed. A general definition and practical conditions are proposed to verify that a security policy is consistent