A Progress-Sensitive Flow-Sensitive Inlined Information-Flow Control Monitor
Andrew Bedford, Stephen Chong, Josèe Desharnais, and Nadia Tawbi
Proceedings of the 31st IFIP TC 11 International Information Security and Privacy Conference (IFIP SEC), pages 352–366, May 2016.

We present a novel progress-sensitive, flow-sensitive hybrid information-flow control monitor for an imperative interactive language. Progress-sensitive information-flow control is a strong information security guarantee which ensures that a program’s progress (or lack of) does not leak information. Flow-sensitivity means that this strong security guarantee is enforced fairly precisely: we track information flow according to the source of information and not to an a priori given variable security level. We illustrate our approach on an imperative interactive language. Our hybrid monitor is inlined: source programs are translated, by a type-based analysis, into a target language that supports dynamic security levels. A key benefit of this is that the resulting monitored program is amenable to standard optimization techniques such as partial evaluation.