"Soundly Extending the Scope of a Security Analysis for Java by Program Rewriting"

Abstract:
Traditionally, type-based approaches to static information flow analysis 
operate on a generic simplified imperative programing language or a 
subset of a practically used language. While the end user of an analysis 
would wish for it to be directly applicable to a working program, the 
developers of the analysis prefer to restrict the complexity of inputs 
in order to keep the analysis easily modifiable and formally verifiable. 
A possible solution is the transformation of full programs into 
semantically equivalent programs in a language or subset of a language 
supported by the analysis. This presentation describes us exploring the 
practicality of this approach by extending the scope of the Adele static 
code analysis tool via the rewriting of Java code containing unsupported 
loops to only contain the supported while loop.