2005 | OriginalPaper | Buchkapitel
History-Based Access Control with Local Policies
verfasst von : Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari
Erschienen in: Foundations of Software Science and Computational Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
An extension of the
λ
-calculus is proposed, to study history-based access control. It allows for security policies with a possibly nested, local scope. We define a type and effect system that, given a program, extracts a history expression, i.e. a correct approximation to the set of histories obtainable at run-time. Validity of history expressions is non-regular, because the scope of policies can be nested. Nevertheless, a transformation of history expressions is presented, that makes verification possible through standard model checking techniques. A program will never fail at run-time if its history expression, extracted at compile-time, is valid.