TY - JOUR
T1 - Stack-based access control and secure information flow
AU - Banerjee, Anindya
AU - Naumann, David A.
PY - 2005/3
Y1 - 2005/3
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=17044429386&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=17044429386&partnerID=8YFLogxK
U2 - 10.1017/S0956796804005453
DO - 10.1017/S0956796804005453
M3 - Article
AN - SCOPUS:17044429386
SN - 0956-7968
VL - 15
SP - 131
EP - 177
JO - Journal of Functional Programming
JF - Journal of Functional Programming
IS - 2
ER -