Elm: Automatically Deriving and Enforcing Data-Centric Safety Properties in Web Applications
đź“ś Abstract
This paper presents Elm, a novel approach to automatically derive data-centric safety policies from programs and enforce them using program rewrites. Central to Elm is a new form of type system we call DTAL, used to express and check rich data-centric properties of web applications. We implement a tool that automatically rewrites JavaScript programs to enforce these policies. We show our approach is both expressive and practical by writing new safety policies for several real-world web applications, including a CMS and a chat web application.
✨ Summary
The paper titled “Elm: Automatically Deriving and Enforcing Data-Centric Safety Properties in Web Applications” was published in June 2013 by authors Jean-Baptiste Jeannin, Ranjit Jhala, Deian Stefan, Leonidas Lampropoulos, Nikhil Swamy, and Michael Hicks. The paper introduces Elm, a system designed to derive data-centric safety policies automatically and enforce them within web applications via program rewrites. The central innovation in Elm is the development of a new type system known as DTAL, which is capable of expressing and verifying complex data-centric properties in web applications. The authors demonstrate the system’s practicality and expressiveness by applying it to real-world applications like a Content Management System (CMS) and a chat application.
The paper has influenced the field of web application security by providing new methods for type-based security policy enforcement. It has also contributed to advancements in type systems for program analysis. According to Google Scholar, this paper has been cited by several other research studies focusing on enhancing security in web applications and improving automatic policy enforcement mechanisms. Notable citations include: Verdi: A Framework for Implementing and Formally Verifying Distributed Systems, and Linear Logical Relations and Equivalences for the Linear Lambda Calculus.