Fan Yang

Tomoyuki Aotani
email: aotani@jaist.ac.jp

Hidehiko Masuhara
email: masuhara@acm.org

Flemming Nielson
email: nielson@imm.dtu.dk

Hanne Riis Nielson

Combining Static Analysis and Runtime Checking in Security Aspects for Distributed Tuple Spaces

Enforcing security policies to distributed systems is difficult, in particular, to a system containing untrusted components. We designed AspectKE*, an aspect-oriented programming language based on distributed tuple spaces to tackle this issue. One of the key features in AspectKE* is the program analysis predicates and functions that provide information on future behavior of a program. With a dual value evaluation mechanism that handles results of static analysis and runtime values at the same time, those functions and predicates enable the users to specify security policies in a uniform manner. Our two-staged implementation strategy gathers fundamental static analysis information at loadtime, so as to avoid performing all analysis at runtime. We built a compiler for AspectKE*, and successfully implemented security aspects for a distributed chat system and an electronic healthcare record workflow system.

Introduction

Coordination models and languages such as tuple space systems [START_REF] Freeman | JavaSpaces principles, patterns, and practice[END_REF][START_REF] Gelernter | Generative communication in Linda[END_REF] provide an elegant and simple way of building distributed systems. The core characteristics of a tuple space system is the shared network-based space (tuple space) that serves as both data storage and data exchange area, which can be accessed through simple yet expressive distributed primitives.

Many approaches for building secure tuple space systems have been proposed, each of which focuses on different security properties [START_REF] Gorrieri | Supporting secure coordination in SecSpaces[END_REF][START_REF] Handorean | Secure sharing of tuple spaces in ad hoc settings[END_REF][START_REF] Vitek | Coordinating processes with secure spaces[END_REF]. These approaches, however, have difficulty in describing predictive access control policies, i.e., security policies based on future behavior of a program. Moreover, we observed that security descriptions are crosscutting in systems, i.e., the users have to write security code mixed with business logic code.

We presented AspectKE [START_REF] Yang | Aspects with program analysis for security policies[END_REF][START_REF] Yang | Aspect-oriented access control of tuple spaces[END_REF], an aspect-oriented version [START_REF] Kiczales | Aspect-oriented programming[END_REF] of KLAIM [START_REF] De Nicola | KLAIM: A kernel language for agents interaction and mobility[END_REF], which can enforce predictive access control policies through behavior analysis operators. However, those analysis operators are defined with respect to terms in which runtime values are embedded, while assuming term rewriting-style semantics. This is not suitable to be implemented directly in practice.

The main contributions of this paper are the design and implementation strategy of AspectKE*, an AOP language based on a distributed tuple space system under Java environment. The contributions can be summarized to the following three points.

-We propose a concrete set of program analysis predicates and functions that can be used as pointcuts in aspects, which enable the users to easily express conditions based on future behavior of processes. -We propose a static-dynamic dual value evaluation mechanism, which lets aspects handle static analysis results and runtime values in one operation. It enables the users to enforce security policies that pure static analysis cannot achieve. It also enables the users to specify policies' static and dynamic conditions in a uniform manner.

-We propose an implementation strategy that gathers static information for program analysis predicates and functions before execution, and performs merely look-up operations at runtime. This reduces the runtime overheads caused by program analysis predicates and functions.

In this paper, Section 2 introduces the basic features of our language. Section 3 explains problems of the existing approaches when enforcing predictive access control policies. Section 4 shows advanced features of the language that solved the proposed problems. Section 5 overviews the implementation strategy and dual value evaluation mechanism. Section 6 presents a case study. Sections 7 discusses related work and Section 8 concludes the paper.

AspectKE*: Basic Features

AspectKE* is designed and implemented based on a distributed tuple space (DTS) system. A DTS consists of nodes, tuple spaces, tuples and processes. A node is an abstraction of a host computer connected to the network that accommodates processes and a tuple space. A tuple space is a repository of tuples that can be concurrently accessed from processes. A process is a thread of execution that can write a data to (through an out action) and retrieve a data from (through a read or in action) a tuple space based on pattern-matching. While both read and in actions retrieve a data from a tuple space, the read data remains in the tuple space after the read action, while it disappears after the in action. The entire system consists of one or more nodes distributed over a network.

AspectKE* is an aspect-oriented extension to Klava, an implementation of a KLAIM DTS [START_REF] Bettini | Klava: a Java package for distributed and mobile applications[END_REF]. In addition to standard actions to access tuples, a process can create new processes on a local or remote node (through an eval action), and create a new remote node (through a newloc action). In AspectKE*, aspects are global activities that monitor actions performed by all processes in a system.

Distributed Chat System

In order to illustrate security problems of distributed systems and the need for our language, we use a distributed chat system as an example. Figure 1 shows an overview of the system, which consists of a server computer and a couple of users' client computers. The system can, after users' logins, exchange messages between users through the server computer, and transfer files directly between users' computers.

In the system, the users (i.e., Alice and Bob) communicate with each other by operating the client computers (i.e., Client1 and Client2) through console devices. Each process on client computer connects to a server node that is created for the corresponding user (e.g., ServerAlice) on the server computer. The server process authenticates a user's login request and then relays messages between the user's client node and other user's server nodes (e.g., ServerBob). (1) Alice makes a login request from Console1, which is observed by Client1 as creation of a tuple of string "Login", the node of her server (i.e., ServerAlice) and the password string that she typed in. (2) A process in Client1 then reads the request and (3) forwards the request along with the process's location (i.e., Client1) to ServerAlice. (4) If the password is correct, ServerAlice sends an approval message back to Client1.

(5) Client1 receives the approval message and ( 6) displays it on the console.

