9.5. STATIC WEAVING OF SAFETY PROPERTIESThe 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:
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:
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. ExampleConsider the following aspect:
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 PhasesOur 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).
Figure 9-2. Phases of weaving.9.5.3. Just-In-Time WeavingThe 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. |