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.
Our findings answer two questions. First, to what extent do existing, industrial-grade web development frameworks eliminate security vulnerabilities from web applications? The short answer is ``very little". Second, how can we either augment existing frameworks or design new frameworks to automatically eliminate security vulnerabilities? Existing Industrial Frameworks We explored two different web development frameworks chosen because of their popularity and the general perception that they were designed to help developers build secure web applications: the Google Web Toolkit (GWT) and Ruby on Rails (RoR) . We discovered is that frameworks today usually automate simple tasks that have little impact on the security of the web application. They effectively save the developer (a sometimes significant amount of) typing but provide no help in terms of avoiding well-known security vulnerabilities on the web, e.g., SQL injection or cross-site scripting. In summary, GWT makes it easier for developers to build applications because it provides the illusion of a single programming language for the client and server. Arguably, GWT applications are more secure because developers can more quickly build their application and have more time and energy to harden it against well-known attacks, but the framework itself offers no help in ensuring applications are free from common web application vulnerabilities. RoR exemplifies the Model-View-Controller (MVC) approach to web application development. Models represent the application's data and protects that data against inconsistency. Roughly, the Models of a web application correspond to the tables in the back-end database. Views display the application's data in different ways and correspond to the web pages of an application. Controllers dictate how user requests change the Models (the database) and how those requests are responded to with Views (web pages). Unlike GWT, which endeavors to provide a single programming language for the entire application, RoR utilizes different languages for different components of the application. Models and Controllers are both written in Ruby, and Views are written in a number of languages: Ruby, HTML, CoffeeScript, JavaScript. And unlike GWT, which encourages the developer to think of the web application as a single Java program, RoR requires the developer to constantly think about the separation of the client and server as well as how they will be communicating. There is built-in support to simplify AJAX requests; however, the developer must insert that AJAX-specific code. RoR provides developers i a plethora of cookie-cutter solutions to common problems, an underlying programming language that encompasses some of the most tried and true ideas for dynamic programming languages from the past 50 years, and a rich library of web-specific algorithms. It is a framework designed specifically for web application development, has a vibrant ecosystem, and is open source. Rails applications are not innately secure; rather, Rails provides developers with a number of basic routines known to mitigate security attacks effectively. These routines must be applied appropriately and consistently or else security vulnerabilities will exist. In short, the RoR Security Guide provides a great deal of helpful and practical information about avoiding security vulnerabilities but leaves it to the developer to follow that advice. Having found that industrial frameworks provide few if any security guarantees, we decided to both extend an existing framework and create a new framework that by construction would eliminate common security vulnerabilities in web applications. In the first thrust of this project, we aimed to improve the security of the Ruby on Rails web development framework by adding mechanisms that would enable strong security guarantees for one particular class of vulnerabilities. In the second thrust of the project, we designed and implemented a clean-slate approach to web development where every application is by construction safe from some of the most prevalent vulnerabilities on the web today. We improve the security of the Ruby on Rails web development framework by automatically extracting data validation code from the server and replicating it on the client. We identified a fragment of RoR that can be soundly and completely replicated on the client and evaluated how prevalent validators written in this fragment are in the wild. The problem with augmenting an existing framework is that developers can ignore that augmentation, write the same applications, and produce code with all the same vulnerabilities. It is therefore often difficult to achieve the kinds of security guarantees we might like unless we design a new web development framework that stops developers from making the same mistakes as with traditional frameworks. Weblog is a new web development framework designed primarily to ensure all its applications can be soundly, completely, and automatically protected against some of the most common web security vulnerabilities today. We developed Weblog so that allows in-design security against SQL injections, XSS attacks, Parameter Tampering attacks, and Access Control attacks. We evaluated the performance of Weblog, as well as developed some ``real life" applications with it.
