Скачать или смотреть "Aura: Programming with Authorization and Audit" (CRCS Lunch Seminar)

CRCS Lunch Seminar (Monday, November 2, 2009)

Speaker: Jeff Vaughan, Harvard CRCS

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.

Bio: Jeff Vaughan's research lies at the intersection of computer security, programming languages, and formal methods. He is particularly interested in access control, information flow, the theory and application of dependent types, and mechanized metatheory. Jeff will be receiving his PhD from the University of Pennsylvania.