[Pl-seminar] PL seminar schedule

[Aaron Turon]

NEU Programming Languages Seminar presents

Jeff Vaughan
Harvard University

Wednesday, Feb 17, 2010
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Title: Aura: Programming with Authorization and Audit

Abstract: Standard programming models do not provide direct ways of
managing secret or untrusted data. This is a problem because
programmers must use ad hoc methods to ensure that secrets are not
leaked and, conversely, that tainted data is not used to make critical
decisions. This talk will advocate integrating cryptography and
language-based analyses in order to build programming environments for
declarative information security, in which high-level specifications
of confidentiality and integrity constraints are automatically
enforced in hostile execution environments.

I will introduce describes Aura, a family of programing languages,
which integrate functional programming, access control via
authorization logic, automatic audit logging, and confidentially via
encryption. Aura’s programming model marries an expressive, principled
way to specify security policies with a practical policy-enforcement
methodology that is well-suited for auditing access grants and
protecting secrets.

Aura security policies are expressed as propositions in an
authorization logic. Such logics are suitable for discussing
delegation, permission, and other security-relevant concepts. Aura’s
(dependent) type system cleanly integrates standard data types, like
integers, with proofs of authorization-logic propositions; this lets
programs manipulate authorization proofs just like ordinary values. In
addition, security-relevant implementation details—like the creation
of audit trails or the cryptographic representation of language
constructs—can be handled automatically with little or no programmer
intervention.