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

  • Nikhil Swamy | University of Maryland

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.

Speaker Details

Nikhil Swamy is a Ph.D. candidate enrolled at the University of Maryland, College Park since 2002. He is a member of the Programming Languages Group at UMD and is advised by Prof. Michael Hicks. He earned his B.A. from Hampshire College in 2000 and his M.S. from UMD in 2005. In addition to security, his research interests include type systems, program analysis and interactive theorem proving.

Watch Next