TY - JOUR
T1 - History-based access control and secure information flow
AU - Banerjee, Anindya
AU - Naumann, David A.
PY - 2005
Y1 - 2005
N2 - This paper addresses the problem of static checking of programs to ensure that they satisfy confidentiality policies in the presence of dynamic access control in the form of Abadi and Fournet's history-based access control mechanism. The Java virtual machine's permission-based stack inspection mechanism provides dynamic access control and is useful in protecting trusted callees from untrusted callers. In contrast, history-based access control provides a stateful view of permissions: permissions after execution are at most the permissions before execution. This allows protection of both callers and callees. The main contributions of this paper are to provide a semantics for history-based access control and a static analysis for confidentiality that takes history-based access control into account. The static analysis is a type and effects analysis where the chief novelty is the use of security types dependent on permission state. We also show that in contrast to stack inspection, confidential information can be leaked by the history-based access control mechanism itself. The analysis ensures a noninterference property formalizing confidentiality.
AB - This paper addresses the problem of static checking of programs to ensure that they satisfy confidentiality policies in the presence of dynamic access control in the form of Abadi and Fournet's history-based access control mechanism. The Java virtual machine's permission-based stack inspection mechanism provides dynamic access control and is useful in protecting trusted callees from untrusted callers. In contrast, history-based access control provides a stateful view of permissions: permissions after execution are at most the permissions before execution. This allows protection of both callers and callees. The main contributions of this paper are to provide a semantics for history-based access control and a static analysis for confidentiality that takes history-based access control into account. The static analysis is a type and effects analysis where the chief novelty is the use of security types dependent on permission state. We also show that in contrast to stack inspection, confidential information can be leaked by the history-based access control mechanism itself. The analysis ensures a noninterference property formalizing confidentiality.
UR - http://www.scopus.com/inward/record.url?scp=24144435318&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=24144435318&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-30569-9_2
DO - 10.1007/978-3-540-30569-9_2
M3 - Conference article
AN - SCOPUS:24144435318
SN - 0302-9743
VL - 3362
SP - 27
EP - 48
JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
T2 - International Workshop, CASSIS 2004
Y2 - 10 March 2004 through 14 March 2004
ER -