EAGER: From Devlopment Tools to Secure Web Applications

Web应用程序框架，如Google Web工具包(GWT)和Rails，如今正被广泛使用，因为它们为用户提供了许多优势。一个日益令人担忧的问题是，这些工具是否会在它们执行的转换过程中引入安全漏洞。翻译验证是一种允许人们验证翻译的正确性而不是译者的正确性的方法。翻译验证的输入是源代码和目标代码(翻译前和翻译后)，输出是一组验证条件(VC)，这些条件建立了翻译的语义正确性。风投是自动生成的，可以向独立的定理证明者收费。翻译验证已成功地应用于优化编译器和微码的向后兼容性。这项工作是应用翻译验证来验证框架没有引入安全漏洞的初步可行性研究。重点是GWT从Java到Java的翻译。该项目的目标是开发自动工具，在给定源代码和目标代码以及适当编码的安全漏洞列表的情况下，自动生成VC，这些VC聚合在一起证明目标没有源代码中不存在的列表中的任何安全漏洞。这项可行性研究的成功完成将有助于开发方法和工具，以自动和正式地证明框架不会引入网络开发人员以及工业界感兴趣的安全漏洞。

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.