End-to-end Security for Web Applications : A Language-based Approach

Опубликовано 6 сентября 2016, 17:09

Most large organizations must maintain a substantial information presence on the world wide web in order to share information with their partners and customers. For instance, the United States military has begun using Intellipedia, a wiki-based online document management system, in order to promote information sharing between the sixteen agencies that comprise the U.S. intelligence community. Among other security requirements, such an application should only allow authorized users to access sensitive portions of a document, it should track the provenance of data in each document and it should ensure that information releases follow a specific downgrading protocol. Web-specific threats, like script injection attacks, must also be thwarted if critical data like authentication tokens are to be protected. A framework that ensures that such a wide range of security concerns is correctly addressed is highly desirable but, to date, no such framework exists. In this talk, I present SELinks, an extension of the Links programming language in which web applications can be shown to correctly enforce a wide variety of security policies end to end. In SELinks, a programmer specifies a custom security policy by associating security labels with sensitive operations and data. SELinks prevents a policy from being circumvented by allowing labeled terms to be manipulated only within a separate part of the program called the enforcement policy; application code must treat labeled values abstractly. SELinks is also equipped with support for policies that protect users running a specially modified browser from script injection attacks. We have used SELinks to build two substantial applications, including a secure online document management system. Our initial experience indicates that it is relatively easy to correctly enforce many common policies in SELinks and, using a formal model, to prove that correct enforcement entails the fulfillment of high-level security objectives.