2018-01-08
286
The starting point in secure information flow analysis is the classification of program variables into different security levels. The most basic distinction is to classify some variables as L, meaning low security, public information; and other variables as H, meaning high security, private information. The security goal is to prevent information in H variables from being leaked improperly.Such leaks could take a variety of forms, of course, but certainly we need to prevent information in H variables from flowing to L variables.More generally, we might want a lattice of security levels, and we would wish to ensure that information flows only upwards in the lattice.For example, if L ≤ H, then we would allow flows from L to L, from H to H, and from L to H, but we would disallow flows from H to L.
Definition 1 (Noninterference). Program c satisfies noninterference if, for any memories μand v that agree on L variables, the memories produced by running c on μand on v also agree on L variables (provided that both runs terminate successfully).
Lemma 1 (Simple Security). If Гsubsumpe: t, then e contains only variables of level _ or lower.
Lemma 2 (Confinement). If Гsubsumpc: t cmd, then c assigns only to variables of level _ or higher.
We might generalize to a possibilistic noninterference property that says that changing the initial values of H variables cannot change the set of possible final values of L variables:
Definition 2 (Possibilistic Noninterference). Program c satisfies possi-
bilistic noninterference if, for any memories μand v that agree on L variables,if running c on μcan produce final memory μ′, then running c on v can produce a final memory v′ such that μ′ and v′ agree on L variables.
Secure information flow analysis has the potential to guarantee strong security properties in computer software. But if it is to become broadly useful, it must better address the security properties that are important in practice.
