Section 9.5. STATIC WEAVING OF SAFETY PROPERTIES


9.5. STATIC WEAVING OF SAFETY PROPERTIES

The previous restrictions allow detecting interactions during weaving. However, they are not sufficient to detect semantic interactions. The code inserted by an aspect may still influence the application of another independent aspect. Our notion of independence only ensures that aspects can be woven in any order. In order to prevent semantic interactions and, more generally, to control the semantic impact of weaving, one has to restrict the language of inserts. Here, we consider the same aspect language as the previous section, except for the language of inserts, which becomes:


I ::= skip | abort

Even if this restriction is quite drastic (aspects can only abort the execution), interesting aspects can still be expressed. The expressive crosscut language allows us to specify safety properties (properties stating that no "bad thing" happens during the execution). Aspects can be used to rule out unwanted execution traces and to express security policies [3].

This restriction has several benefits:

  • Aspects are semantic properties, and the impact of weaving is clear.

  • Inserts always commute. There are no interactions between aspects, which can be composed freely in parallel.

The woven program satisfies the property/aspect: For executions in accordance with the property, it has the same behavior as the base program. Otherwise, it produces an exception and terminates just before violating the property.

The main drawback of execution monitors is their run-time cost. They are not specialized to the program, and each program instruction may involve a run-time check. In the remainder of this section, we present how to weave such trace-based aspects statically and efficiently.

9.5.1. Example

Consider the following aspect:


safe = accountant()  skip ;
         (manager()  skip ;critical()  skip ;  critical()  abort ;  manager()  skip ;
         (accountant()  skip ;critical()  skip ;  critical()  abort ;  critical()  abort ; The property defined by the aspect states that a critical action cannot take place before the clearance of the manager and the accountant (i.e., at least a call to manager and to accountant must occur before each call to critical).

Figure 9-1 illustrates weaving of this property on a very simple imperative base program.

Figure 9-1. Weaving safe on a simple imperative base program.


Since the property is specified by a finite state aspect, it can be encoded as an automaton with alphabet {m, a, c} corresponding to the calls to manager, accountant, and critical, respectively. Notice that the base program may violate this property whenever the condition of the first if statement is false. The woven program, where two assignments and a conditional have been inserted, satisfies the property (i.e., aborts whenever the property is about to be violated).

An important challenge is to make this dynamic enforcement as inexpensive as possible. In particular, if we are able to detect statically that the base program satisfies the property, then no transformation should be performed.

9.5.2. Weaving Phases

Our aspects define a regular set of allowed finite executions. An aspect is encoded as a finite state automaton over events. The language recognized by the automaton is the set of all authorized sequences of events.

The weaver is a completely automatic tool that takes the automaton and the base program and produces an instrumented program [3]. We now outline its different phases (depicted in Figure 9-2).

Base Program Annotation. The first phase is to locate and annotate the instructions of the base program corresponding to events (crosscuts). Depending on the property we want to enforce, the events can be calls to specific methods, assignments to specific variables, opening of files, etc. A key constraint is that an instruction of the base program must be associated with at most one event. This is easy to ensure when events are specified solely based on the syntax. In order to take semantic crosscuts into account, the base program must be transformed beforehand. Consider the event "x is assigned the value 0." It cannot be statically decided whether an assignment x:=e will generate this event or not. A solution is to transform each assignment x:=e into the statement if e=0 then x:=e else x:=e where each instruction is now associated with a single event. Such pre-transformations rely on static program analyses to avoid insertion of useless tests.

Base Program Abstraction. The base program is abstracted into a graph whose nodes denote program points and whose edges represent instructions (events). The abstraction makes the next two phases independent of a specific programming language. Since the aspect is a trace property, the abstraction is the control-flow graph of the base program. In order to produce a precise abstraction, this phase relies on a control-flow analysis.

Instrumentation. The next phase is to transform the graph in order to rule out the forbidden sequences of events. We integrate the automaton by instrumenting the graph with additional structures (states and transition functions) that mimic the evolution of the automaton. Intuitively, this instrumentation corresponds to the insertion of an assignment (to implement the state transition of the underlying automaton) and a test (to check whether the property is about to be violated) before each event. This naïve weaving is optimized by the next phase.

Optimizations. The instrumented graph is refined in three steps. The automaton specifies a general property independent of any particular program. The first step is to specialize the automaton with respect to the base program. Second, a transformation similar to the classical automaton minimization yields a normalized instrumented graph. Finally, static analyses are used to optimize the automaton by removing useless state transitions.

The graph after optimization represents a program where at most one test and/or assignment (state transition) have been inserted at each if and while statement.

Concretization. The optimized graph must be translated back into a program. The graph has remained close to the base program since its nodes and edges still represent the same program points and instructions. We just need a way to store, fetch, and test a value (the automaton state) without affecting the normal execution. This is easily done using a fresh global variable.

Figure 9-2. Phases of weaving.


9.5.3. Just-In-Time Weaving

The most interesting application of this technique is securing mobile code on receipt. The local security policy is declared as a property (aspect) to be enforced on incoming applets. The just-in-time weaver secures (i.e., abstracts, instruments, optimizes, and concretizes) an applet before loading it. Since some steps are potentially costly, our implementation uses simple heuristics that make the time complexity of weaving linear in the size of the program.

There are several benefits to this separation of security concerns. First, it is easier to express the policy declaratively as a property. Second, the approach is flexible and can accommodate customized properties. This feature is especially important in a security context where it is impossible to foresee all possible attacks and where policies may have to be modified quickly to respond to new threats.



Aspect-Oriented Software Development
Aspect-Oriented Software Development with Use Cases
ISBN: 0321268881
EAN: 2147483647
Year: 2003
Pages: 307

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net