History-based access control and secure information flow

Anindya Banerjee, David A. Naumann

Research output: Contribution to journalConference articlepeer-review

30 Scopus citations

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.

Original languageEnglish
Pages (from-to)27-48
Number of pages22
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3362
DOIs
StatePublished - 2005
EventInternational Workshop, CASSIS 2004 - Marseille, France
Duration: 10 Mar 200414 Mar 2004

Fingerprint

Dive into the research topics of 'History-based access control and secure information flow'. Together they form a unique fingerprint.

Cite this