Checking Risky Events Is Enough for Local Policies

Abstract. An extension of the λ-calculus is proposed to study historybased access control. It allows for parametrized security policies with a possibly nested, local scope. To govern the rich interplay between local policies, we propose a combination of static analysis and dynamic checking. A type and effect system extracts from programs a correct approximation to the histories obtainable at run-time. A further static analysis over these approximations determines how to instrument code so to enforce the desired security constraints. The execution monitor, based on finite-state automata, runs efficiently the instrumented code.

• Type: Conference
• Year: 2005
• Where: ICTCS
• Authors: Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari
• Keywords: Historybased Access Control, ICTCS 2005, Parametrized Security Policies, Static Analysis