Cross-tier, Label-based Security Enforcement for Web Applications
Brian J. Corcoran, Nikhil Swamy, and Michael Hicks
In Proceedings of the ACM SIGMOD International Conference on Management of Data, June 2009.
[ abstract |
pdf |
bib ]
This paper presents SELinks, a programming language focused on
building secure multi-tier web applications. SELinks provides a
uniform programming model, in the style of LINQ and Ruby on Rails,
with language syntax for accessing objects residing either in the
database or at the server. Object-level security policies are
expressed as fully-customizable, first-class labels which may
themselves be subject to security policies. Access to labeled data is
mediated via trusted, user-provided policy enforcement
functions.
SELinks has two novel features that ensure security policies are
enforced correctly and efficiently. First, SELinks implements a type
system called Fable that allows a protected object's type to refer to
its protecting label. The type system can check that labeled data is
never accessed directly by the program without first consulting the
appropriate policy enforcement function. Second, SELinks compiles
policy enforcement code to database-resident user-defined functions
that can be called directly during query processing. Database-side
checking avoids transferring data to the server needlessly, while
still allowing policies to be expressed in a customizable and portable
manner.
Our experience with two sizable web applications, a model health-care
database and a secure wiki with fine-grained security policies,
indicates that cross-tier policy enforcement in SELinks is flexible,
relatively easy to use, and, when compared to a single-tier approach,
improves throughput by nearly an order of magnitude. SELinks is
freely available.
@INPROCEEDINGS{corcoran09selinks,
AUTHOR = {Brian J. Corcoran and Nikhil Swamy and Michael Hicks},
TITLE = {Cross-tier, Labeld-based Secuirty Enforcement for Web Applications},
BOOKTITLE = {Proceedings of the {ACM SIGMOD} International Conference on Management of Data},
MONTH = JUNE,
YEAR = 2009,
NOTE = {To appear}
}
Fable: A Language for Enforcing User-defined Security Policies
Nikhil Swamy, Brian J. Corcoran, and Michael Hicks
In Proceedings of the IEEE Symposium on Security and Privacy
(Oakland), May 2008.
[ abstract |
pdf |
tr.pdf |
bib ]
This paper presents Fable, a core formalism for a programming language
in which programmers may specify security policies and reason that
these policies are properly enforced. In Fable,
security policies can be expressed by associating security
labels with the data or actions they protect. Programmers define the
semantics of labels in a separate part of the program called the
enforcement policy. Fable prevents a policy from being circumvented
by allowing labeled terms to be manipulated only within the enforcement
policy; application code must treat labeled values abstractly.
Together, these features
facilitate straightforward proofs that programs implementing a
particular policy achieve their high-level security goals. Fable is
flexible enough to implement a wide variety of security policies,
including access control, information flow, provenance, and security
automata.
We have implemented Fable as part of the Links web
programming language; we call the resulting language SELinks. We
report on our experience using SElinks to build two substantial
applications, a wiki and an on-line store, equipped with a combination of
access control and provenance policies.
To our knowledge, no existing framework enables
the enforcement of such a wide variety of security policies with an
equally high level of assurance.
@INPROCEEDINGS{swamy08fable,
AUTHOR = {Nikhil Swamy and Brian J. Corcoran and Michael Hicks},
TITLE = {Fable: A Language for Enforcing User-defined Security Policies},
BOOKTITLE = {Proceedings of the {IEEE} Symposium on Security and Privacy (Oakland)},
MONTH = MAY,
YEAR = 2008,
}
Verified Enforcement of Stateful Information Release Policies
Nikhil Swamy and Michael Hicks
In Proceedings of the ACM SIGPLAN Workshop on Programming Langauges and Analysis for Security, June 2008.
(One of two best papers; selected for publication in SIGPLAN Notices.)
[ abstract |
pdf |
bib |
TR |
Coq proof (partial) ]
Many organizations specify information release policies to
describe the terms under which sensitive information may be released
to other organizations. This paper presents a new approach for
ensuring that security-critical software correctly enforces its
information release policy. Our approach has two parts. First, an
information release policy is specified as a security automaton
written in a new language called AIR. Second, we enforce an AIR
policy by translating it into an API for programs written in LAIR,
a core formalism for a functional programming language. LAIR uses
a novel combination of dependent, affine, and singleton types to
ensure that the API is used correctly. As a consequence we can
certify that programs written in LAIR meet the requirements of
the original AIR policy specification.
@INPROCEEDINGS{swamy08lair,
AUTHOR = {Nikhil Swamy and Michael Hicks},
TITLE = {Verified Enforcement of Stateful Information Release Policies},
MONTH = JUN,
YEAR = 2008,
BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Workshop on Programming Langauges and Analysis for Security (PLAS)},
}
Combining Provenance and Security Policies in a Web-based Document Management System
Brian J. Corcoran, Nikhil Swamy, and Michael Hicks
In On-line Proceedings of the Workshop on Principles of
Provenance (PrOPr), November 2007.
http://homepages.inf.ed.ac.uk/jcheney/propr/.
[ abstract |
pdf |
bib ]
Provenance and security are intimately related. Cheney et
al. show that the dependencies underlying provenance
information also underly information flow security policies. Provenance
information can also play a role in history-based access control
policies. Many real applications have the need to
combine a variety of security policies with provenance tracking. For
instance, an online stock trading website might restrict access to certain
premium features it offers using an access control policy, while at the same
time using an information flow policy to ensure that a user's sensitive
trading information is not leaked to other users. Similarly, the application
might need to track the provenance of transaction information to support an
annual financial audit while also using provenance to attest to the
reliability of stock analyses that it presents to its users.
We have been exploring the interaction between provenance and security
policies while developing a document management system we call the
Collaborative Planning Application (CPA). The CPA is written in
SELinks, our language for supporting user-defined, label-based security
policies. SELinks is an extension of the Links
web-programming language with means to express label-based
security policies. Labels are associated with the data they protect by
using dependent types which, along with some syntactic restrictions, suffice
to ensure that user-defined policies enjoy complete mediation and
cannot be circumvented. Our interest in provenance and
security policies is thus part of a broader exploration of how security
policies can be encoded, composed, and reasoned about within SELinks. In
this paper, we describe the architecture of the CPA and its approach to
label-based provenance and security policies
and we sketch directions for further exploration on the interaction between
the two.
@INPROCEEDINGS{corcoran07provenance,
AUTHOR = {Brian J. Corcoran and Nikhil Swamy and Michael Hicks},
TITLE = {Combining Provenance and Security Policies in a Web-based
Document Management System},
BOOKTITLE = {On-line Proceedings of the Workshop on Principles of Provenance (PrOPr)},
NOTE = {\url{http://homepages.inf.ed.ac.uk/jcheney/propr/}},
LOCATION = {Edinburgh, Scotland, UK},
MONTH = NOV,
YEAR = 2007
}
Verified Enforcement of Security Policies for Cross-Domain Information Flows
Nikhil Swamy, Michael Hicks, and Simon Tsang.
In Proceedings of the 2007 Military Communications Conference
(MILCOM), October 2007.
[ abstract |
pdf |
bib ]
We describe work in progress that uses program analysis to show that
security-critical programs, such as cross-domain guards, correctly
enforce cross-domain security policies.
We are enhancing existing techniques from the field of
security-oriented programming languages to construct a new language
for the construction of secure networked applications, SELinks.
In order to specify and enforce expressive and fine-grained policies,
we advocate dynamically associating security labels with sensitive
entities.
Programs written in SELinks are statically guaranteed to
correctly manipulate an entity's security labels and to ensure that
the appropriate policy checks mediate all operations that are
performed on the entity.
We discuss the design of our main case study: a web-based
collaborative planning application that will permit a collection
of users, with varying security requirements and clearances, to access
sensitive data sources and collaboratively create documents based on
these sources.
@INPROCEEDINGS{swamy07milcom,
AUTHOR = {Nikhil Swamy and Michael Hicks and Simon Tsang},
TITLE = {Verified Enforcement of Security Policies for Cross-Domain
Information Flows},
MONTH = OCT,
YEAR = 2007,
BOOKTITLE = {Proceedings of the 2007 Military Communications Conference (MILCOM)}
}
|