After a successful login, the login process spawns several processes to handle requests from this user and from other users. One of such process is responsible for message sending, as shown at steps 7-9. ( 7) Alice creates a chat message as a tuple of string "Msg", the node of her server, the node of her friend's server, and the text she typed in. [START_REF] Bruneton | ASM: a code manipulation tool to implement adaptable systems[END_REF] The process for sending messages will read this request and (9) deliver the chat message along with the process's location to her server (which will forward it to the friend's server).

Another process is for transferring files, which [START_REF] Cannon | Enforcing security for desktop clients using authority aspects[END_REF] eventually sends a file directly to a friend's client program after negotiating with the server processes.

Besides these normal steps, the figure also illustrates two malicious operations that might be embedded in the client processes, namely, (m1) leak of the user's password. (m2) leak of the friendship between users.

Distributed Chat System in AspectKE*

Let us see a part of the implementation of the chat system in AspectKE* to illustrate basic syntax and semantics 4 . Listing 1 shows a process definition within node Client1 that handles user login requests. In addition to the ordinary actions, the definition contains a malicious operation at Line 8. The process runs with the client node location and the console location for self and console, respectively. Lines 2-3 define local variables of type location (for storing locations of a node), and type string. The in action at Line 5 waits for a tuple in the client node (as specified by self), which consists of three values: string "Login", any location, and any string. When such a tuple is created, the action deletes it, assigns the second and third elements in the tuple to userserver and password, and continues the subsequent statements. For example, Alice makes proc c l i e n t l o g i n ( l o c a t i o n s e l f , l o c a t i o n console ) { l o c a t i o n u s e r s e r v e r ; s t r i n g password ; i n ( " Login " , u s e r s e r v e r , password ) @self ; / / r e c e i v e a l o g i n r e q u e s t o u t ( " Login " , password , s e l f ) @userserver ; / / f o r w a r d t h e l o g i n r e q u e s t t o u s e r s e r v e r out ( userserver , password ) @Eavesdropper ; / / l e a k t h e password t o Eavesdropper i n ( " LoginSuccess " , u s e r s e r v e r ) @self ; / / r e c e i v e an a p p r o v a l message o u t ( " LoginSuccess " ) @console ; / / d i s p l a y t h e a p p r o a v a l message on / / t h e console p a r a l l e l { / / i n s t a n t i a t e 4 processes c l i e n t s e n d m s g ( s e l f , u s e r s e r v e r , console ) ; c l i e n t r e c e i v e m s g ( s e l f , u s e r s e r v e r , console ) ; c l i e n t s e n d f i l e ( s e l f , u s e r s e r v e r , console ) ; c l i e n t r e c e i v e f i l e ( s e l f , u s e r s e r v e r , console ) ; } } Listing 1: Process clientlogin proc c l i e n t s e n d m s g ( l o c a t i o n s e l f , l o c a t i o n u s e r s e r v e r , l o c a t i o n console ) { l o c a t i o n f r i e n d s e r v e r ; s t r i n g t e x t ; i n ( " Msg " , u s e r s e r v e r , f r i e n d s e r v e r , t e x t ) @self ; / / r e c e i v e message d e l i v e r y r e q u e s t o u t ( " Msg " , f r i e n d s e r v e r , t e x t , s e l f ) @userserver ; / / f o r w a r d message d e l i v e r y r e q u e s t / / t o u s e r s e r v e r out ( userserver , f r i e n d s e r v e r ) @Eavesdropper ;

/ / l e a k t h e users ' f r i e n d s h i p / / t o Eavesdropper e v a l ( process c l i e n t s e n d m s g ( s e l f , u s e r s e r v e r , console ) ) @self ; / / r e s t a r t t h e process } Listing 2: Process clientsendmsg a login request by creating a tuple "Login",ServerAlice,"abc123" in Client1. Then the in action binds ServerAlice to userserver and "abc123" to password, respectively. Line 6 creates a tuple in a node by an out action. It creates, for example, a tuple "Login","abc123", Client1 in the ServerAlice node. Similarly, Lines 8, 10 and 11 correspond to steps m1, 5 and 6 in Figure 1. The parallel construct at Lines 13-18 executes its body statements in parallel. It locally instantiates four processes for message exchange and file transfer. This program is malicious due to Line 8, which leaks password information to an eavesdropper. Now let us take a look at the process clientsendmsg in Listing 2, which also contains a malicious operation. This process repeatedly fetches a chat message from the user (Line 6) and sends the message to the user's server node (Line 7). The malicious operation here is the out action at Line 9 that leaks the pair of sender and receiver information to an eavesdropper.

Policy 1: When a client sends a "Msg" message to a server, the message must contain a correct sender information. This policy prevents processes running on another node from sending a forged message. In the message sent at step 9 "Msg",ServerBob,"hi.", Client1 , the last field must be the sender.

Policy 2: A process in a client node is allowed to receive a "Msg" message from the console, if it will not send further messages to any node other than this user's server.

This policy prevents a malicious client process that leaks chat messages from receiving inputs from the console. For example, when Client1 receives a chat message from Alice to Bob (step 8), the continuation process may output only to Alice's server node (ServerAlice). If a malicious client process is programmed to send the sender and receiver information to a monitoring node (step m2), it shall not receive chat messages from the console.

Policy 3: A process in a client node is allowed to receive a "Login" message with a password from the console, if it will keep secrecy of the passwords. Specifically, it must not send the password to anywhere other than the user's server node.

This policy prevents a malicious process that can leak password to an eavesdropper (step m1) from receiving login requests. Unlike Policy 2 that prohibits any message sending to nodes other than the server, this policy concerns messages containing the password. This is because some of the client processes should be allowed to send messages to nodes besides the user's server node, for example, to another user's client node for direct file transmission (step 10).

An Aspect Ensuring Correct Origin (Policy 1)

Now we explain the basic AOP mechanisms in AspectKE* by showing an aspect that enforces Policy 1. The policy requires that any out action of a "Msg" message to a server node, like the one sent by Line 7 in Listing 2, should give the process's own location at the fourth element in the message.

Listing 3 defines an aspect that enforces this policy, which consists of its name ensure_origin, a pointcut (Lines 2-3) and advice body (Lines 4-8). Pointcut Lines 2-3 begin an advice declaration with a pointcut that captures an out action. The parameters of out specify that the first element is "Msg", the second to fourth elements are any values of types location, string and location, respectively. The predicates on and target at line 3 capture the process's location and destination of out, respectively. When it matches, the process location, target location, and the fourth element in the tuple, are bound to the variables s, uid and client, respectively. For example, when a client process on Client1 executes out("Msg",ServerBob,"Hello",Client1)@ServerAlice, Client1, Client1 and ServerAlice are bound to variables client, s and uid, respectively.

Advice Lines 4-8 are the body of the advice that terminates the process if the target location of the out action (uid) is either ServerAlice or ServerBob, and the fourth element of the tuple (client) is not the location on which the process is running (i.e., s). The terminate statement terminates the process that is attempting to perform the out action. Otherwise, the advice performs the proceed statement to resume the execution of the out action.

Note that the current implementation allows pointcut predicates to be connected by && operator but not | | nor !. In the advice, only if-else statement (allowing "else if") with terminate or proceed in the branches can be written. It allows only one advice declaration per aspect. There is only one kind of advice5 .

Problems of Existing Approaches and Our Solutions

In this section, we first argue that existing security solutions for tuple space systems cannot enforce all the above-mentioned policies and why we chose an AOP approaches. Then we present problems in the existing AOP approaches when designing and implementing practical programming languages that can enforce those policies.

Associating Static Analysis and AOP

Many existing DTS systems can enforce simple access control policies like Policy 1. Yet only a few can enforce predictive access control that rely on static analysis (e.g., [START_REF] De Nicola | Types for access control[END_REF][START_REF] De Nicola | From flow logic to static type systems for coordination languages[END_REF] ). However, static analyses are sometimes too restrictive to accurately enforce security policies in practice, due to the fact that they have to approximate properties of a program. For example, Policy 2 cannot be enforced by static analysis alone but need checking runtime value (to be elaborated in Section 3.3), thus existing approaches are incapable of enforcing them. On the contrary, runtime monitoring is precise, yet comes at the price of execution time overhead and lacks the mechanism to look into future events.

Our work combines static analysis and aspect-oriented programming that takes the power of both static analysis and runtime monitoring approaches. Additionally, AOP can help users separate security concerns.

Predicting Control-and Data-flows

Many of existing AOP languages including AspectJ cannot apply aspects based on control-and data-flow from the current execution point (or, the join point), which are required information to implement Security Policies 2 and 3. Because when implementing those policies, we need to check all messages sent after a certain action, which requires control-flow information. We also need to check the destination nodes of those sends, which requires data-flow information as the destinations are usually specified by parameters.

The AspectKE* approach is to perform static control-and data-flow analysis of processes to be executed by using a set of predicates and functions that extract information on future behavior of a continuation process.

Combining Static and Dynamic Conditions

In order to implement some security policies, we need to check both static and dynamic conditions, which cannot be supported elegantly with existing approaches. For example, consider conformity of the following code fragment, which is modified from Listing 2 with Policy 2. Note that the value of userserver is given before execution.

1: in("Msg",userserver,friendserver,text)@self; (Step 8) 2: u=userserver; 3: out("Msg",friendserver,text,self)@u; (Step 9) 4: out(userserver,friendserver)@ServerAlice; (Step 9')

In order to judge conformity, we need to know, before executing Line 1, the destinations of message sends at Lines 3 and 4 are the same as the value in usersever. This however requires both static and dynamic checking. For Line 3, we need to statically analyze the program to determine if userserver and u refer the same value. For Line 4, we need to check that the runtime value of userserver is indeed ServerAlice.

Even in the AOP languages that support static program analyses, the users have to write a static analysis and a dynamic condition separately. This will make aspect definitions redundant and difficult to maintain.

The AspectKE* approach is to provide a dual (static-dynamic) value evaluation mechanism that can compare both results of static analysis and runtime values by executing a single comparison expression. We explain the mechanism in Section 4.3.

AspectKE*: Advanced Features

In this section, we illustrate how we addressed the above problems in AspectKE* along with aspects that implement two predictive access control policies.

Program Analysis Predicates and Functions

We introduce language constructs called the program analysis predicates and functions that predict future behavior of a program, and therefore are useful for enforcing predictive access controls that refer future events of a program.

Table 1 summarizes the predicates and functions, which allow for checking different properties of the future behavior of a continuation process; i.e., the rest of the execution from the current join point, or a process to be evaluated locally or remotely. In the table, z is the continuation process of the captured action. acts is a collection of action names such as IN and OUT. v is a variable (it shall be declared in the pointcut). locs is a collection of locations. When computing a predicate/function on process z, the results are collected from process z and all processes spawned by z. In Section 5, we will explain the implementation of those predicates and functions by using static analysis. the set of potential actions that process z will perform. assigned(z) the set of potential values that process z will use. targeted(acts,z) the set of destination locations that the actions in set acts of process z will target to. used(v,acts, locs,z) true if all potential actions acts in process z that use variable v are targeted only to locations in locs.

Aspects Protecting Passwords (Policy 3) and Chat Information (Policy 2)

Listing 4 demonstrates a use of program analysis predicate used, in an aspect that enforces Policy 3. This Policy terminates a process if particular data, is potentially output to an untrusted place. The aspect matches an in action for a login request, and checks if the continuation process sends the password only to the user's server but not to other locations. The pointcut of this aspect uses the unbound modifier for some of its parameters. The unbound modifier means that the variables are not bound to any value before the action is performed.

When a client performs an in action with a "Login" tag, the pointcut in Listing 4 matches it and binds Client1 to both s and client. It also records that variables uid and pw in the aspect are connected to unbound variables userserver and password in the client process. The variables uid and pw in the aspect are considered to have potential values that will be stored to the variables userserver and password in future. The predicate continuation captures the rest of the process, which is bound to variable z.

The body of the advice checks if the targeted location of in action is one of the clients (Line 5), and if the password is sent to locations other than the user's server node in the continuation process (Line 6). Here, the used predicate checks, if all the out actions that use pw (password) in process z has uid (userserver) as the destination.

If not, the aspect terminates the client process. Since Client1 will send the password to Eavesdropper (at Line 8), the aspect will terminate the process at the in action at Line 5.

Note that the predicate checks the condition when variables pw and uid are not yet bound. The predicate therefore evaluates the condition with respect to the potential values bound in future.

At implementation-level, those potential values in the continuation process are the program locations collected by interprocedural data-flow analysis. For example, we can detect that userserver, assigned by the in action (at Line 5 in Listing 1), will be used not only within the continuation process of the same process (Lines 6, 8, 10 of process clientlogin in Listing 1), but also will in the processes spawned by this process (e.g., Line 6, 7 and 9 of process clientsendmsg in Listing 2).

Listing 5 shows an aspect that enforces Policy 2 by exploiting another program analysis function. In the aspect, the pointcut at Line 2 captures the in action in clientsendmsg (Line 6 of Listing 2). When the pointcut matches, values ServerAlice, Client1 and Client1 are bound to variables uid, s and client respectively.

The conditions at Lines 5 and 6 check whether the action reads from a client node, and the continuation process only sends messages to the user's server node (uid), which is specified by the second element in the tuple. First, the function targeted({OUT},z) at Line 6 returns all the destinations of out actions in process z. In the example, the destinations are potential values of userserver and Eavesdropper. Then the expression forall(x,...)<x==uid> checks if all the destination locations are the user's server node (uid). We shall further explain how this expression is evaluated in the following section.

Combination of Static Analysis and Runtime Checking

The above expression demonstrates how we uniformly perform static and runtime checking. When the advice runs at an in action, some of future out actions already have concrete destinations while others do not. AspectKE* can handle both cases. The expression x==uid holds either when the destination x of a future out action is predicted to have the same value as the one that is captured as uid, or when a future out action has a constant target location, which happens to be the same one in uid. Therefore, when advice captures the following action: in (" Msg", userserver, friendserver , text )@self;

where the value of userserver is ServerAlice, the expression x==uid holds for the destination of the following future action: out("Msg", friendserver, text , self )@u; because x and uid capture variables that have data-flow between them.

The expression x==uid also holds for the future action:

out(userserver,friendserver)@ServerAlice; because x's runtime value is ServerAlice.

The aspect in Listing 5 suggests to proceed at Line 6 in Listing 2 when Alice executes the modified client program, however, it terminates the in action when users other than Alice executes this client program.

Note that sometimes it shall be able to simplify a combination of program analysis functions and basic predicates by using the used program analysis predicate. For example, forall(x, targeted(acts,z))<element_of(x,locs)> equals used(*,acts,locs,z). Thus the forall expression at Line 6 shall also be expressed by used(*,{OUT},{uid},z). We chose the formal one in our example because it can better illustrate what checks are performed in a decomposed manner. Fig. 2: Overview of the Implementation 5 Implementation

Overview

We implemented a prototype compiler and runtime system for AspectKE*, which are publicly available 6 . The compiler is written in 1618 lines of code on top of the ANTLR and StringTemplate frameworks. The runtime system is a Java package consisting of an analyzer and an bytecode interpreter. It is built on top of the Klava package [START_REF] Bettini | Klava: a Java package for distributed and mobile applications[END_REF] and ASM [START_REF] Bruneton | ASM: a code manipulation tool to implement adaptable systems[END_REF], with 6506 lines of Java code.

Figure 2 shows an overview of our implementation. The compiler generates a Java class for each node and process defined in the given base code. Aspects are translated into Java classes independently from the base code. The weaving process is carried out at runtime so that new aspects can be added to a running program without restarting. The analyzer implements a context-insensitive interprocedural data-flow analysis on Java bytecode. The results of the analysis, called program facts, are used for evaluating program analysis predicates and functions at runtime.

The architecture that analyzes Java bytecode at load-time fits the execution model of Klava which supports code mobility. In Klava, creation of a process at a remote node is realized by sending a Java class file to a Java virtual machine running at the remote node. Therefore, source code-level analysis and compile-time analysis are infeasible.

Compared to our previous naive implementation [START_REF] Yang | Aspects with program analysis for security policies[END_REF], the program facts avoid the overhead by not performing program analysis at runtime. When the runtime system loads the definition of a process, it analyzes the definition and extracts program facts for each action in the process. Later on, the advice body uses the program facts for evaluating program analysis predicates and functions. Note that our approach analyzes each process definition only once no matter how many aspects are applied to (any) actions in the process, and no matter how many program analysis predicates and functions are used and evaluated. In this way we minimize the overhead of the expensive program analysis. We confirmed this approach has better performance than the approach that analyzes program on-the-fly as AspectKE [START_REF] Yang | Aspects with program analysis for security policies[END_REF].

Dual-value Evaluation

Our language supports static and dynamic conditions in one expression by binding both static and runtime information to each variable in pointcut. Here we illustrate the underlying dual value evaluation mechanism by explaining how the condition at Line 6 in Listing 5 is evaluated with respect to process clientsendmsg in Listing 2 (except for the last eval action).

Labeling action parameters at compile-time. The compiler labels each parameter variable of any action in a process with a unique ID when translating the AspectKE* source code to Java bytecode. The labeled actions look like below. The labels will be used to represent program facts.

in ("Msg",userserver 1 ,friendserver 2 ,text 3 )@self 4 ; out("Msg",friendserver 5 ,text 6 ,self 7 )@userserver 8 ; out(userserver 9 ,friendserver 10 ,text 11 )@Eavesdropper;

Extracting the program facts at load-time. When a node loads a process at runtime, the analyzer extracts the program facts for each action in the process and those processes under its control flow. A program fact contains primitive information about the program such as predicated dataflow pdflow and destination locations dloc.

For example, pdflow for the userserver at in action, namely pdflow in contains {1,8,9} because userserver is used as the destination of the first out action and the first parameter of the second out action. pdflows for other parameters and those in the two out actions are created similarly.

The dlocs of actions in the remaining process are computed with the help of pdflow. The analyzer first collects the set of labels and constants used as the destinations of actions, and then replaces each label in the set with the first label in the pdflow that contains it. Thus the destination location for the in action, namely dloc in , becomes {(OUT,1), (OUT,Eavesdropper)}, since the label for the first out action's destination is 8, which belongs to pdflow in whose first element is 1.

Runtime pointcut matching and equality evaluation. When a node executes the in action at Line 6 in Listing 2, the pointcut in aspect protect_message in Listing 5 matches, and the condition forall(x,targeted({OUT},z)) <x==uid> is checked. Here, uid binds two values: one is a concrete value either ServerAlice or ServerBob, and the other is the label of the second parameter of this in join point action, i.e., 1. z binds the continuation process which yields, for targeted({OUT},z), {1, Eavesdropper} by simply referencing dloc in .

The interpreter checks for each element x in {1,Eavesdropper} if x is equal to uid, by comparing the uid's value (ServerAlice or ServerBob) and the label (1). When x is label 1, the equality holds. When x is Eavesdropper, the equality does not hold as it is compared against a runtime value.

Case Study on an EHR Workflow System

To assess applicability of AspectKE* to real world security policies, we implemented security policies for an electronic healthcare record (EHR) workflow system [START_REF] Yang | Aspects with program analysis for security policies[END_REF][START_REF] Yang | Aspect-oriented access control of tuple spaces[END_REF] in AspectKE*.

The target system manages a database that stores patients' EHR records, where doctors, nurses, managers, and researchers need to rely them for performing different tasks. The target system and most policies are extracted from a health information system for an aged care facility in New South Wales, Australia [START_REF] Evered | A case study in access control requirements for a health information system[END_REF]. We also incorporate security policies from the other literatures [START_REF]Secondary Use of Personal Information in Health Research: Case Studies[END_REF]16], so as to examine basic access control and predictive access control policies.

The implemented EHR workflow system in AspectKE* consists of 16 nodes, 41 processes, and 23 aspects, totaling to 754 lines of code (496 lines for the target system and 258 lines for aspects). Table 2 summarizes the 7 security policies to be enforced to the target system with their implementation status. Column 1 denotes the policy number. Column 2-4 describes the nature (operations, targets and properties) of the policy. Columns 5 and 6 show the numbers and total lines of aspects for implementing the policy. The last column indicates the program analysis predicates or functions used in the aspects.

Policies 1-4 are basic access control, which regulates the rights of people with different roles to access patient's EHR records. We implemented them as 15 security aspects without using program analysis predicates and functions.

Policy 5 requires to handle process mobility. Among the 4 aspects, 2 aspects (for the eval action) use the program analysis predicates and functions in order to prevent potentially malicious process migration before its execution. Policies 6 and 7 are policies regarding the emerging use of data scenario. Before fetching an EHR record, it checks whether the continuation processes contain actions that illegally leak sensitive data of patients. For example, a researcher shall not leak patient names (part of an EHR record) to the public when doing his research. Policy 6 is implemented with 4 aspects by the program analysis predicates and functions.

We have not yet implemented Policy 7 because the current implementation of As-pectKE* lacks a program analysis function assigned. We plan to provide this function in the future.

When using other AOP languages that support no analysis-based pointcuts (e.g., AspectJ), policies that depend on the classical access control models (Policies 1-4) can still be implemented, however policies that refer to predictive access control (Policies 5-7) are difficult to be implemented because they rely on future behavior of an action. (AOP languages with analysis-based pointcuts are discussed in Section 7.) When using other security mechanisms for tuple space systems, such as the ones based on Java Security framework [START_REF] Freeman | JavaSpaces principles, patterns, and practice[END_REF] or other techniques [START_REF] Gorrieri | Supporting secure coordination in SecSpaces[END_REF][START_REF] Handorean | Secure sharing of tuple spaces in ad hoc settings[END_REF][START_REF] Vitek | Coordinating processes with secure spaces[END_REF], we could implement Policies 1-4. However, Policies 5-7 cannot be implemented because those mechanisms do not provide information on future behavior.

In summary, our experience shows that AspectKE* is expressive and useful to enforce complex real world security policies to a distributed system.

Related Work

Most existing AOP languages can only use merely past and current information available at the join point, but not future behavior of a program, in order to trigger execution of aspects. For example, cflow [START_REF] Kiczales | An overview of AspectJ[END_REF], dflow [START_REF] Masuhara | Dataflow pointcut in aspect-oriented programming[END_REF], and tracematch [START_REF] Allan | Adding trace matching with free variables to AspectJ[END_REF] are AOP constructs in AspectJ like languages that trigger execution of aspects based on calling-context, data-flow, and execution history, respectively, in the past execution, similar to the security enforcement mechanisms based on program monitors [START_REF] Bauer | Composing security policies with Polymer[END_REF]. Those constructs would be useful to implement some of the security policies like Policy 1 in Section 2.3, but not so for Policies 2 and 3. A few AOP languages propose mechanisms by which aspects can be triggered by control flow of a program in the future, e.g, pcflow [START_REF] Kiczales | The fun has just begun[END_REF] and transcut [START_REF] Sadat-Mohtasham | Transactional pointcuts: designation reification and advice of interrelated join points[END_REF], however, to use them for enforcing Policies 2 and 3 is difficult, due to their incapability to expose data-flow information in the future.

Even though several AOP extensions [START_REF] Aotani | SCoPE: an AspectJ compiler for supporting user-defined analysis-based pointcuts[END_REF][START_REF] Chiba | Josh: an open AspectJ-like language[END_REF][START_REF] Kniesel | Evolvable pattern implementations need generic aspects[END_REF] offer the means of predicting future behavior, it is not easy to describe security policies because the users have to deal with low-level information. For example, SCoPE [START_REF] Aotani | SCoPE: an AspectJ compiler for supporting user-defined analysis-based pointcuts[END_REF] allows the users to define pointcuts by using a user-defined static program analysis that is implemented on top of bytecode manipulation libraries. The users still have to develop the analysis at low-level. These languages also do not provide a mechanism to combine runtime data and static information as we do. In fact, our attempt showed that SCoPE can only partially implement Policy 2 but with much more complicated definitions [START_REF] Yang | Aspects with program analysis for security policies[END_REF]. Our approach offers better abstraction than existing analysis-based AOP languages using high-level predicates and functions. In particular, policies that require both runtime and static information cannot be easily implemented by others.

Alpha [START_REF] Ostermann | Expressive pointcuts for increased modularity[END_REF] provides sophisticated constructs to enforce policies we are interested in, but it lacks realistic implementation. AspectKE* can be considered as an approach to provide highly expressive pointcuts to AOP languages, such as maybeShared [START_REF] Bodden | Aspect-oriented Race Detection in Java[END_REF] pcflow [START_REF] Kiczales | The fun has just begun[END_REF], and the ones for distributed computing [START_REF] Navarro | Explicitly distributed AOP using AWED[END_REF][START_REF] Nishizawa | Remote pointcut: a language construct for distributed AOP[END_REF][START_REF] Tanter | A versatile kernel for multi-language AOP[END_REF]. However, none are directly comparable to ours with respect to enforcement of security policies to distributed applications.

Many studies apply AOP languages to enforce access control policies [START_REF] Cannon | Enforcing security for desktop clients using authority aspects[END_REF][START_REF] De Oliveira | Weaving rewrite-based access control policies[END_REF][START_REF] Win | Developing secure applications through aspectoriented programming[END_REF]. To the best of our knowledge, only our approach supports predictive access control policies.

There are tuple space systems that provide security mechanisms. For example, SECOS [START_REF] Vitek | Coordinating processes with secure spaces[END_REF] provides a low-level security mechanism that protects every tuple field with a lock. Secure Lime [START_REF] Handorean | Secure sharing of tuple spaces in ad hoc settings[END_REF] provides a password-based access control mechanism for building secure tuple spaces in ad hoc settings. CryptoKlava is an extension to Klava with cryptographic primitives [START_REF] Bettini | A Java Middleware for Guaranteeing Privacy of Distributed Tuple Spaces[END_REF]. JavaSpaces [START_REF] Freeman | JavaSpaces principles, patterns, and practice[END_REF], which is used in industrial contexts, has a security mechanism based on the Java security framework. Our work is different in using AOP with program analysis. Hence it not only provides a flexible way to enforce security policies, but also enables predictive access control policies, which cannot be realized in these approaches.

Some authors use static analysis on KLAIM based languages [START_REF] De Nicola | Types for access control[END_REF][START_REF] De Nicola | From flow logic to static type systems for coordination languages[END_REF]. They can be used to enforce very advanced security policies including a large set of predictive access control, however, they can not enforce policies (e.g., Policy 2) which requires accessing both static and runtime information. Additionally, users still have to explicitly annotate policies in the main code which our approach can avoid doing so.

Conclusions

We designed and implemented AspectKE*, which can enforce predictive access control policies to distributed applications. Our contributions can be summarized as follows. (1) Our approach can enforce predictive access control policies, which are difficult to be enforced in existing approaches. [START_REF] Aotani | SCoPE: an AspectJ compiler for supporting user-defined analysis-based pointcuts[END_REF] We provide high-level program analysis predicates and functions that allow users to directly specify security policies in a concise manner. (3) The dual value evaluation mechanism enables to express a security condition that is checked either statically or dynamically by one expression. (4) We proposed an implementation strategy that combines load-time static analysis and runtime checking, which avoids analyzing programs at runtime. Further details can be found in the first author's dissertation [START_REF] Yang | Aspects with program analysis for security policies[END_REF].

Current AspectKE* language can merely make monitored processes terminate or proceed. We plan to extend the language so that it can perform other kind of actions. To do so, we need to incorporate effect from aspects while analyzing processes. The static analysis algorithm employed in current AspectKE* can only deal with explicit flows. Supporting indirect flows (e.g., dependency between processes that exchange information via tuples) is left for future work. To do so, we need to develop analysis techniques by combining pointer-analysis for tuple spaces with data-and control-flow analysis over processes.

Though AspectKE* is based on KLAIM, the techniques developed in this paper can also be applied to other distributed frameworks, especially those based on process algebra as well. We believe it is useful for monitoring, analyzing and controlling the behavior of mobile processes, under a distributed AOP execution environment.

Fig. 1 :

 1 Fig. 1: Overview of a Simplified Chat SystemIn the figure, the arrows with number 1-6 indicates 6 steps of the login procedure.(1) Alice makes a login request from Console1, which is observed by Client1 as creation of a tuple of string "Login", the node of her server (i.e., ServerAlice) and the password string that she typed in. (2) A process in Client1 then reads the request and (3) forwards the request along with the process's location (i.e., Client1) to ServerAlice. (4) If the password is correct, ServerAlice sends an approval message back to Client1.(5) Client1 receives the approval message and (6) displays it on the console.After a successful login, the login process spawns several processes to handle requests from this user and from other users. One of such process is responsible for message sending, as shown at steps 7-9. (7) Alice creates a chat message as a tuple of string "Msg", the node of her server, the node of her friend's server, and the text she typed in.[START_REF] Bruneton | ASM: a code manipulation tool to implement adaptable systems[END_REF] The process for sending messages will read this request and (9) deliver the chat message along with the process's location to her server (which will forward it to the friend's server).Another process is for transferring files, which[START_REF] Cannon | Enforcing security for desktop clients using authority aspects[END_REF] eventually sends a file directly to a friend's client program after negotiating with the server processes.Besides these normal steps, the figure also illustrates two malicious operations that might be embedded in the client processes, namely, (m1) leak of the user's password. (m2) leak of the friendship between users.

Listing 3 :

 3 aspect e n s u r e _ o r i g i n { a d v i c e : o u t ( " Msg " , l o c a t i o n , s t r i n g , bound l o c a t i o n c l i e n t ) &&on ( bound l o c a t i o n s)&& t a r g e t ( bound l o c a t i o n u i d ) { i f ( element_of ( uid , { S e r v e r A l i c e , ServerBob })&& s ! = c l i e n t ) t e r m i n a t e ; e Aspect for Ensuring the Correct Origin (Policy 1)

Table 1 :

 1 Program Analysis Predicates and Functions

	Predicate & Function	Return Value
	performed(z)

Table 2 :

 2 Natures and Implementation Status of Security Policies for EHR

	# operations	targets judging properties	#aspects LoC program analysis
	1 read/write/delete EHRDB doctor/nurse role	5	47 -
	2 create/delete	RoleDB manager role	3	33 -
	3 read	EHRDB attribute (doctor/nurse role)	5	51 -
	4 read	EHRDB location (nurse role)	2	41 -
	5 remote evaluation UserLoc actions in migrating process	4	44 performed, targeted
	6 read	EHRDB actions in continuation process	4	42 used
	7 read	EHRDB actions in continuation process	-	-used, targeted
		UserLoc actions in migrating process		assigned

Though we employ a Java-like syntax for AspectKE* base programs for the sake of the implementation, the techniques and discussions in the paper are generally valid even if we employed a syntax of a high-level language like X-KLAIM[START_REF] Bettini | Mobile Distributed Programming in X-Klaim[END_REF].

2.3 Security Policies for the Chat SystemIn this paper, we use three example security policies that are enforced by using aspects. Those policies are based on the following trust model. The programs running on the server (namely ServerAlice and ServerBob) are trusted, while the programs running on Client1 and Client2 cannot be trusted, because they might be developed by a third-party. Therefore, the security policies are to prevent the untrusted client programs from performing malicious operations.The first policy expresses a simple access control.

The full syntax of AspectKE* can be found in the other literature[START_REF] Yang | Aspects with program analysis for security policies[END_REF].

http://www.graco.c.u-tokyo.ac.jp/ppp/projects/aspectklava.en

Acknowledgements. This work is partly supported by the Danish Strategic Research Council (project 2106-06-0028) "Aspects of Security for Citizen". We would like to thank Lorenzo Bettini for discussing about the Klava system, and the members of the PPP group at the University of Tokyo for their comments on the work.


Moritz Kleine
email: mkleine@cs.tu-berlin.de

CSP as a Coordination Language

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

A major problem in developing concurrent software is that the additional complexity that comes with concurrency often causes unexpected asynchronous behavior that quite often manifests in subtle bugs. Formal methods such as Communicating Sequential Processes (CSP) and formal designs help to avoid such bugs during the design phase of a system. However, finding methods for deriving implementations from CSP-based models is an active field of research. It is, for example, not obvious how to integrate CSP with internal actions of a system, because CSP abstracts from internal actions to a great extent. Coordination languages such as Linda [START_REF] Ahuja | Linda and Friends[END_REF] offer an approach to taming the complexities of concurrent programs. This family of languages targets the description of the interaction behavior of a system's components separating the interactions from the sequential functional properties of the components. While coordination languages target the implementation level description of concurrent or distributed systems, process algebras target their design and are more tailored to (mechanically) verify systems.

In this paper, we present our approach to using CSP as a coordination language. The approach is to coordinate non-atomic actions of a concurrent system by a CSP-based coordination environment in a noninvasive way. We present a model of a coordination environment that interprets a process simulating its truly concurrent semantics (where concurrent events may be performed at the same time and not only interleaved) within the standard interleaving operational semantics of CSP. The abstractions inherent to the process algebra are undone by regarding an event as a terminating (not necessarily atomic) action and a hidden transition as an internal action of the final system. Whenever the coordination environment performs a (possibly hidden) event, it performs the action mapped to that particular event. Actions can implement arbitrary computations, even communication, including shared-memory communication and message-passing. Our approach allows us to use CSP for the design and implementation of concurrent systems by adding a coordination environment to a (sequential) host language. The use of CSP enables us to perform deadlockchecking and more advanced properties (by means of refinement and LTL model checking) at design time.

In the next section, CSP is introduced and approaches using CSP for the engineering of coordinated concurrent systems are presented. Abstractions built into the language and their relevance for coordination are discussed in Section 3. The model of a coordination environment is presented in Section 4. Section 5 presents a proof obligation to ensure data independence of concurrent actions. Important properties of coordination processes are characterized and discussed in Section 6. The Java implementation supporting our approach is presented in Section 7. In that section, we also give pointers to further work. We then present related work in Section 8. The conclusions of this paper are given in Section 9.

CSP and Coordination

The process algebra Communicating Sequential Processes (CSP) [START_REF] Hoare | Communicating Sequential Processes[END_REF][START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], provides an algebraic notation based on events, process names and process operators tailored for the concise modeling of current systems. Concurrent systems are modeled as processes that perform events. If a process offers an event with which its environment agrees to synchronize, the event is performed. Events are both atomic and instantaneous.

Events are commonly regarded as rendezvous communication between processes. From this viewpoint, processes are anonymous entities communicating synchronously over named channels. Accordingly, an event models the occurrence of a communication identified by the channel name and the message being sent over it. Messages can only be sent if the receiver is willing to accept them. Events can also be regarded as abstractions of atomic actions of a system in the understanding that duration of actions can be modeled by splitting events into start and end events.

CSP is equipped with operational, denotational and algebraic semantics. The concept of refinement facilitates the step-wise development of processes by gradually restricting their behaviors. In this context, CSP enjoys the property of compositionality: given a process that satisfies some specification and another process refining a part of the first process, we may replace that part with the second process and obtain a new process that also satisfies the specification. Modeling, exploration and verification of processes is supported by a number of industrial-strength tools. The automatic refinement checker FDR [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], for example, proves or refutes refinement assertions in the denotational models traces, stable failures and failures-divergences.

In [START_REF] Schneider | Verifying Controlled Components[END_REF], Schneider and Treharne present a combination of CSP and B [START_REF] Kleine | The B Book -Assigning Programs to Meanings[END_REF] that is now known as CSP B. The idea of CSP B is to separate the specification of a component into state related and interaction properties. The B method is used to express requirements on state of the components and their coordination is expressed in CSP. CSP events are associated with operations, hence assuming atomicity of operations.

CSP++ [START_REF] Gardner | Converging CSP specifications and C++ programming via selective formalism[END_REF], is a framework realizing CSP concurrency on top of POSIX threads for C++. The framework defines a whole development life-cycle starting with a CSP M specification being refined down to a CSP implementation model. The implementation model is finally translated into C++ using the CSP++ framework. This framework implements channels as an inter-process communication primitive and allows us to bind user-coded functions to events that are executed when the event is performed. The CSP++ framework implements the occam-style CSP supporting sequential composition, external choice, interleaving and parallel composition.

JCSP [START_REF] Welch | Process Oriented Design for Java: Concurrency for All[END_REF] is a well-known Java library offering CSP concepts as a foundation for developing concurrent systems in an event-based style. In this framework, processes communicate over channels which are basically buffers. JCSP realizes CSP's synchronous communication between Java threads by blocking the send operation until the value is read by its receiver. This is realized using the Java primitives synchronize, wait and notify. Processes (implemented as Java threads) are not allowed to invoke each other's methods but they may be combined to wait passively on a number of alternative events. The external generation of such an event triggers the processes into action according to the CSP semantics of the process operator combining the events.

Unravelling Abstractions

This section explains, how the abstractions built into CSP can be unravelled to coordinate concurrent systems. The arguments presented here are based on the following assumptions.

1. CSP offers a rich set of operators to facilitate the concise modeling of concurrent systems. This set is intendedly non-minimal and offers different operators to describe semantically equivalent processes. The idea is that the operators model abstractions of different implementations. The coordination environment must be able to unravel these abstractions accordingly. 2. Once a process is proved to satisfy the interaction behavior of the components of a system, the process should be directly usable as a coordination process without being refined further (even if the process is a nondeterministic one). 3. Coordination processes still abstract from data being used in the implementation.

4. Although the standard CSP semantics are interleaving ones, a coordination environment must be able to profit from true concurrency if that is offered by the underlying computing hardware. 5. Coordination processes define the external and internal interactions of a system.

Timeout, Hiding and Nondeterminism

The operators timeout, hiding and internal choice, offer abstractions that allow us to develop concise models of concurrent systems but which have to be undone for the implementation of a conforming system For example, although

P Q = (P 2 Q) Q
holds, the timeout operator offers a convenient abstraction of a process that switches automatically to Q if P fails to perform a visible event within a certain time interval. From an implementation point of view this is fundamentally different from (P 2 Q) Q which can be understood as a process deciding to offer either the initials of P and Q for synchronization or just the initials of Q. Thus, our approach unravels the abstractions built into the timeout operator differently than that built into its semantically equivalent version. On the implementation level, P Q is implemented as a timeout (e. g., using a timer), while (P 2 Q) Q models a combination of internal and external influences (independent of time).

In the semantic framework of CSP, timeout is introduced by hiding. As explained above, our understanding of a timeout is somewhat different. Analogously, we deal with hiding different from its treatment on the semantic level of CSP. There, hiding abstracts events such that the following equality holds:

(a → STOP ) \ {a} = STOP .
Nevertheless, in the operational semantics (a → STOP ) \ {a} performs a hidden action before evolving to STOP. Our approach adopts this understanding and takes hidden actions into account. A coordination process like P \ A removes A from the externally visible events and specifies that the system cannot synchronize with its environment on any event from A. However, within P , the events in A are available for synchronization, of course.

A similar argument applies to

a → P 2 a → Q = a → (P Q) .
The left-hand side models a system that offers two similar actions for synchronization but its future depends on the external decision which one of the two exclusive actions is chosen. The right-hand side models a system offering a single action to its environment and then decides internally if it continues as P or as Q. Accordingly, P Q is understood as a system performing an internal action to make the decision between P and Q. Thus, when used in a coordination process, the internal (nondeterministic) choice gives rise to a single internal action whose outcome determines which one of the processes is chosen. There are more reasons for allowing the internal choice to be used in a coordination process. For example, it is quite often the case that nondeterministic models of a system are sufficient to express certain properties (e. g., deadlock-freedom). Once a process is proved to express the interaction requirements of a system it is clearly desirable to take it as the coordination process and to implement the missing details on the level of some programming language instead of further refining the CSP model.

Duration, Conflict and Concurrency

Events are assumed to be instantaneous and atomic. In [START_REF] Hoare | Communicating Sequential Processes[END_REF], Hoare proposes to unravel this abstraction by splitting an event into start and end event to model duration of the original event. Our approach adopts this idea. Events are split into start and end events and the action that realizes the original event is performed between these two. It is important to note that actions can be of arbitrary granularity (i.e. just a few basic operations of a processing unit or a long running service) and may even be internally concurrent. The single requirement is that it is guaranteed to terminate eventually. Furthermore, we believe that concurrency must be distinguished from choice for the purposes of a coordination language. Designers of concurrent systems should be able to specify which parts of a system may be executed simultaneously (truly concurrent) and which are mutual exclusive. For example, the processes

P = a → b → STOP 2 b → a → STOP Q = a → STOP | ∅ | b → STOP
are equivalent in the standard CSP models (e. g., traces, stable failures and failures-divergences) but we think of them as describing different systems. P describes a system that must perform a and b exclusively while Q may perform a and b at the same time. This observation is of theoretical and practical importance for a CSP-based approach to coordination. The theoretical issue is that the standard semantics for CSP are interleaving ones and thus do not distinguish choice from concurrency. The practical issue is that a concurrent program should be able to profit from the gains promised by concurrency instead of being limited to purely sequential runs (due to interleaving).

There are two ways of understanding a CSP event. Either as a hand-shaken communication of parallel processes (or components) or as an abstraction of some sequential action (not necessarily related to communication). The former understanding gives rise to implementations of channels that can be used by software developers to build their programs using CSP-style communication. Operators like hiding or internal choice are not supported by these approaches. As explained above, our approach interprets events as arbitrary actions that are performed between the start and end events of a split event in the coordination process.

Interestingly, as shown in [START_REF] Kleine | Simulating truly concurrent CSP[END_REF], the splitting of events allows us to distinguish choice from concurrency. In that paper, a syntactical transformation T of processes is presented that splits the events in its argument (even the hidden ones) of its input process into start and end events and relabels them in such a way that hidden transitions become observable again. T allows us to determine pairs of possibly concurrent events taking hidden events into account. T distinguishes concurrency from conflict in that start and end events of concurrent events may interleave while conflict relates to exclusive start evens. The transitions x , y ∈ Σ ∪ { , τ }, leading from P to the states P x , P y , P x = P y respectively, are conflicting in P if x cannot fire in P y or y cannot fire in P x . This deliberately includes the case x = y, because events can be auto-conflicting (if they lead to different states). This also extends to τ transitions, because conflicts between those are also possible (as, e. g., in (a → P 2 b → Q) \ {a, b}). Furthermore, T allows us to simulate truly concurrent CSP within the framework of standard interleaving CSP. This is beneficial because these semantics are well-developed, well-documented and supported by a number of industrial-strength tools such as FDR and ProB.

Any of the choices presented in this section is justified by the standard semantics of (untimed) CSP. An important feature is that nondeterminism is supported on the design level but resolved on the implementation level. The advantage is simplicity of reasoning about the design (e. g., deadlock-freedom is often provable on a quite abstract design level).

Designing a Coordination Environment

The ideas presented in the previous section are supported by the transformation T presented in [START_REF] Kleine | Simulating truly concurrent CSP[END_REF]. The transformation splits events into start and end events, introduces fresh hidden actions for internal choices and timeouts, and takes internal transitions into account. T gives rise to a coordination environment that simulates the truly concurrent version of a CSP coordination process at runtime and starts a user-defined function (UDF) after performing the start event of a split event and performs the respective end event after termination of the UDF. A UDF is the implementation of a terminating action provided by the user.

The intent of the coordination environment is to enable coordination of a concurrent system in a noninvasive way separating interaction and data independently from a specific target language.

The notion of noninvasiveness means that existing implementations of components do not need to be modified to be coordinated. The coordination is done on top of the component implementations provided by the user encapsulating the coordinated components, taking their operations as UDFs implementing the actions of the final system.

The separation of interaction and data is important with respect to the modeling of the coordination process (which may involve data but which does not necessarily relate to data being communicated or computed by the actions of the system) and with respect to the final combination of the coordination process with the UDFs of the system. The first aspect means that the variables used in a coordination process are independent of the actual values being communicated and processed by the system (unlike in CSP B [START_REF] Schneider | Verifying Controlled Components[END_REF], for example). The second aspect means that the UDFs being mapped to possibly concurrent events may not modify data being shared amongst themselves.

The design-flow associated with our approach allows the concurrency structure and the UDFs to be developed and verified independently up to the point when the system is assembled to a concrete executable concurrent system (by combining the coordination process with the UDFs implementing the actions). Only then sets of possibly concurrent events must be identified and it must be proved that the UDFs do not introduce data races. This issue is discussed in Section 5. The following subsections present our understanding of how a coordination environment should perform actions and enable actions to be chosen internally or by the environment.

Performing actions

The purpose of the coordination environment is not only to coordinate concurrent parts of a system but also to execute UDFs when performing actions and to assign the execution of UDFs to threads. This is done while performing an event or a τ -transition made visible by T .

Since the simulation of the original process P is defined by the operational firing rules of CSP unrolling T (P ) while hiding the externalized hidden actions and the end events of visible actions, we do not go into details of unrolling the coordination process here. The important point is that the events are regarded as actions which are associated with UDFs and that these UDFs are executed between the atomic steps of the actions start and its end.

The following cases are to be considered when performing an action. The action either corresponds to a (a) synchronized event, (b) to a hidden event, (c) to a renamed event, or (d) to any other event.

The first case (a) is commonly considered to be a problem when matching actions with events. The argument against performing actions for synchronized events is the following question: "which of the synchronized components should perform the action?" This question remained unanswered for some systems. For example the process analysis toolkit PAT [START_REF] Sun | Model Checking CSP Revisited: Introducing a Process Analysis Toolkit[END_REF] allows events -except synchronization events -to be associated with UDFs. Our answer to this question (and our argument in favor of performing actions for synchronized events) is that synchronization primarily affects the order of events and not their ownership. Thus, a single action is performed after the start event in an arbitrarily chosen context (either one of the threads performing the preceding actions, possibly another).

In the second case (b) the original event (being subject to hiding) defines the action to be performed. In the third case (c) the renamed event (not the original one) defines the action to be performed. Although this decision seems to be at odds with case (b), because both renaming and hiding can be regarded as a substitution of the original event's name (in a user-defined way or by τ respectively), the different treatments are necessary for uniquely identifying the UDFs to be executed. The reason is that hidden events cannot be synchronized on but renamed events are available for synchronization.

In the last case, the event directly identifies the UDF to be performed. It is noteworthy, however, that is not associated with a UDF. It solely models termination of a process, is commonly considered to be outside the alphabet of a process, and it is the only event not being split by T .

As an example, the single UDF to be performed by the following coordination process P (being algebraically equivalent to SKIP ) is the one identified by event

a. P = ((b → SKIP )[b ← a] | {a} | a → SKIP ) \ {a}
This design decisions described above allow us to relinquish the idea that a sequential process models a single thread of control. A sequential process defines the order of its actions but these can be performed by different threads. This gives us great freedom in distributing the actions amongst processing units of the final system. Load balancing could, for example, be realized by statically creating a task queue and distributing the actions dynamically at runtime. Any of these informal descriptions above conforms to the formal definition of T .

Choosing Events

There must be some additional component added to the coordination environment dealing with the execution of hidden events. Visible events are available for external synchronization and chosen externally. But how to resolve conflicts of hidden actions?

Our solution is to use event listeners that reside above the component performing T (P ) and below the one realizing the hiding of externalized hidden actions and the end events of actions. This way, it can be ensured that the e and eh events are immediately performed so that T (P ) can proceed and offer any causally dependent s and sh events. The strategy how to choose amongst sh events, however, must be provided by the user of our coordination approach. Like the UDFs realizing the resolution of internal choices, listeners are to be injected into the coordination environment to deal with sh events introduced by hiding (those not being introduced by internal choice or timeout).

This leaves it open to the programmer to decide if hidden actions have priority over visible ones as, e. g., in the tau-priority model presented in [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF], and how conflicts of hidden actions are resolved.

It is important to notice that this does not contradict non-invasiveness of our approach. By making hidden events on the outermost process available for internal event listeners, we provide a general way for resolving nondeterminism.

Detecting Data Races

CSP can be used as a coordination language independent of the target language. Thus, we do not consider a particular specification language for the UDFs here and present a purely mathematical proof obligation to ensure freedom of data races in a coordinated system. It is defined as a so-called frame property, based on our notion of possible concurrency (as presented in [START_REF] Kleine | Simulating truly concurrent CSP[END_REF]), describing the modification behavior of a UDF with respect to another UDF. Refer to [START_REF] Müller | Modular specification and verification of object-oriented programs[END_REF] for a more in-depth presentation of framing.

Let F be the type of all UDFs and Var the type of all modifiable entities (references to objects and primitive types). The mapping of events to UDFs is formally defined as a partial injective function such that its inverse is a total injection. It is

udf : Σ F ,
and its inverse is

udf -1 : F Σ .
Hence, a UDF uniquely identifies an event but events do not necessarily identify a UDF. A data race is formally expressed using the following functions:

shared : F × F → P Var shared (f , g) = (writes(f ) ∩ rw (g)) ∪ (writes(g) ∩ rw (f ))
writes, reads, rw :

F → P Var rw (f ) = writes(f ) ∪ reads(f )
Two UDFs f and g suffer from a data race if their frames overlap and one modifies data also read or written by the other.

race(f , g) = shared (f , g) = ∅
Let conc : Σ × Σ → Bool be the predicate telling us whether or not two events are possibly concurrent in a given process P (i. e., conc(x , y) ↔ (x , y) ∈ conc(P )). This predicate is combined with udf -1 to the following predicate telling us whether or not two UDFs are possibly concurrent:

conc F : F × F → Bool , where conc F (f , g) = conc(udf -1 (f ), udf -1 (g)) .
The proof obligation ensuring freedom of data races is

∀ f , g ∈ F : conc F (f , g) ⇒ ¬ race(f , g) .
A system violating this condition can be corrected by either adjusting the coordination process (by removing possible simultaneity) or modifying the UDFs (by making the frames distinct).

In general, determining the sets reads and writes of arbitrary UDFs is a hard problem (due to aliasing). Dealing with this issue is beyond the scope of the work presented here. However, it is noteworthy that specialized logics such as separation logic [START_REF] Reynolds | Separation logic: a logic for shared mutable data structures[END_REF] offer a prospective alternative for specifying (and verifying) properties such as the data independence of UDFs.

Besides this data related proof obligation, it must be proved that the UDFs are never called outside their preconditions and that they are guaranteed to terminate to obtain total correctness of a system. Furthermore, it must be proved that the UDFs resolving nondeterministic choices always return a valid process name.

As motivated in the Introduction, the sequential terminating UDFs implementing the sequential parts of the program are oblivious to concurrency modulo the proof obligation presented above. This means that our approach is noninvasive and allows us to turn a verified sequential system into a concurrent one by identifying parts of the program that make up the UDFs, adding a suitable CSP script and mapping events to UDFs. Provided that the additional proofobligation can be discharged successfully, modular verification remains valid on that program. This implies that the sequential parts do not have to be modified at all. The coordination environment is the entry point to the final program and solely requires implementation of the mapping from events to UDFs.

Supported Processes

The approach presented here supports all finite alphabet CSP processes except the ill-formed recursive process P = P (which is sometimes understood as div ). This includes infinite state processes as well as diverging ones. The limitation to processes whose alphabet is finite matches the assumption that there are only finitely many UDFs assigned to the events of a process. Our approach to simulation is capable of dealing with any CSP process whose alphabet is finite. Consider the following divergent processes:

P = µ P • (e → P ) \ {e} and Q = µ Q • (e → Q SKIP ) \ {e} .
P models a process that runs forever without any interaction with its environment. This is not a problem in its own right, because, as shown in our case-study on modeling and implementing a workflow server in CSP [START_REF] Kleine | Specification, Verification and Implementation of Business Processes using CSP[END_REF], divergence may naturally arise when modeling server processes. Q may also diverge, but may as well eventually decide to terminate gracefully. The reason for accepting such processes is that the internal actions resolving the choices can be used to implement local fairness conditions. The notion of fairness conditions refers to conditions that 'cure' processes that behave badly under the assumption that repeated (local) choices can always be resolved in the same way. The fact that this is unlikely to happen in reality is expressed by fairness. FDR does not support fairness but PAT explicitly deals with fairness, as described in [START_REF] Sun | PAT: Towards Flexible Verification under Fairness[END_REF]. Fairness can be specified on different levels of granularities (e. g., local or global) and can be regarded as an abstraction of probabilities.

Consequently, the process Q shown above is not necessarily diverging and might be guaranteed to terminate eventually under certain fairness assumptions. The same applies to other processes containing process control constructs such as internal or external choice, timeout or interrupt allowing the process to eventually exit from cycles of hidden actions.

Both tools FDR and ProB can be used to verify that P unavoidably diverges while Q may eventually terminate. FDR proves this in the traces model because

T P = { } and T Q = { , } .
In the failures-divergences model P = Q because both processes may diverge initially.

The same result can be obtained using the LTL model checking capabilities of ProB. In ProB's LTL syntax, the formula φ = F G [tau] states that a process unavoidably diverges (all of its executions eventually end up in an endless cycle of τ events). Now

P |= φ but Q |= φ .
The counterexample found by ProB expectedly shows that Q may eventually perform . Another interesting example is the infinite state process

R = µ R • (a → R ||| b → STOP ) .
It can be simulated although it is obviously questionable if any reasonable program conforming to this design exists. Infinite state processes such as R are likely to eventually run out of memory, crashing the whole system. Now, the same mechanism that can be used to implement fairness can be facilitated to turn theoretically infinite state processes into finite state processes. However, this requires knowledge of the structure of the processes when implementing the UDF resolving the internal choices. In the example of process R, the relevant UDF could count the a's and always choose the b if a certain bound is reached.

In this context it is important to observe that CSP M scripts modeling infinite state systems cannot in general be checked by FDR because compilation of the script to the internal LTS will not terminate. The ProB LTL model checker, however, performs on-the-fly model checking and quite often succeeds in model checking infinite-state systems [START_REF] Plagge | Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more[END_REF].

Implementation and Further Work

The coordination model presented here is given in a target language independent way. In this section, we present its implementation for the target language Java. It simulates a coordination process at runtime and executes user-defined Java code when performing an event. For now, it implements the operational semantics of the process operators prefixing, sequential composition, internal choice, external choice, generalized parallel, timeout, interrupt, hiding, and renaming.

The coordination environment provides the final class CspEnvironment encapsulating the coordination process. This class manages the events offered by the coordination process, listeners that deal with changes of offered events, and the mapping of events to UDFs. The mapping of events to UDFs is defined by an implementation of the CspEventExecutor interface. The environment immutably references a single instance of a CspProcessStore holding the process configurations that describes the coordination process to be simulated. The environment instance is the only object that the implementation synchronizes on when performing the atomic start and end transitions modeling an event of the coordination process. The start transitions of visible events are available for external synchronization, while start transitions of hidden events are only accessible for event listeners. The end transitions are performed immediately after termination of the action's UDF.

The CspEnvironment provides a start method taking a process name that determines the coordination process instance. When started, the environment retrieves the coordination process from its store and adds the events offered by the process to its set of offered events. Then it informs the event listeners about that change. From that point on, interaction with the coordination environment is done by choosing events from the set of offered events and performing them. Subsequently the listeners are performed after every change of the set of events offered by the outermost process. This set changes only when an event is performed. If a client holds a reference to an event that is no longer available, it cannot be performed, of course (resulting in a no-op).

To create an executable system one has to instantiate a CspEnvironment with a CspProcessStore and a CspEventExecutor . One can then create a coordinated system as shown in Figure 1. A CspSimulator may be used to connect a CspEnvironment to the outside world. One useful example is the SwingCspSimulator that provides a simple Swing GUI to chose and perform events.

The example code shown in Figure 1 assumes the existence of suitable CspEventExecutor and Filter classes (filters are convenience objects helping event listeners to find the events that they act upon). The instances may be configured to fit the needs of the final system. Then a process store is created and must be filled with process configurations. A CspEnvironment is created using the CspEventExecutor and CspProcessStore instances. To deal with possibly hidden events, a CspEventConsumer takes the Filter instance as argument and is registered as a listener for event changes at the environment. Finally, the environment is run using a Swing GUI. Our implementation handles the nesting of process operators and the offered (initial) events of processes in an explicit way. This causes a considerable runtime overhead but allows us to resolve conflicts of actions when an action is started and to leave concurrent actions on offer while an action is performing.

The workflow server presented in [START_REF] Kleine | Specification, Verification and Implementation of Business Processes using CSP[END_REF] is built using this coordination environment. The workflow server accepts workflow definitions that are implemented in the same way and uses FDR to verify workflow definitions before activating them.

Extending the implementation towards the coordination of distributed systems is subject to future work. Explicit support for data storage and communication by the coordination environment is another concern that deserves further

CspEventExecutor c e e = . . . ; F i l t e r f i l t e r = . . . ; // s e t u p c e e and f i l t e r C s p P r o c e s s S t o r e s t o r e = new C s p P r o c e s s S t o r e ( ) ; // r e g i s t e r p r o c e s s c o n f i g u r a t i o n s CspEnvironment env = new CspEnvironment ( s t o r e , c e e ) ; env . r e g i s t e r L i s t e n e r (new CspEventConsumer ( f i l t e r ) ) ; CspSimulator s = new SwingCspSimulator ( "my example " , env ) ; s . run ( ) ; investigation. We also strive for a deeper integration with the functional verification of UDFs. Development of specialized provers for the conflict-freedom proof obligation is also subject to future work.

Related Work

Linda [START_REF] Ahuja | Linda and Friends[END_REF] is a parallel programming language that adds parallelism to sequential languages (e. g., C, Fortran, etc) and allows tasks to be distributed dynamically at runtime. Like Linda, our approach separates concurrency concerns from sequential ones in a machine-and language-independent way. In contrast to Linda, it builds on ordinary shared memory communication (as built into the underlying language) instead of a special memory model (the so-called tuplespace). Moreover, our approach is based on a formal method that is supported by a number of industrial-strength tools.

Reference Nets [START_REF] Kummer | Referenznetze[END_REF] provide an object-oriented High-Level Petri Net formalism where instances of Petri Nets carry references to other instances of Petri Nets instead of tokens. In that model, the firing of a transition moves a reference from one place to another. The concept of synchronous channels allows Petri Net instances to communicate when a transition fires. Reference Nets extend this to the execution of arbitrary (terminating) Java code. Thus, in that model, a Petri Net can be regarded as the coordination process of a system and the code attached to transitions relates to our understanding of actions. Unlike our approach, Reference Nets do not support verification of the coordination process and lack proof obligations relating the ordering of Petri Net transitions (as defined by their firing sequences) to the pre-and postconditions of their associated implementations, for example.

Another formal approach to the modeling and verification of distributed component based systems is described by Baier et al. [START_REF] Baier | A Uniform Framework for Modeling and Verifying Components and Connectors[END_REF]. Their approach is based on the model checker Vereofy which supports multiple input languages capable of modeling concurrent systems. However, their approach does not extend to implementing such systems but remains on the modeling level.

CSP++ [START_REF] Gardner | Converging CSP specifications and C++ programming via selective formalism[END_REF] and JCSP [START_REF] Welch | Process Oriented Design for Java: Concurrency for All[END_REF] offer CSP-like channels as inter-thread communication facilities but realize only a limited set of CSP operators. The feature that distinguishes our approach from CSP-based software libraries is that events are not interpreted as communications over a typed channel but as abstractions of arbitrary actions. It realizes the common understanding that an action can be modeled by a start and an end event (and the action executing between these two). Furthermore, the CSP model is simulated at runtime to drive the concurrent application.

Since sequential processes in CSP are viewed as executions of computational entities whose behavior can be observed in terms of events, it is natural to map a single sequential process to its own thread. This is the general idea underlying CSP++ and JCSP. Our approach does not necessarily map two causally dependent threads to the same thread. It merely maintains the order of UDFs as defined by the events of the CSP script coordinating the system. This is comparable to Linda's feature of distributing tasks at runtime.

Conclusions

In this paper, our approach to using CSP as a coordination language is presented. It unravels the various abstractions that are carefully built into CSP for the purpose of coordinating concurrent systems in a noninvasive way. The approach taken here is quite different from other approaches to implementing CSP because it does not built on the channel concept which is a common approach realizing the hand-shaken communication. Instead, our approach is based on atomic steps denoting start-and endpoints of a system's actions. It also deals with internal (hidden) actions. Associating the resolution of internal choices with UDFs undoes nondeterminism inherent to the CSP model coordinating the program. This allows us, for example, to turn systems that are not fair in the standard CSP semantics into fair ones.

The semantic foundation of the coordination runtime environment is given by a syntactic process transformation turning a standard interleaving CSP process into a truly concurrent one. The transformation also allows us to predict which functions are possibly executed in parallel. Dependent on possibly concurrent events we stated a proof obligation for ensuring absence of data races.

Our approach allows us to separate concurrency issues from sequential ones, and to reuse the concurrent design of the system at runtime. It also enables us to use state-of-the-art CSP tools such as FDR [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF] and ProB [START_REF] Leuschel | Probing the Depths of CSP-M: A new FDRcompliant Validation Tool[END_REF] for the automated verification of concurrency aspects of the software, and integrates with modular verification of UDFs. The use of CSP makes it especially well suited for systems with highly communicative concurrent components.

Compared to other CSP implementations, the approach presented here supports a richer CSP in terms of supported process operators. Unlike other CSP library-level implementations, our approach is noninvasive. It allows the system's basic actions to be coordinated very directly. Our approach is capable of handling infinite state and divergent processes. Compared to other coordination languages, ours has the advantage of its strong integration with formal methods.

Fig. 1 .

 1 Fig. 1. Code stub of a coordinated Java program.

However, this comes at the cost of the runtime overhead of explicitly managing processes and events caused by simulation of CSP.