Do As I SaY! Programmatic Access Control with Explicit Identities

We address the programmatic realization of the access control model of security in distributed systems. Our aim is e the gap between abstract/declarative policies and their concrete/operational implementations. We present a programming formalism (which extends the asynchronous pi-calculus with explicit principals) and a specification logic (which extends Datalog with primitives from authorization logic). We provide two kinds of static analysis methods to tie implementation to specification. Type checking determines that a program is a sound implementation of policy; i.e., that all granted accesses are safe in the face of arbitrary opponents. Model checking determines a degree of completeness; i.e., that accesses permitted by the policy are actually granted in the implementation.

• Type: Conference
• Year: 2007
• Where: CSFW
• Authors: Andrew Cirillo, Radha Jagadeesan, Corin Pitcher, James Riely
• Keywords: Access Control Model, Checking Determines, CSFW 2007, Security Privacy, Type Checking Determines