Information Flow Monitor Inlining

In recent years it has been shown that dynamic monitoring can be used to soundly enforce information flow policies. For programs distributed in source or bytecode form, the use of just-in-time (JIT) compilation makes it difficult to implement monitoring by modifying the language runtime system. An inliner avoids this problem and also serves to provide monitoring for more than one runtime. We show how to inline an information flow monitor, specifically a flow sensitive one previously proved to enforce termination insensitive noninterference. We prove that the inlined version is observationally equivalent to the original.

I. Introduction

Many security requirements involve information flow. Many practical security measures involve runtime mechanisms – but it was long thought that information flow requires static enforcement mechanisms because it is not a trace property [29], [9] and runtime monitoring enforces trace properties [35]. Hamlen et al [22] show that any property that can be statically analyzed can also be checked by a runtime monitor with access to the program source. Le Guernic et al. [20] confirm this for an information flow monitor that performs some static analysis. They suggest that their security automaton could be implemented by program transformation. Subsequent work has explored dynamic information flow monitoring, but not by transformation. In this paper, we argue that, for web applications, inlining is the only way to go, and we show how to prove an inlining transformation correct.