Information Flow Monitor Inlining

Date Added: Feb 2010
Format: PDF

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 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. The authors show how to inline an information flow monitor, specifically a flow sensitive one previously proved to enforce termination insensitive noninterference. They prove that the inlined version is observationally equivalent to the original.