Access control mechanisms are widely used with the intent of enforcing confidentiality and other policies, but few formal connections have been made between information flow and access control. Java and C are object-oriented languages that provide fine-grained access control. An access control list specifies local policy by authorizing permissions for principals (code sources) associated with class declarations; a mechanism called stack inspection checks permissions at run time. An example is given to show how this mechanism can be used to achieve confidentiality goals in situations where a single system call serves callers of differing confidentiality levels and dynamic access control prevents release of high information to low callers. A novel static analysis is given which applies to such examples. The analysis is shown to ensure a noninterference property formalizing confidentiality.
Anindya Banerjee, David A. Naumann