AuraConf
Jeffrey A. Vaughan · 2011
This paper introduces AuraConf, the first programming language with a unified means to specify access-control and confidentially policies. In concert with a proof-carrying access control mechanism, to known-techniques for describing access-control, AuraConf allows confidentially policies to be specified declaratively using types and enforced via cryptography. Programs written in AuraConf enjoy a formal security guarantee via noninterference. Additionally, the language definition introduces a novel type system where the typechecker may use resources (i.e., private keys) and knowledge of an object's provenance (i.e., how a ciphertext was computed) to guide analysis.