Computer Sciences Seminar
Friday, April 16, 2004
11:30 AM, NAC 8/206

Access control mechanisms are often used with the intent of enforcing confidentiality and integrity policies, but few rigorous connections have been made between information flow and runtime access control. The Java virtual machine and the .NET runtime system provide a dynamic access control mechanism in which permissions are granted to program units and a runtime mechanism checks permissions of code in the calling chain. We investigate a design pattern by which this mechanism can be used to achieve confidentiality and integrity goals: a single interface serves callers of more than one security level and dynamic access control prevents release of high information to low callers. Programs fitting this pattern would be rejected by previous flow analyses. We give a static analysis that admits them, using permission-dependent security types. The analysis is given for a class-based object-oriented language with features including inheritance, dynamic binding, dynamically allocated mutable objects, type casts and recursive types. The analysis is shown to ensure a noninterference property formalizing confidentiality and integrity.

(Joint work with David A. Naumann, Stevens Institute of Technology)

Bio:

Anindya Banerjee is Associate Professor in the Department of Computing and Information Sciences at Kansas State University.

His research interests are in computer security where he is interested in using techniques from program analysis to verify security properties.

Dr. Banerjee earned his PhD in Computing and Information Sciences at Kansas State University, and was subsequently a postdoctoral fellow at the Ecole Polytechnique, Paris and a research assistant professor at the University of Aarhus, Denmark.

He was an assistant professor at the Stevens Institute of Technology from 1997-2001 and received the NSF Career Award in 2000.