History-based access control and secure information flow

Abstract

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. © Springer-Verlag Berlin Heidelberg 2005.