Section 9.4. DETECTION AND RESOLUTION OF ASPECT INTERACTIONS

9.4. DETECTION AND RESOLUTION OF ASPECT INTERACTIONS

By restricting the expressiveness of our aspect language (while still adhering to stateful aspects), it is possible to automatically prove (certain) aspect properties. In this section, we consider a second instantiation of the general framework that supports a more restrictive yet expressive crosscut language in which static checking of interactions is feasible.

Crosscuts A crosscut is defined by conjunctions, disjunctions, and negations of terms

C ::= T | C₁ and C₂ | C₁ or C₂ | not C

where T denotes terms with variables. The formulas used to express these crosscuts belong to the so-called quantifier-free equational formulas [5]. Whether such a formula has a solution is decidable. This is one of the key properties making the analysis in this section feasible.

We can define, for example, a crosscut matching logins performed by the user root on any machine, or by any non-root user on any machine but the server as follows:

login(root, m) or (login(u,m) and (not login(u, server)))

In this context, checking whether the current join point (which, remember, is represented by a term) matches the crosscut definition is computed by a generalized version of the unification algorithm that is well-known, e.g., from logic programming.

Note that, for the sake of decidability (i.e., static analyses), the crosscuts C defined by the equation above are less expressive than those considered in the previous section. They can only denote join points as term patterns (as opposed to arbitrary term predicates).

Stateful aspects. The main idea of the aspect language presented in this section is to restrict stateful aspects to regular expressions using the following grammar:

A ::= C  A            ; sequence
   | C  var           ; end of sequence
   | A₁  Using this aspect language a security aspect logAccess that logs file accesses (calls to read) from a call to login until a call to logout (assuming non-nested sessions) can be expressed as

logAccess = login(u, m)  skip ; logRead = (logout()  skip ;  (read( addLog(logRead)

where x matches the name of the accessed file.

9.4.1. Aspect Interactions

Remember that a parallel composition of n aspects A₁ ||...|| A_n does not define any specific order of aspect application; the result of weaving may be non-deterministic. This situation arises when aspects interact, that is to say when at least two inserts must be executed at the same join point. For instance, consider the following aspect:

cryptRead = read(x)  crypt(cryptRead

This aspect states that the reads should be encrypted. It interacts with the aspect logAccess defined previously, which describes logging for all users. When a user logs in and accesses a file, this access must be logged, and the file name must be encrypted.

The algorithm to check aspects interaction is similar to the algorithm for finite-state product automata. It terminates due to the finite-state nature of our aspects. Starting with a composition A || A", the algorithm eliminates the parallel operator by producing all the possible pairs (conjunction) of crosscuts from A and A". A conjunction of crosscuts C₁ and C₂ is a solvable formula, and we can check if it has a solution using the algorithm of [5]. A crosscut with no solution cannot match any join point and can be removed from the aspect [7]. In the case of the example logAccess || cryptRead, we get:

logccess || cryptRead
         = login(u, m)  skip ;  read( crypt(logAccess || cryptRead
logCrypt = logout()  skip ;  read( (addLog( crypt(logCrypt

Conflicts are represented using the non-deterministic function (I₁ I₁ ; I₂ or I₂ ; I₁. Here, we have (addLog(x) crypt(
(I  skip) = (skip  I.

This analysis does not depend on the base program to be woven. When there is no () in the resulting sequential aspect, the two aspects are independent for all programs. This property does not have to be checked again after any program modification. However, this property is a sufficient but not a necessary condition for aspect interaction. A more precise analysis is possible by taking into account the possible sequences of join points generated by the base program to be woven [7].

9.4.2. Support for Conflict Resolution

When no conflicts have been detected, the parallel composition of aspects can be woven without modification. Otherwise, the programmer must get rid of the nondeterminism by making the composition more precise. In the following, we present some linguistic support aimed at resolving interactions.

The occurrences of rules of the form C C C C I₃ is a new insert that combines I₁ and I₂ in some way. For instance, in the previous example, (addLog(x) crypt(x) ; addLog(x) in order to generate encrypted logs.

This option is flexible but can be tedious. Instead of writing a new insert for each conflict, the programmer may indicate how to compose inserts at the aspect level. We propose a parallel operator ||_seq to indicate that whenever a conflict occurs, (I₁ I₁ ; I₂ (where ";" denotes the sequencing operator of the programming language). Other parallel operators are useful, such as ||_fst, which replaces (I₁ I₁ only.

Let us reconsider the two aspects logAccess and cryptRead:

• logAccess ||_seq cryptRead generates plaintext logs for super users.

• cryptRead ||_seq logAccess generates logs for users by logging (possibly encrypted) accesses.