Temporal Aspects

Our starting point is aspect-oriented languages (see, for example, Kiczales et al. 1997) such as AspectJ (Kiczales et al. 2003). In the aspect-oriented approach to software change, new functionality can be added, or existing functionality changed, by adding advice code to an existing method call. A paradigmatic example of this style of programming is the addition of logging to an existing program. By adding appropriate advice, a programmer can trap method calls and cause log information to be written; the key being that the existing source code of the program does not need to be modified. It is clear that these program-transformation techniques are relevant to security: rather than logging method calls, advice could block unauthorized method calls.

Prior work on aspect-oriented security assurance (such as Cigital Labs, 2003) builds on aspect languages as they exist. We argue that current aspect-oriented languages, such as AspectJ, lack key ingredients required for our purposes.

• They are based on the static edit/compile/test cycle of software development, and do not support the dynamic advice loading required for on-line configuration of software systems.
• They do not support full history-based access control. For example, AspectJ only supports a limited form, called cflow, that provides information similar to the current call stack.
• They do not currently support detection of feature interaction. Even for small numbers of features, tool support for detecting feature interaction is a key component in the analysis of system trustworthiness.

The aim of the Temporal Aspects project is to design an aspect-oriented language that addresses these shortcomings. This research follows the line of research in language-based security such as Abadi and Gordon's (1999) spi-calculus, surveyed by Mitchell (2001).

Language design

Widely-used aspect-oriented languages such as AspectJ are based on static weaving of advice, which is performed at compile-time rather than run-time. We will study languages that support dynamic advice loading. We have already published preliminary results (Jagadeesan et al., 2003, and Bruns et al., 2004) that analyze the execution semantics of such aspect-oriented languages.

The observation that dynamic advice is necessary for modelling security properties is not unique to our work: parallel work by Walker et al. (2003) has shown the power of dynamic aspects for giving security guarantees in a functional setting. However, our work differs from theirs in a number of ways, of which the most crucial is the treatment of pointcuts. Pointcuts are logical formulae describing when a piece of advice should be applied: in the work of Walker et al., pointcuts are treated as atomic, named, control-flow points. In our previous work, pointcuts were taken from a propositional logic.

To accomodate history-based access control, we will extend the logic of pointcuts to include temporal properties. This allows the specification of security policies and their implementation to be given in one common language of great expressive power: that of temporal logic (see, for example, Manna and Pnueli, 1991). The classical methods that compile temporal formulas to automata (Vardi and Walter, 1986) provide the infrastructure required to translate these policy specifications to mechanisms that can be implemented.

These two ingredients, dynamic aspects and temporal aspects, will serve as the basis for the design of a domain-specific aspect-based language that serves both to realize system functionality and dynamically configure security properties.

Analysis and Validation

The key analysis problem we will address is the interaction between security policies that are described as aspects.

A novel feature of our approach is the cross-fertilization of ideas with the closely-related area of feature interaction in telecommunication systems. For example, suppose Alice wishes to screen calls from Bob, but that Bob is forwarding calls from Alice's son Charlie to Alice. Should a call to Alice from Charlie be screened if it is forwarded to Alice via Bob?

Existing work on detecting interactions use classical techniques such as model checking (Blom et al., 1994), bisimulation checking (Bruns et al., 1999), or more local analysis (Fisler and Krishnamurthi, 2001). However, these techniques are not directly applicable to this proposal, which involves programs rather than abstract process models, and in which features can be dynamically deployed.

We will therefore adapt classical programming language and model-based techniques for analysis. We will explore validation methodologies that occupy different points in the spectrum along two dimensions: in the range of expertise required from the tool user (from fully-automated to those that require significant domain knowledge) and in the guarantees provided (ranging from ``bug-finding'' to guarantees of conformance to specifications).

References

M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: the spi calculus. In Information and Computation 148:1-70, 1999.

J. Blom, B. Jonsson, and L. Kempe. Using temporal logic for modular specification of telephone services. In W. Bouma and H. Velthuijsen, editors, Workshop on Feature Interactions in Telecommunications Systems II, pages 197-216. IOS Press, 1994.

Cigital Labs. AOP: An aspect-oriented security assurance solution. DARPA-funded project, 2003.

G. Bruns, R. Jagadeesan, A. S. A. Jeffrey and J. Riely. μABC: A minimal aspect calculus. In Proc. Concur. Springer-Verlag, pages 209-224, 2004.

G. Bruns, P. Mataga, and I. Sutherland. Feature as service transformers. In Feature Interactions in Telecommunications Systems V. IOS Press, 1999.

K. Fisler and S. Krishnamurthi. Modular verification of collaboration-based software designs. In Proc. ACM Conf. Foundations of Software Engineering, pages 152-163. ACM Press, 2001.

G. Kiczales, J. Lamping, A. Mendhekar, C. Maeda, C. V. Lopes, J.-M. Loingtier, and J. Irwin. Aspect-oriented programming. In Proc. European Conference on Object-Oriented Programming, 1997.

G. Kiczales, E. Hilsdale, J. Hugunin, M. Kersten, J. Palm, and W. G. Griswold. An overview of AspectJ. Lecture Notes in Computer Science, 2072:327-355, 2001.

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.

J. C. Mitchell. Programming language methods in computer security. In Proc. ACM Symp. on Principles of Programming Languages, pages 1-26. ACM Press, 2001.

M. Vardi and P. Wolper. Automata theoretic techniques for modal logics of programs. J. Computer and Systems Sciences, 32:183-221, 1986.

D. Walker, S. Zdancewic, and J. Ligatti. A theory of aspects. In Proc. ACM Int. Conf. Functional Programming, 2003.