Marco Krauweel

Sung-Shik T Q Jongmans

Simpler Coordination of JavaScript Web Workers

JavaScript is a popular sequential language for implementing Web applications. To enable concurrent execution of JavaScript code, modern JavaScript engines support the Web Workers API. Using this API, developers can spawn concurrent background workers from a distinguished main worker. These workers, which run on the same machine (e.g., to exploit multicore), interact via message-passing. The Web Workers API is relatively low-level, which makes implementing coordination protocols among background workers laborious and errorprone. To simplify this, we propose to hide the Web Workers API behind a coordination language that provides higher-level constructs. Importantly, developers already use JavaScript together with domain-specific languages HTML (for markup/structure) and CSS (for style/design); another domain-specific language (for coordination) seamlessly fits this practice. Using the coordination language Reo, we demonstrate the advantages and feasibility of this approach by example. We also present the necessary tool support (compiler; runtime library and API; front-end).

Introduction

Context. JavaScript [7] is a sequential language originally invented to add dynamic behavior to static Web pages. Together with domain-specific languages HTML and CSS, JavaScript has become one of the most widely used languages for implementing Web application clients. In recent years, JavaScript was popularized also for writing server-side code and mobile apps. This makes JavaScript a key language in contemporary software engineering.

Single pieces of JavaScript code are executed sequentially. To concurrently execute multiple pieces of JavaScript code on the same machine (e.g., to exploit a multicore processor), modern JavaScript engines support also the Web Workers API [9]. This API "allows Web application authors to spawn background workers running scripts in parallel to their main page", which "allows for thread-like operation with message-passing as the coordination mechanism."

Problem. The Web Workers API is relatively low-level.

First, the Web Workers API provides no constructs for background workers to send messages directly to each other; background workers can send messages only to a distinguished main worker ("hierarchical communication" [START_REF] Myter | Many Spiders Make a Better Web: A Unified Web-Based Actor Framework[END_REF]). Second, the Web Workers API provides no constructs for a background worker to correlate messages sent to, and later received from, the main worker; workers cannot reply to messages. Third, the Web Workers API provides no constructs for a background worker to pause processing of the current message in anticipation of receiving the next message; background workers cannot block.

Thus, sending messages end-to-end, replying to messages, and awaiting messages, can be implemented only in terms of lower-level constructs. This is laborious and error-prone. For instance, it is already nontrivial to implement a background worker that simply needs to send a message to, and await a reply from, another background worker as part of the same task.

Contribution. To simplify implementing coordination protocols using the lowlevel Web Workers API, we propose to provide developers additional higher-level constructs. Such constructs have, in fact, been under development already for decades, in coordination languages. We therefore propose to hide the Web Workers API behind a coordination language. An observation particularly relevant to this approach is that developers already use JavaScript together with domainspecific languages HTML (for markup/structure) and CSS (for style/design); another domain-specific language (for coordination) seamlessly fits this practice.

