IFC

Are fine-grained and coarse-grained dynamic information flow control always equally expressive?

In this work, we lift two technical assumptions that stand out among the details of Vassena et al.’s translation. First, the security property for which the equivalence is formally established is termination-insensitive noninterference. Second, both coarse and fine-grained languages are statically typed in a standard (security unaware) way. We derive a novel 2-labeled fine-grained dynamic IFC system, for which we have not found a semantics-preserving approach that is idiomatically coarse-grained. We conjecture that 2-labeled (and generally n-labeled) fine grained monitors unveil an expressiveness gap between the fine-grained and the coarse-grained approaches to dynamic IFC.

Retrofitting Impure Languages with Static Information-Flow Control

How can we write secure programs in a pervasively effectful language? In a “pure” language, such as Haskell, effects performed by a program are recorded explicitly in its type. Thus, a function of type Int - Int is just that: a function that receives an integer and returns an integer. It does not perform side effects such as writing to or reading from a channel. In an impure language, such as ML, however, a function of type Int - Int may read, write, or even order a burrito. It’s impossible to assert that a function is secure from its type alone, since it may be performing invisible side effects that may leak a secret.