Many interesting security properties are history-dependent; however, currently deployed pointcut languages cannot express history-sensitivity. (Mechanisms like cflow in AspectJ capture only the current call stack.) We present a language of pointcuts with past-time temporal operators and discuss their implementation using a variant of security automata. The main result is a proof that the implementation is correct.

AOP is usually presented as an extension of an underlying computational mechanism, but the extension is in no sense conservative. For program analysis, this is in some sense this is the worst of both worlds. We adopt a different approach: refining our earlier work, we de ne a minimal language of events and aspects in which everything is an aspect. The minimalist approach serves to clarify the issues and may be of independent interest.