An Epistemic Formulation of Information Flow Security

The non-interference (NI) property defines a program to be secure if changes to high-security inputs cannot alter the values of low-security outputs. NI indirectly states the epistemic property that no low-security principal acquires knowledge of high-security data. We consider a directly epistemic account of information flow (IF) security focusing on the knowledge flows engendered by the pro-gram’s execution. Storage effects are of primary interest, since prin-cipals acquire knowledge from the execution only through these ef-fects. The IF properties of the individual effectful actions are char-acterized using a substructural epistemic logic that accounts for the knowledge transferred through their execution. We prove that a low-security principal never acquires knowledge of a high-security input by executing a well-typed program. The epistemic approach has several advantages over NI. First, it directly accounts for the knowledge flow engendered by a pro-gram. Second, in contrast to the bimodal NI property, the epistemic approach accounts for authorized declassification. We prove that a low-security principal acquires knowledge of a high-security input only if it is authorized by a proof in authorization logic. Third, the explicit formulation of IF properties as an epistemic theory pro-vides a crisp treatment of “side channels. ” Rather than prove that a principal does not know a secret, we instead prove that it is not provable that the principal knows that secret. The latter statement characterizes the “minimal model, ” for which a precise statement may be made, whereas the former applies to “any model, ” including those with “side channels ” that violate the model’s basic premises. Fourth, the NI property is re-positioned as providing an adequacy proof of the epistemic theory of effects, ensuring that the logical theory corresponds to the actual program behavior. In this way we obtain a generalization of the classical approach to IF security that extends to authorized declassification. Categories and Subject Descriptors CR-number [subcategory]: third-leve