Web Application Frameworks, such as Google Web Toolkit (GWT) and Rails are being widely used nowadays because of numerous advantages they offer their users. A growing concern is whether such tools introduce security vulnerabilities during the translations they perform. Translation validation is an approach that allows one to verify the correctness of a translation rather than that of a translator. The input to translation validation is a source and target code (before and after translation), and the output is a set of verification conditions (VCs) that establish the semantic correctness of the translation. The VCs are automatically generated and can be charged to independent theorem provers. Translations validations had been successfully applied to optimizing compilers and to backward compatibility of microcode. The work is a preliminary feasibility study of applying translation validation to verifying that frameworks do not introduce security vulnerabilities. The focus is GWT's translations from Java into JavaScript. The project's goal is to develop automatic tools that given a source and target code, as well as a suitably encoded list of security vulnerabilities, automatically generates VCs that, in aggregate, prove that the target does not have any of the security vulnerabilities from the list that do not exist in the source code. A successful completion of this feasibility study will allow for the development of methodologies and tools for automatic and formal proofs that frameworks do not introduce security vulnerabilities that will be of interest to web developers as well as to industry.
EAGER: From Devlopment Tools to Secure Web Applications