In Sect. 2, we present preliminaries on JavaScript and the Web Workers API. In Sect. 3, we illustrate the limitations of the Web Workers API. In Sect. 4, we describe the existing coordination language Reo [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, The Magic Protocol[END_REF]. In Sect. 5, we demonstrate how the use of Reo to hide the Web Workers API alleviates its limitations, in theory. In Sect. 6, we present tool support (compiler; runtime library and API; front-end) for developers to implement and run coordination protocols using Reo. In Sect. 7, we demonstrate the feasibility of our approach, in practice. Section 8 concludes this paper, including related work. To our knowledge, this is the first paper that presents high-level constructs to simplify implementing coordination protocols among background workers in JavaScript and the Web Workers API.

2 JavaScript and the Web Workers API -JavaScript provides first-class functions and the usual control constructs [7].

-The Web Workers API provides constructs for spawning background workers from a main worker and constructs for sending/receiving messages [9].

Together, JavaScript and the Web Workers API constitute an actor language in the style of active objects, in the taxonomy of De Koster et al. [START_REF] De Koster | 43 Years of Actors: A Taxonomy of Actor Models and Their Key Properties[END_REF].

Every worker starts by performing some initial work (e.g., initializing variables). It then checks if, in the meanwhile, events have occurred that require processing. Examples include message events (i.e., receipt of a message) and timeout events (i.e., passage of time). If so, the worker executes event listeners in response, until all events have been processed; otherwise, it suspends until the next event occurs. Execution of event listeners is nonblocking and nonpreemptive: event listeners run to completion in one go, uninterleaved with other event listeners of the same worker. A worker has an event handler for every type of event that it responds to. For instance, every background worker has a message event listener to process messages received from the main worker; as background workers cannot receive messages directly from each other, no other message event listeners are necessary. Conversely, the main worker receives messages from all background workers, and it may need to respond differently to each of them; the main worker, therefore, may have multiple message event listeners. Although many types of events exist, only message and timeout events matter in this paper, w.l.o.g. A worker's cycle of awaiting and processing of events is called its event loop, and it is repeated indefinitely; pending event listeners are stored in a private FIFO queue. Furthermore, every worker has its own private heap. No memory is shared; message-passsing is the only means of communication.

Example 1. Figures 12show an example program. This program defines two background workers, called Ping and Pong, who iteratively send "ping" and "pong" to each other. Syntactically, a message event handler is a function, where parameter e represents a message event to be processed; the message is accessed through e.data. postMessage(m) sends message m. setTimeout(f,t) generates a timeout after t milliseconds; subsequently, function f is called.

Figure 2 defines Ping (and Pong). Initially, Ping only sets his message event handler (line 1-9); subsequently, he suspends. Whenever Ping receives a "pong" message from the main worker, he resumes by sending back a "ping" message, after a 1000 milliseconds delay (lines 6-8); subsequently, he suspends again.

Figure 1 defines the main worker. Initially, the main worker spawns Ping and Pong (lines 1-2), then it sets its message event handlers (lines 4-7), then it sends an initial "pong" message to Ping (line 9); subsequently, it suspends. Whenever the main worker receives a message from Ping or Pong, it resumes by forwarding that message to Pong or Ping; subsequently, it suspends again.

Note that the main worker must call postMessage on a particular background worker, to indicate the receiver. In contrast, background workers do not need to call postMessage on the main worker; as background workers can send messages only to the main worker, no confusion can arise about who is the receiver. Figure 5 defines Bob. Initially, Bob sets an empty list of pending serial numbers (line 1) and sets his message event handler (lines 15-21); subsequently he suspends. Whenever Bob receives a message, he resumes. If Bob does not recognize the serial number in the message (line 17), he starts a new processing cycle for that serial number (line 18); otherwise, he continues a previous processing cycle (line 20). In the former case, Bob processes the initial value to a final value (line 4), then he sends a message to the main worker (lines 5-6), who forwards it to Carol, then he registers the serial number (line 7); subsequently, he suspends again. In the latter case, Bob unregisters the serial number (line 11) and finalizes his processing cycle (line 12); subsequently, he suspends again.

Figure 3 defines the main worker. The main worker unconditionally forwards messages received from Alice to Bob (line 7). As such, Alice communicates to Bob via an unbounded buffer. In contrast, the main worker forwards messages received from Bob to Carol (line 13) only if the number of buffered messages i is smaller than a bound n (line 11). As such, Bob communicates with Carol via an n-capacity buffer (e.g., to avoid excessive memory usage if Carol is slower than Bob, and many large message from Bob would otherwise need to be buffered). To prevent loss of messages, the main worker acknowledges a serial number sn to Bob only once the corresponding message can be forwarded (line 12); Bob awaits this acknowledgment before beginning the second half of its processing cycle for sn. As such, the n-capacity buffer is blocking. If the main worker cannot forward a message yet, it schedules an immediate retry (lines [START_REF] Jongmans | Automata-Theoretic Protocol Programming[END_REF][START_REF] Jongmans | PrDK: Protocol Programming with Automata[END_REF]. 3This example program illustrates the limitations of the Web Workers API, stated in Sect. 1. First, it illustrates that background workers cannot directly send to, and receive from, each other. In particular, background workers cannot obtain references to other background workers. Second, this example program illustrates that background workers cannot directly understand replies to messages. In particular, whenever Bob receives from the main worker a reply (acknowledgment) to an earlier message, the context in which he sent that message is gone; to Bob, the reply might just as well be a new forwarded message from Alice. This is why messages need to be explicitly tagged with a serial number and why Bob needs to do extra bookkeeping. Third, this example program illustrates that background workers cannot straightforwardly block. In particular, after Bob sends a message to the main worker, he needs to await an acknowledgment, but the only means of waiting is through suspension and resumption (event loop). As a result, Bob's processing cycle is unnaturally split into two functions.

The coordination protocol between Bob and Carol in the previous example is among the simplest: asynchronous communication through a blocking FIFO buffer of bounded capacity. Yet, due to limitations of the Web Workers API, the implementation of this simple coordination protocol is not that simple at all: as higher-level constructs are missing (sending message end-to-end, replying to messages, awaiting messages), key characteristics can be expressed only indirectly (through forwarding, through serial numbers, through split functions). This makes development laborious and error-prone.

Another issue is that "computation code" is entangled with "coordination code". This lack of separation and modularity between computation and coordination complicates development. For instance, changing the implementation of a coordination protocol typically requires global understanding of, and modifications to, larger parts of a program; it cannot be localized, because implementations of coordination protocols are scattered across multiple workers. Moreover, reusing the implementation of a coordination protocol in other programs typically requires so much effort that it is practically infeasible. Example 3. Suppose that we want to instantiate two Bobs instead of only one (e.g., because Alice and Carol are twice as fast as Bob). Effectively, then, we need to generalize the coordination protocol between Alice and Bob to multiple readers, and the coordination protocol between Bob and Carol to multiple writers. Figure 7 shows modifications to the main worker to achieve this. 3 Additionally, we crucially need to insert a postMessage({}) call between lines 12 and 13 in Fig. 5, through which a Bob informs the main worker that he is ready for the next message. The latter illustrates that modifications cannot be localized to one specific piece of code; global understanding and modifications are necessary.

For more complex coordination protocols (e.g., tighter synchronization, many control states), the impact of these limitations and issues becomes only more serious. This is why we propose to provide developers additional higher-level constructs that hide the low-level Web Workers API. Next, we present an existing coordination language that achieves this aim.

Reo

Reo [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Arbab | Puff, The Magic Protocol[END_REF] is a graphical language for compositional construction of coordination protocols, manifested as circuits. Briefly, a circuit is a graph-like structure consisting of typed channels (decorated edges), through which values flow, and nodes (vertices), on which channel ends coincide. Figure 8 shows examples.

Every channel has a type, graphically indicated by (the absence of) a decoration. The type of a channel determines how values flow through it-its behavior.

Name Syntax

Semantics

sync e1 e2
Synchronously accepts a value through e1 and offers that value through e2.

syncdrain e1 e2
Synchronously accepts and loses values through e1 and e2.

fifo1 e1 e2 e1 e2
Asynchronously accepts a value v through e1 and stores v in a buffer , then offers v through e2 and clears the buffer . A token means that a buffer is initially filled with a random v. A source end accepts values into its channel, while a sink end offers values out of its channel. A channel in Reo has either two source ends, or two sink ends, or a source and a sink end. Table 1 shows common channels types. Users of Reo may extend this set by defining their own channels (modeled in some formalism [START_REF] Jongmans | Overview of Thirty Semantic Formalisms for Reo[END_REF]).

The behavior of a node depends on its coincident channel ends.

-A node with only coincident source ends is a source node. A source node is linked to an output port of a worker. By performing a put(v) operation on an output port, a worker attempts to offer value v to the linked source node.

As soon as each of the coincident source ends of the source node is ready to accept v, it synchronously replicates v into all of them, and the put returns; until then, the pending put blocks the worker. -A node with only coincident sink ends is a sink node. A sink node is linked to an input port of a worker. By performing a get operation on an input port, a worker attempts to accept a value from the linked sink node. As soon as at least one of the coincident sink ends of the sink node is ready to offer a value, the sink node nondeterministically selects a value v from one of them, and the get returns v; until then, the pending get blocks the worker. -The source and sink nodes of a circuit are its boundary nodes (light-gray color). A node on which both source and sink ends coincide is a mixed node (dark-gray color). Mixed nodes combine the behavior of source and sink nodes: synchronously, a mixed node nondeterministically selects a coincident sink end and replicates its value into all coincident source ends. Nodes cannot temporarily store, generate, or lose values.

Before a value can flow through a circuit, its channels and nodes must first reach consensus about their local behavior to ensure consistent global behavior. For instance, a node should not locally (decide to) replicate a value into the coincident source end of a fifo channel if the buffer of that channel is full.

Example 4. The circuit in Fig. 8a implements the coordination protocol between Alice and Bob in Ex. 2; the circuit in Fig. 8b implements the coordination protocol between Bob and Carol in Ex. 2. This shows that Reo is expressive enough to define both nonblocking coordination protocols (e.g., between Alice and Bob) and blocking ones (e.g., between Bob and Carol); ultimately, the programmer decides what kind of communication is needed. The circuit in Fig. 8c implements the coordination protocol between the two Bobs and Carol in Ex. 3.

The circuit in Fig. 8c works as follows. For a put(v) operation performed on the top-left source node to return, this node must replicate v into the coincident source end of the sync channel. This is possible only if the sync channel accepts v, which depends on whether it can synchronously offer v through its sink end to the connected mixed node. This is possible only if the mixed node accepts v, which depends both on its nondeterministic selection and on whether it can synchronously replicate v into the coincident source end of the fifon channel. The latter is possible only if the fifon channel accepts v, which depends on whether its buffer is not full. Thus, only if the mixed node makes the "right" nondeterministic selection and the buffer is not full, only then flows v synchronously from the topleft source node into the buffer (and put(v) returns).

Once the buffer is full, no value can flow from either of the two source nodes into the buffer. The only thing that can happen at this point is the flow of a value out of the buffer to the sink node. Subsequently, because the buffer is not full anymore, a value can flow from one of the two source nodes into the buffer.

For Java developers to use Reo to implement and run coordination protocols, a Reo-to-Java compiler, a Reo@Java runtime library, and a Reo@Java API exist [START_REF] Jongmans | Automata-Theoretic Protocol Programming[END_REF][START_REF] Jongmans | PrDK: Protocol Programming with Automata[END_REF]. The idea is that developers implement workers as Java classes and coordination protocols as Reo circuits. Then, the Reo-to-Java compiler computes the semantics of the Reo circuits as state machines (more precisely, as constraint automata [START_REF] Baier | Modeling component connectors in Reo by constraint automata[END_REF][START_REF] Jongmans | Automata-Theoretic Protocol Programming[END_REF]), and it generates Java classes for their runtime simulation.

At runtime, every hand-written worker object, and every compiler-generated state machine object, runs in its own Java thread. Through the Reo@Java API, every worker object has access to (data structures for) ports, on which it can perform put and get operations. State machine objects monitor those ports: whenever a worker object performs a put or get on one of its ports, a designated state machine object checks whether this operation enables a transition out of its current state; every transition represents a synchronous flow of values among ports. If so, the state machine object makes the transition, distributes values accordingly among participating ports, and completes all put and get operations involved; if not, the state machine object does nothing and awaits the next put or get. In accordance with the blocking nature of put and get, the execution of worker objects is suspended so long as their puts and gets are pending. The Reo@Java runtime library provides an implementation of the Reo@Java API. Reo enables developers to implement coordination protocols in terms of domainspecific abstractions and higher-level constructs. As a coordination language that hides the low-level Web Workers API, use of Reo has two main implications.

The first implication is the adoption of a syntactic separation between computation and coordination: developers should implement workers in JavaScript, while they should implement coordination protocols purely in Reo. This separation leads to modularization (of workers and coordination protocols), which has well-known advantages [START_REF] Parnas | On the Criteria To Be Used in Decomposing Systems into Modules[END_REF], including improved changeability and reusability. The second implication is that programmers should no longer implement communications with nonblocking postMessage from the existing Web Workers API, but with blocking put and get from our new Reo@JS API. If necessary, as demonstrated in Ex. 4, put and get can effectively be made nonblocking by connecting them to a circuit with fifo buffers. Of course, nothing prevents programmers from implementing additional "covert communications" among background workers in an indirect way (e.g., using message channels or sockets), but this is against the philosophy of our approach and therefore discouraged.

Example 5. Figure 9 shows implementations of Alice, Bob, and Carol in the example program from Ex. 2, using the Reo@JS API instead of the Web Workers API. Alice, Bob, and Carol are now implemented as functions, with output ports and input ports as parameters. As put and get are blocking, especially function bob is significantly simpler than the code in Fig. 5 (fewer details to worry about).

Figure 10 shows implementations of the coordination protocols between Alice and Bob, and between Bob and Carol. This diagram also defines which workers the program consists of, by which functions those workers are defined, and how workers' ports are linked to boundary nodes. Using higher-level constructs to express coordination, as in Reo, developers are relieved from the burden of working with low-level constructs provided by the Web Workers API.

Example 6. Figure 11 shows implementations of the coordination protocols between Alice and the two Bobs, and between the two Bobs and Carol, in the example program from Ex. 3. The "crossed" mixed node replicates a value into only one of its coincident source ends (instead of all), selected nondeterministically. 4 Notably, Alice, the two Bobs, and Carol are defined by exactly the same functions as those in Fig. 9. Such reusability is one of the advantages of separating computation from coordination. Figure 12 shows an implementation of a different coordination protocol between Alice and the two Bobs, where every Bob now has its own unbounded buffer (instead of them sharing one). Making these modifications at this level of abstraction is simple; at the level of abstraction of the Web Workers API, it is not. Figure 13 shows an implementation of yet a different coordination protocol between Alice and the two Bobs, where values from Alice are divided evenly over the two buffers (not guaranteed with Fig. 12). The circuits in Fig. 11 are built from (the two simple) circuits in Fig. 10. This shows that not only can coordination protocols be reused, but in fact, they can be further composed into more complex ones. In plain JavaScript and the Web Workers API, reusing and composing existing implementations of coordination protocols is practically infeasible.

Examples 5-6 show how the limitations and issues of the Web Workers API (Sect. 3) are alleviated when a coordination language, such as Reo, is used. Hiding the Web Workers API behind Reo makes both workers and coordination protocols simpler to implement, easier to change, and easier to reuse, in theory. To actually reap these advantages in practice, developers need tool support. We present such tools in the next section, to show that our approach is also feasible.

Tool Support

Overview. For developers to use Reo to implement and run coordination protocols, they need a compiler and a runtime library. The "easy part" was developing our new Reo-to-JS compiler, which works much in the same way as the existing Reo-to-Java compiler. The "hard part" was developing our new Reo@JS runtime library, which differs significantly from its Java counterpart.

Compiler. Most of the internals of the new Reo-to-JS compiler are reused from the existing Reo-to-Java compiler (see Sect. 4). In particular, computation and optimization of state machines for Reo circuits is independent of the target language and works in exactly the same way for JavaScript as for Java.

The JavaScript code generated by the Reo-to-JS compiler is also conceptually similar to the Java code generated by the Reo-to-Java compiler: in the same event-driven way as explained in Sect. 4, the generated JavaScript code simulates a computed state machine. This state machine is executed by the main worker.

The Reo-to-JS compiler also generates "wrappers" around the functions that are linked to the boundary nodes of the circuit; these wrappers are executed in separate background workers, using the Web Workers API. All necessary initialization code is also generated. Thus, the only code that developers need to write by hand are the functions that link to the boundary nodes (e.g., Fig. 9).

Runtime library. The new Reo@JS runtime library contains auxiliary code that simplifies and reduces the amount of code that needs to be generated. Most of this code is similar to the code in the existing Reo@Java runtime library. The two runtime libraries significantly differ, however, in their implementation of ports, and particularly, the implementations of put and get. This is because Java differs from JavaScript and the Web Workers API in two significant ways: Java supports shared-memory concurrency and blocking constructs, which JavaScript and the Web Workers API do not support. Shared memory in Java enables straightforwardly linking worker objects to state machine objects by sharing the same port objects between them; this is not possible in JavaScript. Blocking operations in Java make implementing the blocking semantics of put and get straightforward; this is also not possible in JavaScript.

We first explain our solution to the unshared memory complication. The idea is to use two sets of output ports and input ports: one set for background workers, and another set for the main worker. Figures 1415show simplified 5 loop(runMultiplier(/* ports */), null null null); Fig. 18: Looping on promises inside the constructor, the executor is called with a resolve (function) as parameter. The resolve is called once the asynchronous computation finishes. Initially, the resolve is empty. To "fill" the resolve, then can be called on the created Promise object with a callback (function) as parameter. If the resolve has already run at that point, the callback is immediately run; otherwise, the resolve is filled with a call to the callback (which runs as soon as the asynchronous computation finishes). Technically, then returns another Promise object, making it possible to express a sequence of seemingly blocking computations by successively calling then. Such a chain of then calls nests promises in promises, which asynchronously-interrupted in the event loop-resolve one after the other.

Example 7. As shown in Fig. 14, get returns a new Promise object; the same holds for put. Figure 16 shows what a worker looks like if developers were to express computations directly with promises. Note that the callbacks for the two get operations have a formal parameter val (which contains, conceptually, the value offered by the circuit); the actual parameter is passed on line 17, Fig. 14 (at which point this.r refers to the callback).

The previous example shows that using promises to implement blocking, still places a heavy burden on developers. To simplify this, we use generators. A generator is a function that can be exited and re-entered: whenever a yield is encountered during the execution of a generator, the context is saved, and the generator is exited (optionally yielding a result). When the generator is later re-entered, its saved context is restored, and it proceeds from where it left off.

We require that workers are implemented as generators instead of as normal functions (indicated with an asterix), and that put and get are always used together with yield. Subsequently, we can apply promise-based asynchronous task running [START_REF] Zakas | Promises and Asynchronous Programming[END_REF], where every background worker calls its generator, waits until a promise from put or get is yielded, provides this promise a callback in which the generator is re-entered, and suspends; the provided callback ensures that this process repeats itself until the generator is done. Figure 18 shows this approach in code. In this way, every background worker effectively runs a loop (but with continuous interruptions through suspension and resumption) in which all code is executed in callbacks, from one put/get to the next put/get. For instance, "unrolling" the code in Fig. 17 results in the code in Fig. 16.

Using promises and generators, we largely relieve developers from the burden of bookkeeping for continuations, with concise code as a result (e.g., Fig. 9).

Front-end. We hooked our Reo-to-JS compiler into PrDK [START_REF] Jongmans | Automata-Theoretic Protocol Programming[END_REF][START_REF] Jongmans | PrDK: Protocol Programming with Automata[END_REF]. PrDK consists of plugins for Eclipse, including a graphical editor for Reo circuits that allows developers to draw Reo diagrams as the ones in Figs. 10-13, using a dragand-drop interface. From this editor, the Reo-to-JS compiler can directly be run to generate and package all JavaScript code, for client-side execution in browsers or for server-side execution in Node.js (using the tiny-worker library [6]).

Hiding the Web Workers API behind Reo -In Practice

Examples 5-6 (Sect. 5) showed that, in theory, the limitations and issues of the Web Workers API (Sect. 3) are alleviated when a coordination language, such as Reo, is used. Our example programs were still abstract, though. In this section, complementary, we report on a concrete example program that we implemented using the tools presented in Sect. 6.

Example 8. To avoid bias, we took an existing program [START_REF]Javascript Web Workers Test[END_REF] (not ours) that uses the Web Workers API. This program performs a nontrivial numerical computation, where n background workers cooperatively compute a b mod c. This calculation is also performed, for instance, in RSA decryption, where a is the encrypted message, and where b and c constitute an agent's private key.

In the original program, first, the main worker sends a message (a, b i , c)-a "work package"-to every background worker 1 ≤ i ≤ n, such that b i = b. Subsequently, every background worker i computes a bi mod c and sends back the result. Finally, the main worker aggregates these results into the final outcome. Communication between the main worker and the background workers thus follows a typical master-slaves pattern.

Using our tools, we adapted the original program to use the Reo@JS API, effectively by replacing all postMessage calls with put and get calls on ports. We also relieved the main worker from its original tasks of dividing the work and aggregating the results, and placed these responsibilities with two new background workers. As a result, the background workers now exactly fit Alice, the Bobs, and Carol in Ex. 3: Alice divides the work, the Bobs perform the work and compute the results, and Carol aggregates the results. By instantiating Alice, the Bobs, and Carol in this way, Fig. 11 is directly applicable in this case study, including all its previously explained advantages (Exs. 5-6).

As a result of these changes, the coordination code that needed to be written manually was reduced from 145 lines to 46 lines (reduction of nearly 70%). Moreover, by implementing the coordination protocol in a separate module as a Reo circuit, it became amenable to reuse; essentially, the changes to the original program turned a specific implementation of master-slaves coordination into a reusable generic one. Thus, the effort of designing the circuit (less than an hour by a Reo expert) need not be remade in the future.

Example 9. Suppose that the original program "accidentally" (e.g., as the result of a programming mistake) lets the main worker send all work packages to the same background worker, so losing concurrency. As the implementation of the coordination protocol is not an explicit module in the original program, there is no obvious place to enforce that work packages should be evenly distributed among background workers.

In contrast, using Reo, we can encode such constraints in the circuit, and the compiler-generated code automatically enforces them. Figure 13 already showed such a circuit for two Bobs, which can be generalized to n. Using this circuit, if a faulty Bob performs multiple get operations, the circuit still ensures that the other Bobs receive a work package before the faulty Bob receives its second one, so preserving concurrency. Thus, new constraints (e.g., to improve robustness) can directly be added in our approach, due to improved changeability.

Example 10. As a first indication of performance, we conducted the following experiment. We took a synchronous variant of the circuit in Fig. 13 and a synchronous variant of the circuit between the two Bobs and Carol in Fig. 11, then we used the Reo-to-JS compiler to generate code, and finally we ran the resulting programs in Firefox on a machine with four hardware threads, processed by two physical cores. We experimented with synchronous circuits, because we wanted to test a worst-case scenario (asynchrony is cheaper than synchrony). The computation to be performed was always 2 1024•10 6 mod 97777. We repeated this for 1 ≤ n ≤ 10 Bobs, and we averaged our timing measurements over ten runs per n; we did the same for the original program to make a comparison.

Figure 19a shows the begin-to-end execution times (error bars indicate standard deviation). The figure shows that scalability is quite well, so long as there is hardware parallelism to harness (up to n = 4). Evaluating the effectiveness of the parallelization is actually not our main concern, though; we are primarily interested in the performance of the compiler-generated protocol implementation relative to the hand-written one in the original program. (measured by commenting out the computations of the workers). 6 This figure shows that the compiler-generated code is on average 20% slower. Given that we have not seriously optimized our compiler and runtime library yet, we consider this a promising result: it suggests that we can have the advantages in Sect. 5 without prohibitive performance costs.

The examples in Sect. 5 and in this section, combined with the tools in Sect. 6, provide first evidence that hiding the Web Workers API behind a coordination language, such as Reo, is advantageous in theory and feasible in practice. 6 Ideally, coordination overhead is completely independent of workload. In practice, however, this is not always so. The memory footprint of a workload can, for instance, affect the size of coordination overhead [START_REF] Jongmans | Automata-Theoretic Protocol Programming[END_REF]. Generally, the larger a workload, the smaller the ratio coordination computation , the less impact coordination overhead has on performance, and the less important minimizing such overhead becomes; at that point, other software qualities (changeability, reusability, etc.) may take precedence.

Related work. Beside the Web Workers API, other proposals to incorporate actor-based concurrency in JavaScript have been made. For instance, Stivan et al. [START_REF] Stivan | Akka. js: Towards a portable actor runtime environment[END_REF] ported the JVM-based implementation of the Akka framework to JavaScript, called Akka.js. One of the differences between the Web Workers API and Akka.js is that Akka.js allows actors on different JavaScript engines to communicate with each other. For Myter et al. [START_REF] Myter | Many Spiders Make a Better Web: A Unified Web-Based Actor Framework[END_REF], supporting both parallelism and distribution was a key design consideration in developing the Spiders.js framework. Spiders.js places particular emphasis on ease of programming, but not on coordination protocols. Welc et al. [START_REF] Welc | Generic Workers: Towards Unified Distributed and Parallel JavaScript Programming Model[END_REF] proposed generic workers to support both parallelism and distribution in terms of an API very similar to the Web Workers API. These approaches are complementary to ours: in this paper, we simplify implementing coordination protocols among background workers running on the same machine, but a generalization to distributed actors would be interesting.

There has also been work on incorporating data parallelism in JavaScript, including the River Trail framework by Herhut et al. [START_REF] Herhut | River Trail: A Path to Parallelism in JavaScript[END_REF] and the WebCL initiative [8], which constitutes a JavaScript binding to OpenCL. In an emperical study of twelve Web applications, Radoi et al. [START_REF] Radoi | Are web applications ready for parallelism?[END_REF] found "a surprisingly large quantity of compute-intensive loops of which many were latently parallel."

Outside academia, several libraries have been developed to simplify programming with the Web Workers API, including q-connection [5], parallel.js [4], Hamsters.js [2], and operative [3], but without emphasizing coordination protocols.

Technical differences aside, the main conceptual difference between all this related work and our proposed approach is that we emphasize the importance of coordination protocols as explicit programming artifacts, thereby enforcing syntactic separation of coordination and computation. Such a separation makes it easier to change and reuse coordination protocols. This work. We showed that implementing coordination protocols among background workers is difficult, because of limitations and issues with the low-level Web Workers API (Sects. 2-3). To make this simpler, we proposed to hide the Web Workers API behind a coordination language that provides higher-level constructs. Using Reo (Sect. 4), we demonstrated the advantages and feasibility of our approach by example (Sects. 5, 7), and we presented the necessary tool support in terms of a compiler, a runtime library and API, and a front-end (Sect. 6). As Web application developers have a tradition of separating concerns (HTML, CSS, JavaScript), Web applications may constitute a fertile new application domain for existing coordination languages.

Future work. We argued, by example, that use of a coordination language makes implementing coordination protocols among background workers simpler (i.e., it has particular advantages over directly using the Web Workers API). Complementary proof for this claim would consist of a set of successful real projects; we therefore aim to empirically evaluate the merits of our proposed approach, and improve our tools in the process. Optimizing the Reo-to-JS compiler and Reo@JS runtime library is also high on our list, including a study of impact on performance, which we barely touched upon in this paper.

An important aspect of the previously mentioned future work is studying the scalability of our proposed approach, both in terms of usability and performance. We expect modularity (separation of coordination and computation) to play an enabling role in dealing with complex systems, but it requires a new way of working from programmers; the consequences of this are unclear and should be better studied. Also, tools (notably, the compiler) need to ensure performance scalability as coordination protocols grow larger (i.e., involve more participants), which generally is a nontrivial technical challenge [START_REF] Jongmans | Can High Throughput Atone for High Latency in Compiler-Generated Protocol Code?[END_REF].

We chose to use Reo in this work, because it is strongly rooted in separation of computation and coordination. Reo, however, also has its limitations. For instance, run-time parametrization in the number of workers is not yet possible. It is therefore interesting to see if a JavaScript variant of, for instance, Pabble [START_REF] Ng | Pabble: parameterised Scribble[END_REF] (based on multiparty session types [START_REF] Honda | Multiparty Asynchronous Session Types[END_REF]) is more suitable.

A special case of a background worker is one that only calls an asynchronous API (e.g., the Geolocation API) and processes the result in a callback. In another experiment with our tools [START_REF] Krauweel | Concurrent and asynchronous JavaScript programming using Reo[END_REF] (omitted from this paper to save space), we encountered several such distinguished background workers and already added support for them in our tool (the tool automatically generates code to make asynchronous API calls from our framework; the programmer does not need to write such boilerplate code her/himself). Further research is necessary, however, to study to what extent coordination languages can also be used to orchestrate asynchronous API calls as a solution to "callback hells", and whether there are advantages compared to existing approaches; see Philips et al. [START_REF] Philips | Dependence-driven delimited CPS transformation for JavaScript[END_REF].

Fig. 1 : 5 6

 15 Fig. 1: main-pp.js

  bob1 = new new new Worker("bob.js"); var var var bob2 = new new new Worker("bob.js"); ... var var var pendingBobs = [bob1, bob2]; alice.onmessage = function function function(e) { if if if (pendingBobs.length > 0) { var var var bob = pendingBobs.shift(); bob.postMessage(e.data); } else else else { setTimeout(function function function(e) { alice.onmessage(e); }, 0);

17

 17

25 }

 25 Fig. 7: main-abbc.js

  Version of fifo1 with an n-capacity buffer fifo e1 e2 ∞ Version of fifo1 with an unbounded buffer

12 / 19 .Fig. 10 :

 121910 Fig. 9: workers-reo.js

Fig. 19 :

 19 Fig. 19: Experimental results

Table 1 :

 1 Common channelsEvery channel has two ends, each of which is either a source end or a sink end.

This is an inefficient implementation, but we aim for simplicity here.

This node is, in fact, syntactic sugar for a complexer circuit (i.e., it can be composed).

Compared to Figs.[START_REF] Herhut | River Trail: A Path to Parallelism in JavaScript[END_REF][START_REF] Honda | Multiparty Asynchronous Session Types[END_REF], the actual implementation also supports multiple ports per workers, and it is protected against workers that perform the next get (or put) before the previous one is completed. Details appear elsewhere[START_REF] Krauweel | Concurrent and asynchronous JavaScript programming using Reo[END_REF].

versions of the code for input ports; the code for output ports is similar. Fig. 14 shows class InputPort, instances of which are used by background workers. At the "background side", whenever get is called, sndRequest is subsequently called (through a promise; see below). sndRequest essentially relays the get call to the proxy of the main worker, by sending a null message. Then, at the "main side", this null message is processed by rcvRequest, which calls the real get that is monitored by the state machine. The resulting value is eventually sent back to the background worker, where it is processed by rcvResponse.

The nonblocking operations complication is trickier to solve, because it seems impossible to implement blocking operations in JavaScript without exposing the programmer to some of the required logic. The argument is as follows. JavaScript has no blocking constructs, so we need to implement them ourselves. One option is busy-waiting, where an event listener that needs to block repeatedly checks the value of a variable until it is changed by another event listener of the same worker (e.g., in response to a message receipt). But, as event listeners are never preempted, they are never interleaved. This entails a causal loop that causes a busy-waiting worker to busy-wait forever: the second event listener is not executed until the busy-waiting is over, which does not happen until the variable is updated, which is what the second event listener should do. The only viable alternative to implement blocking, then, seems suspending the worker in its event loop, by ending the current event listener. Importantly, just before suspending, bookkeeping is required to register a continuation; otherwise, the worker does not know how to proceed later on. It seems inevitable to place the burden of bookkeeping for continuations on the developer. The main challenge is to minimize this burden, encapsulating it in the Reo@JS runtime library wherever possible.

First, we use promises. A Promise object represents the eventual result of an asynchronous computation, which may not have finished yet when the Promise object is created. Upon calling the constructor of a Promise object, an executor (function) is passed that defines the asynchronous computation to be performed;


Paolo Baldan
email: baldan@math.unipd.it

Alessandro Beggiato
email: alessandro.beggiato@imtlucca.it

Alberto Lluch Lafuente

Many-to-Many Information Flow Policies

Keywords: Information Flow, Coordination, Concurrency, Declassification, Non-Interference, Causality, Event Structures

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

Introduction

As the number of interconnected devices increases, the focus on security-related aspects of coordinated computations gains more and more relevance and appeal. Techniques for controlling and enforcing the flow of information need to be applied, and possibly extended to deal with coordination aspects. Typically, the entities of a system are assigned a security level, and information flow policies prescribe which interactions are legal and which are forbidden. This is normally expressed via a relation that models the admitted flows between security levels.

Motivation and Problem Statement. The information flow relations used in the literature to model policies are almost invariably binary relations between individual security levels. This paper is motivated by the observation that some desired information flow properties naturally involve suitable coordinated sets of security levels rather than mere individual levels. For example, some secret information (say, owned by a government agency E, cf. Figure 1) could be safely disclosed to a set of confidential channels of incomparable security levels (say, corresponding to competing investors C and D) simultaneously, with individual leaks considered instead illegal or unfair. This is for instance, the spirit of U.S. security and exchange commission's regulation fair disclosure [START_REF]Selective disclosure and insider trading[END_REF]. Dually, a group of competing companies (say A and B in Figure 1) may agree to collectively disclose their secrets (say to the government agency E), with individual disclosures being undesired. This paper is motivated by such scenarios and, in general, by the following question: what is a natural notion of information flow policies that regulate flows among sets of security levels? Contributions. We address the question by proposing a simple policy specification language that extends the usual security diagrams by allowing relations between sets of security levels instead of just single levels. The clauses in our policies are of the form A 1 , . . . , A m B 1 , . . . , B n , intuitively meaning that the security levels A 1 , . . . , A m are allowed to coordinate in order to let information flow to security levels B 1 , . . . , B n .

In our approach the flow of information between entities is captured in terms of the existence of causal dependencies between events representing occurrences of actions of such entities. In particular, we use event structures [START_REF] Nielsen | Petri nets, event structures and domains[END_REF][START_REF] Winskel | Event structures[END_REF] as a reference semantic model. The idea is that causal dependencies between events represent the transfer of some information. Thus causal dependencies are required to obey to coordination patterns as prescribed by the information flow policy. For traditional intransitive binary policies any flow of information, i.e., any (direct) causality a < b between events a and b needs to be allowed by the policy, i.e., if the level of a is A and the level of b is B then the policy has to include a clause A B. We generalise this to many-to-many policies by requiring that any direct causality a < b is part of a possibly more complex interaction that conforms to a coordination pattern allowed by the policy, i.e., if A 1 and B 1 are the security levels of a and b, respectively, there must exist a clause A 1 , A 2 . . . A n B 1 , B 2 , . . . , B m in the policy and events a 1 , a 2 , . . . , a n , b 1 , b 2 , . . . , b m (with b equal to some b k ) such that each event a i has level A i , each event b j has level B j , and events a 1 , . . . a n are (suitably coordinated) causes of the events b 1 , . . . , b m .

As an example, consider the diagram of Figure 1, where arrows represent direct causalities between events and the security levels coincide with the principals. For events we use the notation name : level. The direct causality from event disclose : A to event collect : E is allowed by the policy A, B E since collect : E is also causally dependent on disclose : B, thus providing some guarantee of the fact that A and B disclose their secrets collectively. Analogously, the direct causality from disclose : E to collect : C is allowed by the policy E A, B since there is a causality relation from disclose : E to collect : D as well, yielding some sort of simultaneity in the disclosure of the secrets from E to C, D.

We study several properties of our policy language. In particular, we observe that checking whether a system satisfies a policy is decidable for a general class of event structures, the so-called regular trace event structures [START_REF] Thiagarajan | Regular event structures and finite Petri nets: A conjecture[END_REF]. As a matter of fact, policy satisfaction is expressible as a first-order property and the corresponding model checking problem is decidable [START_REF] Madhusudan | Model-checking trace event structures[END_REF]. We also discuss the relation with classical notions of information flow control, including non-interference and declassification, and suggest applications beyond secret exchange protocols, including program security and routing in security architectures.

Synopsis. Section 2 introduces several motivating examples, including a running example that is used throughout the paper. Section 3 provides some technical background on event structures. Section 4 presents the policy language, the notion of policy satisfaction and a decidability result. Section 5 compares with notions of information flow based on interleaving semantics, in particular with trace-and bisimulation-based non-interference. Section 6 discusses other related works. Section 7 concludes our paper and outlines future research.

Motivating Examples

We introduce here some examples that have motivated our work and that we envisage as application domains for many-to-many information flow analysis.

put secA @AB : A get ?sec @AB : B put secB @BA : B get ?sec @BA : A @ @ v v n n n n (a) Protocol P1 put secA @AE : A put secB @BE : B gather ?sec1,?sec21,?sec2 @AE,BE : E scatter sec2,sec1 @EA,EB : E get ?sec @EA : A get ?sec @EB : Simultaneous Secret Exchange. Consider first the problem of exchanging a secret between two parties, say Alice and Bob. We shall use this as a running example throughout the paper. A way to solve the problem would be to proceed according to the protocol in Figure 2a, where Alice starts sending her secret to Bob, which then replies with his own secret. The graphical representation (technically a security-labelled event structure) will be explained later. Here it suffices to understand that the figure represents the structure of the communication in an execution, where an event put m @C : P, represents party P sending m on channel C, and an event get t @C : P, represents party P receiving a message from channel C to be saved according to the pattern t (binding/formal fields being denoted with a leading question mark "?"). Arrows represent (direct) causal dependencies between events. The protocol has essentially the same structure of classical key exchange protocols [START_REF] Merkle | Secure communications over insecure channels[END_REF] and does not solve one of the main concerns of the so-called simultaneous secret exchange problem, which is to avoid or minimise competitive advantage among the parties exchanging the secrets (see e.g. [START_REF] Okamoto | How to simultaneously exchange secrets by general assumptions[END_REF]). If we assume to deal with information of two security levels (one for each party), a standard approach to information flow does not help much in this scenario, as we can just allow flows between Alice and Bob (and thus accept any protocol with no guarantee) or forbid them (and thus reject all protocols). One standard solution to the simultaneous secret exchange problem is to use an intermediary (say Eve). Many-to-many information flow policies can be used to specify some desired properties of intermediary-based protocols. For example, we may require that the intermediary forwards information to Alice and Bob simultaneously (denoted by an information flow policy Eve Alice, Bob), and that the intermediary accepts information from Alice and Bob only if collectively disclosed (denoted by an information flow policy by Alice, Bob Eve). A graphical representation for this security policy, that will be refined and explained in detail later, can be found in Figure 2c. The protocol sketched in Figure 2b, which uses multi-party interactions, satisfies the desired information flow properties. The protocol uses in particular an MPI-like gather operation to (point-wise) collect a list messages from different sources, and MPI-like scatter operation to piece-wise broadcast the list of secrets.

B 8 8 v v v v x x r r r r x x r r r r 8 8 v v v v (b) Protocol P2 A B E u u u s s s y y y y (c) Policy
put secA @AB : A put secB @BA : B get ?sec @BA : A get ?sec @AB : B B B t t j j j j j j j j j j j We shall see that the causality approach to information flow allows one to provide stronger guarantees on secret exchange protocols, by only admitting in-formation to flow collectively and simultaneously between Alice and Bob, namely, Alice, Bob Alice, Bob (see Figure 3b, for a graphical representation), even without intermediaries. This is realised by the protocol in Figure 3a, where vertical and cross dependencies are control and data dependencies, respectively.

Language-Based Security and Declassification. We use a classic problem of declassification in access control to illustrate how our approach can be used to check information flow properties in the traditional sense [START_REF] Sabelfeld | Language-based information-flow security[END_REF], and how our policies can be used to specify several useful forms of declassification [START_REF] Mantel | Controlled declassification based on intransitive noninterference[END_REF][START_REF] Sabelfeld | Declassification: Dimensions and principles[END_REF]. The access control program below, on the left, written in a simple imperative programming language in the style of [START_REF] Sabelfeld | Language-based information-flow security[END_REF], is checking a password and preparing a reply to the user in a variable display. A causal semantics to the program can be given based on the following idea: (i) events correspond to variable updates or initialisations, (ii) an update x := e causally depends on previous updates of all variables in e or their initialisation, (iii) if a control point is conditioned by y then all updates in all branches of the control causally depend on the latest update of y (or its initialisation), and (iv) conflict relations (represented as dotted lines) capture branching. For the program at hand, the resulting event structure can be found on the right.

if downgrade then if check(user,password) then display := "ok"; log := log , user,"ok" ; else display :="ko"; log :=log , user,"ko" ; downgrade := ... password := ... user := ... display := "ok" display := "ko" log := log , user,"ok" log := log , user,"ko" D D r r ee ee ee ee ee ee A A | | y y y y y y y y y y y y

4 4 i i i i i i i i i i i i u u l l l l l l l A A 3 3
} } u u l l l l l l l l l l l l l l l l l l Disregarding whether the password is correct or not, there is a flow of information concerning the password to the user, represented as a causality relation from the latest update of the password to the updates of variable display.

For simplicity assume that each variable has its own security level, coinciding with the variable name. A standard security type system would consider the program to be insecure and our approach would agree on that in absence of a policy password display allowing the leaks. Of course, such a policy is not desirable in general (e.g. the user may be malicious). However, the program provides some guarantees that make it acceptable from the security point of view. First, the reply is also influenced by a check on variable downgrade, which may be used to disable login (e.g. after several unsuccessful attempts). This provides a standard form of controlled declassification. Requiring that the declassification is controlled as desired can be done through a policy password, downgrade display. In addition, the program above is using a log to keep track of logging attempts. This provides the additional desirable property that password leaks are only possible when the information concerning the access attempt also flows to the log (denoted user, password display, log).

Security architectures. A third motivating case are systems where information of different security levels needs to traverse shared resources, like a routing network.

An archetypal example is the Multiple Independent Levels of Security (MILS)

architecture [START_REF] Rushby | Separation and integration in MILS (the MILS constitution)[END_REF]. The diagram on the left of the figure below depicts a simplified version of such an architecture, inspired by the case study of [START_REF] Li | Disjunctive information flow for communicating processes[END_REF]. Information from security level A (resp. B) should be allowed to flow into C (resp. D) only.

Messages are routed through a common network made of a multiplexer component (M) that accepts messages from both A and B and forwards it to a demultiplexer component (W), which dispatches the messages either to C or to D, according to routing information.

A B M W C D & & T T T Ô Ô ¨¨ Ô Ô ¨¨¨& & T T T A B M W C D & & T T T Ô Ô ¨¨ l l
The diagram on the left of the figure can be also seen as an information flow policy (isomorphic to the architecture) aiming at enforcing the desired flows. The problem of this naive policy is that it allows also for undesired flows, e.g., from A to D and from B to C, indirectly through the network: a protocol wrongly routing the information would be admitted by the policy. Consider instead a policy where individual flows from W to C and D are not allowed, and instead, they need to be collectively produced with A and B, respectively (denoted A, W C and B, W D). The new policy (sketched on the right of the figure) would reject protocols wrongly routing the messages.

Event Structures

We model the causal behaviour of a system with prime event structures [START_REF] Nielsen | Petri nets, event structures and domains[END_REF][START_REF] Winskel | Event structures[END_REF], a well-studied semantic model of concurrency where causality is a primitive notion. The way in which an event structure is associated to a specific formalism will depend on the system features one intends to capture (data/control flow, etc.).

Definition 1 (event structure

). An event structure E = E, ≤, # consists of a set E of events, a partial order relation ≤ ⊆ E × E called causality, and an irreflexive symmetric relation # ⊆ E × E called conflict such that: For e, e ∈ E we write e < e (e is a proper cause of e ) if e ≤ e and e = e . We say that e is a direct cause of e (denoted e e ) if e < e and for all e ∈ E if e ≤ e ≤ e either e = e or e = e . The causes of a set of events X ⊆ E are defined as [X] = e∈X [e]. We lift causality to sets of events, with a universal interpretation, i.e., for X, Y ⊆ E, we write X < Y (resp. X Y ) if for all e ∈ X and e ∈ Y we have e < e (resp. e e ). For e ∈ E we define the set of its proper causes as [e) = [e] \ {e}. We say that e, e ∈ E are in direct conflict, written e# µ e , when e#e and for all e ∈ [e) it holds ¬(e #e ) and for all e ∈ [e ) it holds ¬(e#e ), i.e., the conflict is not inherited. ∅ {put secA @AB : A} {put secB @BA : B} {put secA @AB : A, put secB @BA : B} {put secA @AB : A, put secB @BA : B, get ?sec @BA : A} {put secA @AB : A, put secB @AB : B, get ?sec @AB : B} {put secA @AB : A, put secB @BA : B, get ?sec @BA : A, get ?sec @AB : 4. Configurations of the event structure in Figure 3a.

B} u u l l l l l l l l A A A A u u l l l l l s s h h h h h h h C C s s h h h h h h h C C Fig.
Figures 2a-3a show three event structures corresponding to different protocols in our running example. The set of events correspond to communication operations, and are annotated with the initials of the principal executing the action (which is actually the security level assigned to the event, as we shall explain later). Causality is represented graphically by directed arrows, while conflict (to be seen in subsequent examples) is represented by dotted undirected lines. For the sake of a lighter notation, we follow the tradition of depicting direct causalities and conflicts only.

Event structures describe the possible events in computations and their mutual relations. When e < e then e must necessarily occur before e , while if e#e then the occurrence of e excludes e (and vice versa). Computations are characterised as conflict-free sets of events, containing the causes of all events. Definition 2 (configuration). Let E = E, ≤, # be an event structure. A configuration of E is a subset C ⊆ E such that ¬(e#e ) for all e, e ∈ C and

[C] = C. The set of configurations of E is denoted C(E).
For any event e, the causes [e] and the proper causes [e) are configurations.

Figure 4 depicts all the configurations of the event structure of Figure 3a. They are related by arrows that represent transitions, i.e., how a configuration can be extended to another configuration by adding an event.

Definition 3 (extension)

. Let E = E, ≤, # be an event structure, and let C ∈ C(E). We say that an event e extends C when e ∈ C and C ∪ {e} ∈ C(E). In this situation we write C ⊕ e for C ∪ {e}. The set of possible extensions of a configuration

C is PE(C) = {e ∈ E | C ⊕ e ∈ C(E)}.
The transition system semantics of an event structure is obtained considering configurations as states and extensions as transitions.

Definition 4 (transition system). The transition system of an event structure

E = E, ≤, # is the tuple TS (E) = C(E), {C → C ⊕e | C ∈ C(E)∧e ∈ E} .
The diagram of Figure 4 represents the transition system of the event structure in Figure 3a. When events carry a label, the above definition yields labelled transition systems with transitions C a → C ⊕ e, where a is the label of e.

Many-to-Many Information Flow Policies

We introduce here our notion of many-to-many information flow policies, which describe the legal interactions among sets of security levels. Section 4.1 presents the policy language, Section 4.2 defines the semantics, Section 4.3 studies some of its properties, and Section 4.4 provides a decidability result.

A Policy Language for Many-to-Many Information Flows

We start by introducing the syntax of many-to-many information flow policies.

Definition 5 (many-to-many information flow policy). Let L be a finite set of security levels and C = {d, f } be a set of coordination constraints. A many-to-many multi-level information flow policy is a pair Π = L , where ⊆ 2 L × 2 C × 2 L and (A, ∅, A) ∈ for all A ∈ L . We denote by P the set of all policies.

We will write A σ B for (A, σ, B) ∈ , often dropping brackets from σ, A and B. Security levels in L are ranged over by A, B, . . . and sets of security levels are ranged over by A, B, . . .. The requirement that A A for all A ∈ L is natural in information flow: information is always allowed to flow within the same level of security. Finiteness of the set of security levels L is a natural assumption. It could be meaningful to allow L to be infinite only when security levels can be generated dynamically. The theory in the paper could be adapted trivially apart from the decidability result in Section 4.4, that relies on regularity of the model which in turn implies the finiteness of L .

Note that an information flow policy can be seen as a directed hyper-graph whose hyper-arcs are labelled by (possibly empty) subsets of the alphabet of coordination constraints C (to be explained later). This analogy is exploited in the visual representation of security policies.

Informally, a clause A σ B specifies that a group of entities whose set of security levels is A is allowed to influence a group of entities whose set of security levels is B, subject to the coordination constraints in σ. E.g., a policy

Alice, Bob

Eve

allows Alice and Bob to influence Eve, while the policy Eve Alice, Bob

allows Eve to influence Alice and Bob. We will see that the above two policies can be combined to allow Alice and Bob to exchange their secrets using Eve as an intermediary, and providing some fairness guarantees. A different policy that would allow a similar flow of information is Alice,Bob,Eve Alice,Bob Alice Eve Bob Eve

(3)

A B d E m m m E d,f A B x x q q 8 8 w w A B d E d,f m m m y y y y A B E f q q q q w w w w G G o o y y y y A B d,f
q q q w w w y y y y

Π1 Π2 Π1 ∪ Π2 Π3 Π4
Fig. 5. Security policies, graphically.

that allows Alice, Bob and Eve to influence Alice and Bob, Alice to influence Eve, and Bob to influence Eve. Intuitively, this can be used to specify that both Alice and Bob can talk individually to the intermediary Eve, which in turn can talk to Alice and Bob in coordination with them. For a clause in A σ B the superscript σ ⊆ C allows one to specify some additional coordination constraints on the interaction pattern among the levels in A and B. The superscript d requires all entities in A to influence all the entities in B directly. For instance, for the policy (1) we might want Alice and Bob to influence Eve directly, with no delegation among them or to another intermediary. This leads to the policy Π 1 Alice, Bob d Eve depicted in Figure 5.

In general the flow of information to all of the entities in B is just potential, i.e., the information is made available to entities in B simultaneously, but it could happen that after one entity in B acquired the information (some of) the others get disabled. The superscript f , that stands for "fair" disclosure, prevents the above to happen: whenever information flows to one of the entities in B, then it must eventually flow to all other entities in B.

It is worth to remark that the information flowing to the entities in B need not be the same since causality in our approach represents in general the transfer of some information. Ensuring that the same information is being transferred depends on the actual causal semantics under consideration.

In our previous examples, for policies (2) and (3) it is natural to require fairness to forbid competition among Alice and Bob. This leads to the policies Π 2 and Π 3 in Figure 5. Observe that fairness constraints are superfluous when there is only one security level in the target, like Eve in Π 1 . Notice that in policy Π 3 , the absence of the "direct" constraint allows Eve to act as an intermediary. A variant of Π 3 without intermediary is Π 4

Alice, Bob d,f Alice, Bob, which specifies a direct exchange of information between Alice and Bob.

Semantics of Many-to-Many Policies

In our setting, a security model is an event structure used to capture the structure of computations and flows. Events correspond to actions of some security level.

Definition 6 (causal security model). Let L be a set of security levels. A (causal) security model in L is a pair E, λ where E = E, ≤, # is an event structure and λ : E → L is a security assignment.

The security assignment λ maps each event to a security level and can be lifted to sets of events: given X ⊆ E we let λX = {A ∈ L | ∃e ∈ X . λ(e) = A}. For X ⊆ E and A ⊆ L we write X : A if |X| = |A| and λX = A. We write e : A instead of {e} : {A}. The event structures of Figures 1-3a are security models, where the security assignment corresponds to the principal annotations.

We next formalise in which sense a clause A σ B justifies a situation in which we have sets of events X and Y such that X : A, Y : B and the events in X cause the events in Y . We do this by introducing a semantic counterpart of the relation σ over sets of events. We first define some properties of sets of events that are related to the coordination constraints. We say that a set of events X ⊆ E is flat if [X) is a configuration and for every e, e ∈ X it holds e < e . Notice that when X is flat, all events in X are are enabled at [X). The events in a flat set X may disable each other or there can be future events that disable some of them but not the others. We say that X is fair if for all events e, e ∈ X and event e ∈ E, we have e#e iff e #e . Note that in this case, since the events in X have the same conflicts and conflict is irreflexive, either all or none of them is executable.

Definition 7 (relation σ )

. Let E = E, ≤, # be an event structure and let X, Y ⊆ E. We write

(i) X Y if X < Y , and Y is flat; (ii) X d Y if X Y and X Y ; (iii) X f Y if X Y and Y is fair; (iv) X d,f Y if X d Y and X f Y .
In words, we write X Y whenever each event in X is a cause for each event in Y , and the set Y is flat, ensuring that [Y ) is a configuration enabling all events in Y .

We write X d Y when additionally X Y , i.e., causality is direct, meaning that delegation is not permitted.

Notice that when X Y events in Y are all enabled at configuration [Y ), so that the possibility of getting information from X is granted to all elements of Y , but once an event in Y is executed other events in Y could get disabled: it may be the case that the events in Y disable each other or, more generally, they could be in conflict with different events. The constraint X f Y , asking that Y is fair, guarantees, instead, that if the information reaches one of the events in Y it will eventually reach all of them, or, more formally, that any configuration intersecting Y extends to a configuration including Y . Note that, in absence of conflicts, the fairness constraint becomes inessential since it is always trivially satisfied.

We can now define what it means for a security model to satisfy a policy.

Π1 ∪ Π2 Π3 Π4 P1 P3 P2 P4 P5 P6
Table 1. Models versus policies.

Definition 8 (security). Let Π = L , be an information flow policy, E = E, ≤, # be an event structure, let E, λ be a security model in L . Given X, Y ⊆ E and σ ⊆ C , we say that the clause

A σ B ∈ Π allows X σ Y , written A σ B |= X σ Y if X : A, Y : B.
We say that E, λ satisfies Π or that E, λ is Π-secure, denoted E, λ |= Π, if for all e, e ∈ E such that e e there exist X, Y ⊆ E with e ∈ Y such that

X σ Y and A σ B |= X σ Y for some A σ B ∈ Π such that λ(e) ∈ A. When λ is clear from the context we sometimes write E |= Π.
Intuitively, a security model satisfies a policy if any direct causality e e is part of a (possibly larger) interaction X σ Y justified by some clause A σ B of the policy. We require e ∈ Y in order to ensure that the flow to e is influenced by X : A (recall that X < Y ) and thus by all levels in A. On the other hand, event e is not necessarily in X since the information of level λ(e) that is required to flow to all levels in B might have been provided by another cause of e . Still, since e is a cause of e , it will be part of any computation involving e , hence it will coordinate with the events in X to enable e . This is fundamental, e.g., to implement a simultaneous disclosure asynchronously as we shall explain later.

Table 1 summarizes the satisfaction of policies by the protocols of our running example. The double horizontal lines separate protocols without intermediaries (P 1 ,P 3 ) from those with intermediaries (P 2 ,P 4 ,P 5 ,P 6 ), and the vertical double lines separates policies with intermediaries (Π 1 ∪ Π 2 and Π 3 ) from policies without intermediaries (Π 4 ). We start discussing the scenarios with intermediaries.

The security model of Figure 2b (Protocol P 2 ) satisfies the policies Π 1 ∪ Π 2 and Π 3 of Figure 5. For example, the direct causality put secA @AE : A gather ?sec1, ?sec2 @AE, BE : E is justified by clause Alice, Bob d Eve of policy Π 1 , by choosing X = {put secA @AE : A, put secB @BE : B} and Y = {gather ?sec1, ?sec2 @AE, BE : E}. In words, the disclosure to Eve is allowed since it is collectively made by Alice and Bob. The direct causalities between the multicast of Eve and the receptions by Alice and Bob are justified by the clauses in policies Π 2 or Π 3 . In order to see this for the only clause of Π 2 , observe that we can choose X = {scatter sec2, sec1 @EA, EB : E} and Y = {get ?sec @EA : A, get ?sec @EB : B}. In words, both message receptions of Alice and Bob depend on Eve sending the secrets, and they cannot be disabled, put secA @AE : A put secB @BE : B gather ?sec1,?sec2 @AE,BE : E put (sec1,sec2) @C : E get ?sec @C : A get ?sec @C :

B 6 6 s s s z z u u u Ò Ò ¦ ¦ ¦ ¦ ¦ ¦ ¦ ¦ ( ( V V V V V V V V
put secA @AE : A put secB @BE : B gather ?sec1,?sec2 @AE,BE : E put sec2 @EA : E put sec1 @EB : E get ?sec @EA : A get ?sec @EB :

B 6 6 s s s z z u u u 3 3 g g g Ô Ô ¨¨¨¨¨¨¨ @ @
put secA @AE : A put secB @BE : B get ?sec1 @AE : E get ?sec2 @BE : E scatter sec2,sec1 @EA,EB : E get ? @EA : A get ?sec @EB : hence they have the same (i.e., no) conflicts. For the only clause of Π 3 the situation is a bit more involved: the idea is to select Y as before and X to be the rest of the events. Intuitively, Eve acts as a delegated intermediary: the submission of the secrets by Alice and Bob influence their final receptions, indirectly through the events of Eve.

B Ô Ô ¨¨¨¨¨¨6 6 s s s z z u u u 6
Consider now the event structures in Figure 6, which represent variants of the protocols of our running example where Eve is used as an intermediary. They can be seen as alternatives to the protocol P 2 in Figure 2b. Protocol P 4 is like P 2 but the intermediary does not scatter the secrets; these are instead combined in a composite message and sent to a channel C thus creating a conflict between Alice and Bob since both expect to extract the (combined) secrets from C. In protocol P 5 , Eve sends the messages asynchronously with point-to-point operations, first to Alice and then to Bob. Finally, in P 6 , the reception of the secrets is asynchronous, with point-to-point operations.

None of these variants satisfies policy Π 1 ∪ Π 2 . For instance, no clause in Π 1 ∪ Π 2 justifies the direct causality put (sec1, sec2) @C : E get ?sec @C : A in P 4 due to the conflict between get ?sec @C : A and get ?sec @C : B. In P 5 the direct causalities from Eve's put events to the get events of Alice and Bob cannot be justified since there is no Eve-labelled event that is a direct cause for both get events. Notice that such causalities could be justified if we drop the directness constraints from the clauses since the reception of the messages by Bob and Alice are causally dependent by the first put of Eve. Similarly, the direct causalities from Alice and Bob's put events to Eve's get events in P 6 cannot be justified.

The situation is different for Π 3 . Indeed, both P 5 and P 6 satisfy the policy. Intuitively, the asynchronous collection of the secrets in P 6 that could not be justified in Π 2 can now be justified since Alice and Bob are allowed to talk to Eve independently. On the other hand, the asynchronous disclosure by Eve in P 5 is justified since it also depends on both Alice and Bob without directness constraint.

Similarly, it can be seen that among the protocols not using intermediaries, namely P 1 (Figure 2a) and P 3 (Figure 3a), only P 3 satisfies the policy Π 4 . Protocol P 3 is indeed the only one that guarantees that Alice and Bob collectively make their secrets available to Alice and Bob simultaneously. Indeed, protocol P 3 has a unique advantage over P 1 : when Alice (resp. Bob) gets the secrets, (s)he is not ensured to be in competitive advantage. Clearly, protocol P 1 does not have this property. Therefore, P 3 offers a solution to the simultaneous secret exchange problem with guarantees based on causality rather than on bounds on the amount of different information obtained by the parties (as e.g. in [START_REF] Fujisaki | How to enhance the security of public-key encryption at minimum cost[END_REF]).

Semantic properties

We next present some properties of security policies. We first observe that aggregating security levels preserves the satisfaction of policies.

Proposition 1 (soundness of level aggregation). Let E, λ be a security model in L and ρ : L → L , a total mapping between security levels (possibly merging some of them

). If E, λ |= Π then E, ρ • λ |= ρ(Π).
In the above definition ρ(Π) is the homomorphic lifting of ρ to policies, i.e.,

ρ(Π ∪ Π ) = ρ(Π) ∪ ρ(Π ), ρ(A σ B) = ρ(A) σ ρ(B) and ρ(∅) = ∅.
Secondly, we discuss how policies can be related according to their strictness.

Definition 9 (strictness relation). The strictness relation ⊆ P × P is defined as the least transitive and reflexive relation among policies closed under

Π Π Π 1 ⊆ Π 1 Π ∪ Π 1 Π ∪ Π 1 (Ctx) σ ⊆ σ A σ B A σ B (Constr) A = A ∪ A {A σ B, A σ B} A σ B (SplitL) |B| = 1 A σ∪{f } B A σ B (ConstrF) B = B ∪ B {A σ B , A σ B } A σ B (SplitR) |A| = |B| = 1 A σ∪{d} B A σ B (ConstrD)
The intuition is the following. Rule Ctx says that the strictness relation is preserved under context closure (i.e., if Π Π then Π ∪ Π Π ∪ Π ). In addition, the relation is preserved even if the weaker policy Π is embedded in a larger context since the addition of clauses to a policy makes it more permissive. By rule SplitL if the source A of a clause is split as A ∪ A then the clause can be relaxed by replacing it with two clauses having the same coordination constraints, the same targets and A and A , respectively, as sources. This weakens the policy since any direct causality from an event of level A ∈ A to an event of level B ∈ B that is justified by A σ B can be justified by A σ B or by

A σ B.
Rule SplitR is analogous, but with the split performed on the target. Rule Constr says that a clause can be relaxed by removing coordination constraints in σ. The last two rules ConstrF and ConstrD capture the fact that some constraints are trivially satisfied when clauses have a special shape. More precisely, given a clause A σ B with |B| = 1 the fairness constraint is vacuously satisfied and this motivates rule ConstrF. If, additionally, |A| = 1 the same applies to the directness constraint and this leads to rule ConstrD.

When Π Π we say that Π is less restrictive than Π . For instance, the policies Π 1 and Π 2 of our example are less restrictive than Π 1 ∪ Π 2 , and Π 1 ∪ Π 2 and Π 3 are incomparable.

An interesting result is that the strictness relation is sound and complete with respect to policy satisfaction. Proposition 2 ( is sound and complete). Let Π = L , , Π = L , be two policies. The following holds

(i) if Π Π then, for all models E, λ in L , E, λ |= Π implies E, λ |= Π ; (ii) if for all models E, λ in L , E, λ |= Π implies E, λ |= Π , then Π Π.
By soundness, whenever Π Π Π, the policies Π and Π are equivalent, i.e., they are satisfied by exactly the same models. Syntactically different policies can be equivalent because they have clauses that differ for constraints which are vacuosly satisfied (see rules ConstrF and ConstrD). Moreover, equivalent policies can differ for the presence of clauses which are useless because they are subsumed by others (e.g., if a policy includes the clauses A σ B, and A σ B, the addition of a clause A ∪ A σ B produces an equivalent policy). It can be proved that the partial order induced by the preorder (P, ) is a complete lattice. The (equivalence class of the) policy {(A, C , A) | A ∈ L } is the top element (the most restrictive policy, which admits flows within individual security levels only), and (the equivalence class of) L × ∅ × L is the bottom element (the most permissive policy, which accepts all flows).

It is interesting to observe that the most restrictive policy satisfied by a security model does not exist in general. In fact, in order to determine such policy the idea could be to start with the most permissive policy, allowing for all binary flows, and keep using the rules (by joining or removing clauses, or adding coordination constraints) in order to restrict it until no more rules can be applied. This works, but the policy obtained is not uniquely determined, not even up to equivalence. For example, consider the security model M on the left of the figure below. Clearly, M satisfies both Π 1 and Π 2 . Such policies are incomparable with respect to (none of them can be obtained from the other by removing or joining classes, and indeed event structures can be found that satisfy one of them but not the other like those at the middle and the right of the figure above). Hence Π 1 and Π 2 are distinct minimal policies satisfied by model M: the most restrictive policy satisfied by M does not exist.

Decidability on Regular Trace Event Structures

The event structure associated with a system exhibiting a cyclic behaviour is infinite, since events represent "occurrences" of computational steps. Nevertheless, we can show that policy satisfaction is decidable once we focus on regular trace event structures [START_REF] Thiagarajan | Regular event structures and finite Petri nets: A conjecture[END_REF], a class of "effectively represented" event structures enjoying suitable regularity properties. This result relies on the observation that policy satisfaction can be expressed as a first order property and first order logic (FOL) is known to be decidable on regular trace event structures [START_REF] Madhusudan | Model-checking trace event structures[END_REF].

Roughly speaking, for regular trace event structures dependencies are required to be induced by a finite labelling, endowed with an independence relation. More precisely, recall that a trace alphabet consists of a pair M = Σ, I where Σ is a finite label alphabet and I ⊆ Σ × Σ is an irreflexive relation called the independence relation. An M -labelled event structure is an event structure E, with a labelling function ξ : E → Σ satisfying (1) if e# µ e then ξ(e) = ξ(e );

(2) if e e or e# µ e then (ξ(e), ξ(e )) ∈ I; and (3) if (ξ(e), ξ(e )) ∈ I then e ≤ e or e#e. Conditions ( 2) and (3) ensure that the concurrency relation of the event structure (unordered events that are not in conflict) conforms to the independence relation of M . Condition (1) asks that the Σ-labelled transition system associated with E is deterministic. In addition, as in [START_REF] Madhusudan | Model-checking trace event structures[END_REF], we require the regularity of the set of (labelled) sequences of execution from the empty configuration in the event structure, i.e., of the set seq

(E) = {σ ∈ Σ * | ∅ σ -→ * C in TS (E)}.
Definition 10 (regular trace event structure). An event structure E is regular trace if it is M -labelled for some trace alphabet M = Σ, I and seq(E) ⊆ Σ * is a regular language.

When we need to make the trace alphabet explicit, we say that the event structure E is M -regular trace. The class of regular trace event structures is quite general. In [START_REF] Thiagarajan | Regular trace event structures[END_REF] it has been shown to coincide with the class of event structures associated with finite safe Petri nets by the unfolding construction [START_REF] Nielsen | Petri nets, event structures and domains[END_REF].

We first instantiate the notion of regularity in the setting of security models.

Definition 11 (regular trace model). A security model E, λ in L is regular trace if there exists a trace alphabet M = Σ, I such that E is M -regular trace via the labelling ξ : E → Σ and λ = λ • ξ for some λ : Σ → L.

The encoding of policy satisfaction as a FOL sentence crucially relies on the fact that, in order to check whether a causal dependency a b is justified by some clause A σ B, we need to find sets of events X : A, Y : B with bounded cardinality |X| = |A| and |Y | = |B|. Then decidability follows from [START_REF] Madhusudan | Model-checking trace event structures[END_REF].

Proposition 3 (decidability on regular trace security models). Let Π = L , be an information flow policy and let E, λ be a regular trace security model in L . The decision problem E, λ |= Π is decidable.

Non-Interference

We discuss in this section how our causality-based notion of information flow compares with notions of information flow based on non-interference for concurrent systems. The key differentiating factor resides in the semantic model: causal semantics are normally finer than interleaving semantics. The paradigmatic example is given by processes a | b and a.b + b.a which are equated in an interleaving world but are different from a causal point of view. Hence we would expect our notion of security, when confined to binary policies, to be more restrictive than those based on interleaving semantics. However, this is not always the case mainly because observational non-interference approaches capture flows of information due to conflicts (i.e., branching), which are instead not considered in our notion of security. We will also briefly discuss how our approach could be amended to consider conflict-related flows.

Consider, for example Strong Non-deterministic Non-Interference (SNNI) [START_REF] Focardi | A taxonomy of security properties for process algebras[END_REF][START_REF] Focardi | Classification of security properties (part I: information flow)[END_REF][START_REF] Busi | Structural non-interference in elementary and trace nets[END_REF]. Informally, a system S is SNNI whenever S \ H (i.e., the low level system in isolation) and S/H (i.e., the entire system where high H actions are unobservable) are weak trace equivalent. Let us say that an event structure E is SNNI whenever its transition system TS (E) is SNNI. Then it is easy to see that {L H}-security is strictly finer than SNNI. The easiest case is to show that SNNI does not imply {L H}-security. The counterexample is the event structure E 0 below: Clearly E 0 is SNNI since the set of traces of both E 0 \ H and E 0 /H is { , l}, but E 0 is not {L H}-secure since the direct causality h l cannot be justified. On the other hand, {L H}-security implies SNNI: if E 0 is {L H}-secure then it contains no direct causality e e with e : L and e : H, and hence all traces are such that high transitions are never necessarily followed by low transitions. Hence, the traces of E 0 \ H and the traces of E 0 /H coincide.

Observational non-interference properties are expressive enough to capture information leakages arising from deadlocks and divergence. Particularly popular in this tradition are notions based on weak bisimulation, like the Bisimulationbased SNNI (BSNNI) and the finer Bisimulation-based Non-Deducibility on Compositions (BNDC) [START_REF] Focardi | A taxonomy of security properties for process algebras[END_REF][START_REF] Focardi | Classification of security properties (part I: information flow)[END_REF]. BSNNI is like SNNI but with weak bisimulation equivalence instead of trace equivalence. Note that BSNNI and {L H}-security are incomparable. First, it is easily seen that {L H}-security does not imply BSNNI. The event structure E 1 above is {L H}-secure (since there is no direct causality between l and h) but is not BSNNI, since TS (E 1 )\H and TS (E 1 )/H are not weak bisimilar. Informally, the low part of the system can deduce that h occurred by observing that l is not executable. Vice versa, one can show that BSNNI does not imply {L H}-security. Consider the event structure E 2 below. Clearly, E 2 is not {L H}-secure since the direct causality h l is not allowed. On the other hand, E 2 is BNNI since TS (E 2 )\H and TS (E 2 )/H are weak bisimilar.

For similar reasons, our notion of security is also incomparable to other observational notions of non-interference based on transition systems such as BNDC and those that extend [START_REF] Rushby | Noninterference, transitivity, and channel-control security policies[END_REF] by requiring the source and the target states of every high transition to be (low) trace equivalent [START_REF] Bossi | Modelling downgrading in information flow security[END_REF][START_REF] Focardi | Classification of security properties (part I: information flow)[END_REF][START_REF] Gorrieri | On intransitive non-interference in some models of concurrency[END_REF].

Related Work

Logic-based languages have been investigated as flexible formalisms to express security properties. We mention, e.g., hyperproperties [START_REF] Clarkson | Hyperproperties[END_REF] and their logics (e.g. [START_REF] Clarkson | Temporal logics for hyperproperties[END_REF][START_REF] Milushev | Towards incrementalization of holistic hyperproperties[END_REF]). Our policies can be easily integrated in logic-based languages to obtain a richer policy language. For instance, the simplest solution is to combine our policies by using standard propositional operators.

Another example is Paralocks [START_REF] Broberg | Paralocks: role-based information flow control and beyond[END_REF], a language for specifying role-based information flow policies. In Paralocks a data item x can be annotated with clauses of the form Σ → a, specifying the conditions Σ under which x can flow into actor a. Such policies can be related to many-to-one policies in our approach, i.e., of the form A 1 . . . A m B 1 . It less clear how many-to-many policies, i.e., policies stating that data can flow to an agent a if it also flows to an agent b, could be expressed in Paralocks.

In addition to FOL and MSO for event structures [START_REF] Madhusudan | Model-checking trace event structures[END_REF], our work can be related to other logics motivated by causality. An example is Event Order Logic (EOL) of [START_REF] Leitner-Fischer | Probabilistic fault tree synthesis using causality computation[END_REF], a logic based language used to specify boolean conditions on the occurrence of events, with applications to safety analysis. EOL is inspired by Linear-time Temporal Logic (LTL) and introduces ad-hoc operators to specify the order of events. The more relevant operator is ψ 1 ∧ . ψ 2 which allows one to express that the events described by ψ 1 occur before those described by ψ 2 . Hence, a policy A 1 . . . A m B 1 . . . B n can be related to an EOL formula A 1 ∨ . . . ∨ A m ∧ . B 1 ∨ . . . ∨ B n . However, EOL does not feature operators to express some of our coordination constraints.

Conclusion

We have presented a novel approach to many-to-many information flow policies that allows one to specify patterns of coordination among several security levels. In particular, each clause in a policy can specify that a certain set of levels is allowed to cooperate to provide the flow collectively, and possibly simultaneously to another set of security levels. We believe that the approach can turn useful in several scenarios including secret exchange protocols, security architectures and systems with controlled forms of declassification. We have provided decidability results and discussed the relation to some traditional notions of security, including observational non-interference and language-based security. We are currently investigating the development of verification and enforcement mechanisms for concrete specification languages, like programming languages and Petri nets. We are also investigating extensions of our work in several directions, including how to suitably deal with indirect flows of information due to conflicts, and how to deal with the transfer of specific values.

Fig. 1 .

 1 Fig. 1. Information flow example.

Fig. 2 .

 2 Fig. 2. Two secret exchange protocols and a security policy.

Fig. 3 .

 3 Fig. 3. A secret exchange protocol satisfying a policy without intermediary.

  (i) for all e ∈ E the set of causes [e] = {e ∈ E | e ≤ e} is finite (finitariness); (ii) for all e, e , e ∈ E, if e#e and e ≤ e then e#e (conflict inheritance).

Fig. 6 .

 6 Fig. 6. Secret exchange protocols P4 (left), P5 (center) and P6 (right).

|

  | y y y y and the policies Π 1 = (A, B C), (A B) and Π 2 = (A B), (B C).

  TS (E0) \ H TS (E0)/H

l

  : L h : H h : H l : L TS (E2) \ H TS (E2)/H