The aspect-oriented programming paradigm provides an elegant way of modularizing crosscutting concerns of a software system. A crosscutting concern is one whose implementation is scattered throughout the implementation of many other concerns within the software. A modular unit that implements a crosscutting concern is an aspect. In addition to providing the behavior (implementation) for a crosscutting concern (known as advice), an aspect also encapsulates pointcuts that describe locations in the rest of the software where the aspect’s behavior should be integrated. Pointcuts do not refer to locations explicitly, but rather specify how such locations can be identified and selected. The locations where an aspect should be integrated are known as join points. Security is one such crosscutting concern that is encoded using aspects.

This paper explores bugs that creep in when multiple pointcuts in an aspect-oriented security policy provide conflicting advice for a shared join point, a phenomenon called pointcut nondeterminism. These bugs are hard to detect during unit testing, as they may only manifest under unusual circumstances. Jones and Hamlen present and evaluate an algorithm written using constraint-based Prolog, which they show to be invaluable in detecting such hard-to-find bugs.

The authors first provide a background on Security Policy Extensible Markup Language (SPoX), a declarative aspect-oriented specification language, which is the target of their analysis algorithm. Then, they provide a formalism for SPoX security policy nondeterminism. The analysis algorithm uses this formalism to identify pointcut nondeterminism.

Verifying correct security policy specification in general is difficult. The algorithm developed is limited to security policy specifications with purely declarative advice and a pointcut language that includes declarative predicates. It reduces the problem of detecting policy nondeterminism to some well-known hard problems such as Boolean satisfiability, so scalability of the algorithm is less of an issue, as efficient state-of-the-art Boolean satisfiability solvers that can handle problems with thousands to millions of variables are now available.

The elegance of this paper resides in providing a formalism for verifying critical security properties of a software system where security policies are implemented using a declarative aspect-oriented specification language. Jones and Hamlen provide several case studies where the algorithm based on this formalism proves valuable in detecting undesired nondeterminism in security policies of real-life systems.