Back to Search Start Over

History-Based Access Control and Secure Information Flow.

Authors :
Barthe, Gilles
Burdy, Lilian
Huisman, Marieke
Lanet, Jean-Louis
Muntean, Traian
Banerjee, Anindya
Naumann, David A.
Source :
Construction & Analysis of Safe, Secure & Interoperable Smart Devices; 2005, p27-48, 22p
Publication Year :
2005

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. [ABSTRACT FROM AUTHOR]

Details

Language :
English
ISBNs :
9783540242871
Database :
Supplemental Index
Journal :
Construction & Analysis of Safe, Secure & Interoperable Smart Devices
Publication Type :
Book
Accession number :
32976110