Tony Bourdier
email: tony.bourdier@loria.fr

Horatiu Cirstea
email: horatiu.cirstea@loria.fr

Symbolic analysis of network security policies using rewrite systems

Keywords: D.4.6 [Operating systems]: Security and Protection, F.1.1 [Computation by abstract devices]: Models of Computation, F.4.2 [Mathematical logic and formal languages]: Grammars and Other Rewriting Systems Security, Theory, Verification Security policies, firewalls, rewrite systems, tree automata

First designed to enable private networks to be opened up to the outside world in a secure way, the growing complexity of organizations make firewalls indispensable to control information flow within a company. The central role they hold in the security of the organization information make their management a critical task and that is why for years many works have focused on checking and analysing firewalls. The composition of firewalls, taking into account routing rules, has nevertheless often been neglected. In this paper, we propose to specify all components of a firewall, i.e. filtering and translation rules, as a rewrite system. We show that such specifications allow us to handle usual problems such as comparison, structural analysis and query analysis. We also propose a formal way to describe the composition of firewalls (including routing) in order to build a whole network security policy. The properties of the obtained rewrite system are strongly related to the properties of the specified networks and thus, classical theoretical and practical tools can be used to obtain relevant security properties of the security policies.

INTRODUCTION

Security constitutes a crucial concern in modern information systems. Several aspects are involved, such as user authentication (establishing and verifying users' identity), cryptology (changing secrets into unintelligible messages and back to the original secrets after transmission) and security policies (preventing illicit or forbidden accesses from users to information).

Due to the increasing complexity of organizations, network security policies are rarely defined as a single firewall. Most of the time, they are made up of numerous firewalls whose composition depends on the network topology and on the routing rules. That is why it is often difficult to ensure that the composition of different local security policies (i.e. firewalls) expresses the intended security policy. Their formal specification is thus crucial and for several years now the importance of using formal methods to specify security policies has been generally accepted. For example, to achieve high levels of certification (EAL 1 5, 6, 7), it is necessary to provide a formal specification enabling to obtain mechanized formal proofs, to carry out techniques for test generation, or to perform static analyses ensuring required properties.

Many methods and tools have been developed for analysing and testing firewall policies. These methods are broken down into two different categories: the active methods and the passive methods. The former consist in sending packets to the network and to make a diagnosis according to the received packets. The main advantage of these methods is that they require no abstract representation of firewalls and thus no error can be introduced between the specification and the implementation. However, such methods have the major drawback of consuming bandwidth, interfering with the traffic and being non exhaustive. That is why we focused on passive methods, that is methods which send no packet and make an offline analysis. Two main categories of passive analysis are investigated in the literature: structural analysis and query analysis. Structural analysis examines the relationships that rules have with other rules within a firewall configuration or across multiple firewalls. A misconfiguration (or conflict) occurs when several rules match the same packet or when a rule can be removed without changing the behavior of the firewall. Query analysis provides a way to ask questions of the form "Which computers in the private network can receive packets from 212.12.30.25 ?". It then consists in defining a language to describe a firewall query and a way to compute its solutions. Some works [START_REF] Cuppens | Detection of network security component misconfiguration by rewriting and correlation[END_REF][START_REF] Abbes | An inference system for detecting firewall filtering rules anomalies[END_REF][START_REF] Benelbahri | Tuple based approach for anomalies detection within firewall filtering rules[END_REF][START_REF] Gouda | Firewall design: Consistency, completeness, and compactness[END_REF][START_REF] Cuppens | Detection and removal of firewall misconfiguration[END_REF][START_REF] Liu | Formal verification of firewall policies[END_REF][START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF] deal with structural analysis and focus on defining, detecting and discussing misconfigurations while others [START_REF] Hazelhurst | Algorithms for analysing firewall and router access lists[END_REF][START_REF] Eronen | An expert system for analyzing firewall rules[END_REF][START_REF] Liu | Firewall policy queries[END_REF] concentrate on query analysis. Some of these works abstract firewall filtering rules as one or two-dimensional ranges of IP, which does not allow to take completely advantage of the obtained results. Others assume that packets are not modified during their network traversal and then do not support network translation address capabilities. Moreover, they often focus on policies based on a single firewall or do not take into account the network topology. Some of the approaches can handle these various aspects (a detailed comparison between the different techniques could be found in [START_REF] Nelson | The margrave tool for firewall analysis[END_REF]) but the routing aspects and especially the issues related to their combination with firewall policies are not deeply investigated. More generally, several rewrite based frameworks have already been proposed for specifying and analysing security policies. In particular, [START_REF] Kirchner | Analysis of rewrite-based access control policies[END_REF] introduces a narrowing based method for querying rule based policies and illustrates the proposed technique by the analysis of a standalone firewall policy. This approach can be seen as a first step toward a dedicated and more complete method for rewrite based analysis of firewall security policies.

In this paper, we introduce a new framework, based on rewrite systems and automata, for specifying and analysing firewall security policies. First, we show that this approach is particularly well adapted for the efficient verification of standalone firewall rules. The particular specification we propose here is not only natural since quite close to real world firewall rules but allows also an efficient implementation. We briefly explain how this approach can be used to perform the various types of analyses described in the literature. Second, we extend this approach to take into account the network topology of the network secured by firewall security policies. We show that there is a strong relationship between relevant properties of the secured network and the properties of the rewrite systems used to specify them. We focus here on completeness, i.e. the ability to take a decision for any (routed) packet, and consistency, i.e. the coherence of the final decisions independently of the routing protocol. We consider this approach particularly interesting since the correspondence with the properties of the rewrite systems used for the specifications allowed us to use theoretical and automatic tools to perform these analyses.

The paper is structured as follows. In Section 2 we present notions and notations we use throughout this paper. Section 3 is devoted to the presentation of the rewrite-based framework for specifying and analysing (standalone) firewalls. In Section 4 we address the composition of firewalls with respect to topologies and routing rules. Finally, the last section concludes with some perspectives for further work.

TECHNICAL PRELIMINARIES

We suppose the reader is familiar with notions related to term algebra (terms, substitutions, positions, . . . ), rewriting systems (reduction relation, confluence, termination,. . . ) [START_REF] Baader | Term rewriting and all that[END_REF] and tree automata [START_REF] Comon | Tree automata techniques and applications[END_REF]. In this section we recall some basic notions, present the notations we use throughout this paper and introduce the notion of constrained rewrite systems.

Term algebra. We consider in this paper many-sorted sig-natures of the form (F, S) consisting of a set of sorts S and a set of function symbols F. Symbols of F are denoted by bold characters f , g, . . . and their profiles are denoted as follows f : s1 × . . . × sn s where s1, . . . , s are sorts of S and n is the arity of f . The set of terms of sort s built out of symbols from F and of sorted variables from a set X is denoted by T s X and the set of ground terms of sort s is denoted by T s . For any t ∈ T X = ∪s∈S T s X , Var(t) denotes the variables occurring in t. If any variable of t occurs only once in t, then t is said linear. A position within t is a sequence ω of integers describing the path from the root of t (seen as a finite labeled tree) to the root of the subterm at that position, denoted by t |ω . We use ε for the empty sequence. | ω | is the length of the position. Pos(t) denotes the set of positions of t. t(ω) is the symbol of t at position ω and t [s] ω the term t with the subterm at position ω replaced by s. A substitution σ is a mapping from X to T X which is the identity except over a finite set of variables (its domain) and which is extended to an endomorphism of T X . A substitution is said ground if all the variables of its domain are mapped to ground terms. A term t matches a term t ′ iff σ(t ′ ) = t for some substitution σ. Two terms t and t ′ are unifiable iff σ(t ′ ) = σ(t) from some substitution σ.

Tree automata. A tree automaton is a triple A = (Q, QF , ∆) where Q is a finite set of symbols called states disjoint from F, QF ⊆ Q is the set of final states and ∆ is a finite set of transitions of the form f (q1, . . . , qn) →∆ q where q1, . . . , qn, q ∈ Q and n is the arity of f . →∆ is extended to → * ∆ as follows: if ∀i, ti → * ∆ qi and f (q1, . . . , qn) →∆ q, then f (t1, . . . , tn) → * ∆ q. The language recognized by A

= (Q, QF , ∆) is L(A) = {t ∈ T | ∃q ∈ QF , t → * ∆ q}.
A set (or a language) of terms recognized by a tree automaton is said regular. A relation R is regular if there exists an automaton recognizing { t | t ∈ R} where for any t = (t1, . . . , tn) and ω ∈ ∪iPos(ti), t(ω) = (t1[ω), . . . , tn[ω)) with ti[ω) = ti(ω) if ω ∈ Pos(ti) and the special symbol Λ otherwise. Boolean operations, Cartesian product, projection and cylindrification preserve regularity. We say that a set or a relation is effectively regular iff it is regular and we can compute an automaton which recognizes it.

Rewrite systems. A rewrite rule is a pair of terms l → r. The terms l and r are respectively called the left-hand side and right-hand side of the rule. A rewrite system R is a finite set of rewrite rules. Any rewrite system R induces a binary relation over terms denoted by →R as follows: for any terms t, t ′ , t →R t ′ if there exist a rule l → r of R, ω ∈ Pos(t) and a substitution σ such that t |ω = σ(l) and t ′ = t [σ(r)] ω . A rewrite rule is linear iff its left-hand side and right-hand side are linear. A rewrite system is linear if all its rules are linear. A growing rewrite system (GRS) [START_REF] Jacquemard | Decidable approximations of term rewriting systems[END_REF] is a linear rewrite system such that for every rule l → r, if

l(ω) = r(ω ′ ) ∈ X for some positions ω, ω ′ , then | ω | ≤ 1.
An ordered rewrite system is a rewrite system in which rules are ordered. For an ordered rewrite system R, →R is defined as follows: for any terms t, t ′ , t →R t ′ if there exists a rule l → r of R, ω ∈ Pos(t) and a substitution σ such that t |ω = σ(l) and t ′ = t [σ(r)] ω and such that there is no prior rule l ′ → r ′ such that t |ω ′ = σ ′ (l ′ ) for some ω ′ and σ ′ . A constrained rewrite system (CRS) is a rewrite system such For any linear (constrained or not) rewrite system R and rule r of R, we denote by rec(r) the regular set of ground terms that are reducible by r. If R is an ordered rewrite systems, we denote by rec(r/R) the set of terms that are reducible by r and by no rule prior to r in R.

STANDALONE FIREWALL SPECIFICA-TION AND ANALYSIS 3.1 Short introduction to firewalls

In a network, when a host wants to transmit a message to another host, the data are encapsulated in a packet. Such a packet consists of the data that should be transmitted as well as of some additional information used to route it to the appropriate destination. The additional information, or header, mainly contains the packet's source and destination IP address, its protocol and the source and destination port. To control packet transmission between different subnetworks, it is common to deploy a network security policy based on a combination of firewalls. A firewall is an application that controls the forwarding of packets which cross it by using a combination of:

• packet filtering, which consists in inspecting each packet and either allowing it to continue its traversal or dropping it and • network address translation, which consists in modifying network address information in packet headers.

Firewalls inspect incoming packets and accept or deny to forward them based on a list of decision rules which map the description of a set of packets to a decision. The most common criteria [START_REF] Conoboy | Ip filter based firewalls howto[END_REF][START_REF] Russell | Linux 2.4 packet filtering howto[END_REF] that firewalls use are the packet's source and destination address, its protocol, and, for TCP and UDP traffic, the port number. Moreover, firewalls often offer network address translation (NAT) functionality, which consists in rewriting the source (SNAT) or destination address (DNAT) into another address. The diagram in Figure 1 sums up the behavior of a firewall. At each step (1, 2 and 3), the packet is compared against a list of rules and the action (translation of destination address, drop or forward and translation of source address) corresponding to the first matched rule is performed.

Example 1. We give in Figure 2 a simple example of a firewall consisting of three rules: a filtering rule, a DNAT rule and an SNAT rule. We use the CIDR notation [START_REF] Fuller | Classless Inter-Domain Routing (CIDR): The Internet Address Assignment and Aggregation Plan[END_REF] to denote subnetworks

Rewrite-based specification of firewalls

In this section, we present a formalization of firewalls based on rewrite systems. The ports and IP addresses are specified as terms and the firewall rules are specified as rewrite rules. Such specifications can be easily and automatically obtained from firewall configurations defined using classical firewall configuration languages such as netfilter [START_REF] Russell | Linux 2.4 packet filtering howto[END_REF].

Packets and subnetworks

In our approach, packets are represented as algebraic terms.

For readability reasons, we consider that firewalls inspect only addresses and ports. Other information, such as protocols, TCP flags, states, could be considered without difficulty. The selected symbolic representation of packets is based on the following signature:

0, 1 : Binary Binary # : Binary from : Binary × Binary SrcAddr dest : Binary × Binary DstAddress packet : SrcAddr × DstAddress Packet
We briefly describe in this section the meaning of the above symbols and defer until Section 3.3 the discussion about the consequences of our choices.

IPv4 as well as IPv6 addresses can be equivalently seen as sequences of bits, tuples of hexadecimal numbers or inte-<

: gers. We have thus numerous possibilities to describe addresses as terms. However, we must keep in mind that the packet inspection performed by firewalls strongly relies on checking whether an address belongs to some given address ranges which generally correspond to subnetwork3 domains.

IP
A special feature of subnetwork domains is that all hosts it contains are addressed with a common, identical prefix in their IP address when this address is written as a bit vector.

It is thus natural to specify subnetworks as bit sequences of variable length and to use pattern matching for testing if an address belongs to a subnetwork domain.

By representing addresses as words over {0, 1}, or equivalently as terms built from monadic symbols 0 and 1 and a constant #, we obtain a representation of subnetworks by linear terms built from 0 and 1. For example, the term t = 11000000 10101000 00010100(x ) (we omit parentheses to keep readability) denotes the subnetwork 192.168.20.1/24 whereas 11000000 10101000 00010100 00000001(#) denotes the IP address 192.168.20.1. For convenience, we will use in this paper the dot-decimal notation for addresses, the decimal notation for ports and the CIDR notation for subnetworks. When a variable occurs in the corresponding term, it will be indicated in brackets. For example t will be denoted by 192.168. As showed in Section 3.3, explicitly identifying the source and destination addresses (using the symbols from and dest) allows us to encode the firewall rules by appropriate tree automata that can be effectively used for firewall analysis.

Firewall rules.

To represent firewall rules, we add to the signature the following symbols:

accept, drop : Decision

From a rewriting point of view, a filtering rule rewrites a packet into accept or drop whereas a NAT rule rewrites the source or destination address of a packet.

Definition 1 (Firewall).

A firewall f is composed of three ordered rewrite systems Pre f , Filter f and Post f such that: Definition 2 (Semantics). For any firewall f, its semantics is denoted by f and defined as follows:

f = f accept ∪ f drop with 4 f accept = {(t, u) ∈ T Packet × T Packet | ∃v ∈ T Packet , t → Pre f ;{x→x} v → Filter f accept ∧ v → Post f ;{x→x} u} f drop = {(t, drop) ∈ T Packet × T Decision | ∃v ∈ T Packet , t → Pre f ;{x→x} u → Filter f drop}
From an abstract point of view, a firewall can be seen as a partial or total function which takes as input a packet and returns either another packet (possibly the same) or drop.

Analysis of firewalls

In this section, we show that this rewrite based specification allows one not only to automatically check properties concerning the semantics of a firewall but also to perform structural and query analysis over firewalls.

Firewall semantics analysis

A firewall can be seen as a decision process which associates to an incoming packet a decision which could be either drop or another packet, and thus the following properties should be verified: consistency, which indicates that at most one decision is taken for a given incoming packet, termination, which ensures that a firewall computes a decision in a finite time and completeness, which means that for any incoming packet, the firewall returns a decision.

As we have already said, by construction, any firewall denotes a terminating and consistent decision process and thus a function. The completeness can be thus defined as follows:

Definition 3 (Completeness). We say that a firewall f is complete iff f is a total function.

The particular shape of the rules defining a firewall allows us to represent the semantics of a firewall as a regular relation and consequently to verify its completeness:

Proposition 1. Completeness is decidable.

Proof. The proof relies on the regularity of the relations involved in the definition of the semantics of a firewall. Indeed, since the left-hand sides of all the rewrite rules composing a firewall are linear and share no variable with their corresponding right-hand sides, we can easily show that →Pre f and →Post f are regular tree relations (some technical manipulations are needed to take into account the order). Since the identity is a regular relation, it follows that → Pre f ;{x→x} and → Post f ;{x→x} are also regular. By composition and restriction, we obtain that f accept and f drop are regular tree (functional) relations. Consequently, f is a regular tree (functional) relation. The completeness can be tested by checking that the first projection of f covers the (regular) set of all possible incoming packets.

In the case of complete firewalls, it can be important to determine if a firewall is less or more permissive than another one. A more permissive firewall allows at least the same traffic as a less permissive one. Such an order is obviously not total. Definition 4 (Order). We define a partial order over complete firewalls as follows: for any f and f

′ , f f ′ (f ′ is more permissive than f) iff f accept ⊆ f ′ accept . We write f ≈ f ′ iff f f ′ and f ′ f.
A firewall f ′ is thus more permissive than a firewall f if it accepts all the packets f accepts and if it the result of the address translation is the same for these packets. Note that

f ≈ f ′ iff f = f ′ .
For the same reasons as before, we can decide whether a firewall is more or less permissive than another one: Proposition 2. The order relation is decidable.

Proof. As we have already shown, for any firewall f , f accept and f drop and f are regular relation. Consequently, the inclusion f accept ⊆ f ′ accept is decidable.

Note that two firewalls may have the same semantics even if their rules are different. This is particularly interesting since it allows to simplify or optimize the rules of a firewall and check if the resulted firewall has the same semantics as before.

Structural analysis.

Structural analysis refers to the detection of so-called misconfigurations (or anomalies) in (the rules of) a firewall. More precisely, such misconfigurations are properties expressed as relationships between the rules of a firewall. A complete survey of misconfigurations can be found in [START_REF] Cuppens | Detection of network security component misconfiguration by rewriting and correlation[END_REF][START_REF] Hamed | Taxonomy of conflicts in network security policies[END_REF]. Examples of anomalies are shadowing (a rule leads to decisions contradictory to decisions of prior rules), redundancy (a rule can be removed without changing the filtering result), generalization (a rule matches a superset of the set of packets matched by a prior rule with a different decision),. . . . We should mention that although several approaches have been developed for the detection of the above misconfigurations, this kind of anomalies are often intentionally introduced by firewall administrators in order to obtain more compact or more efficient rule sets. Detecting them is still interesting since it can outline some potential problems.

We only discuss here our approach for detecting shadowing; the other anomalies can be treated in a similar way. Let us first recall the definition of the shadowing anomaly: we say that a firewall has shadowing iff it contains at least one filtering rule such that all packets it accepts (resp. drops) are dropped (resp. accepted) by a prior rule. In such a case, the concerned rule is said to be shadowed.

The detection of the shadowed rules, as well as of the other misconfigurations, is based on the regularity of the sets of terms associated to a given rule. More precisely, each rule r is associated to several sets: rec(r), denoting the set of packets matching r; rec(r/Filter f ), denoting the set of packets matching r that match no prior rule of Filter f (i.e. rec(r) \ S r ′ <r rec(r ′ )) and rec(r/Filter f [d]) denoting the set of packets matching r that match no other rule of Filter f associated to the decision d. Since the left-hand sides of the filtering rules are linear terms, all the sets rec(r) are regular; the other sets are also regular since they can be built starting from rec(r) and using operations which preserve regularity. Misconfigurations can then be detected using inclusion or emptiness tests. For example, to detect if a rule r is shadowed, it suffices to check the emptiness of rec(r/Filter f [accept]) if the right-hand side of r is drop and the emptiness of rec(r/Filter f [drop]) otherwise.

It is well-known that the complexity of the operations over tree automata is quite high in general. In our case, the complexity of the needed operations strongly depends on the representation of packets and in particular on the representation of addresses. The choice of describing addresses as words over {0, 1} (or equivalently as terms built from the monadic symbols 0 and 1 and the constant #) was indeed made in order to obtain efficient implementations of the corresponding automata operations.

To simplify explanations, let us consider word automata; the correspondence with tree automata is straightforward. Due to the representation of address ranges, we are confronted with n-prefix (or simply prefix) languages, i.e. regular languages of the form α1.{0, 1} * ∪ . . . ∪ αn.{0, 1} * . A good property of the manipulated address ranges is that corresponding minimal and deterministic automata have no loop except at their unique final state which loops over itself for any word. The main advantages of n-prefix languages are the following:

• boolean operations preserve the prefix property,

• boolean operations can be performed in O(n) (where n is the number of states of the biggest operand) over the minimal deterministic automata and • the corresponding algorithms directly produce deterministic and minimal automata (and thus there is no need to perform any determinization).

As said before, the sets of addresses of a given subnetwork are 1-prefix. It follows that rec(r), rec(r/Filter f ), . . . , are prefix languages. Consequently, misconfigurations can be efficiently detected using our approach.

Query analysis

Another kind of analysis proposed by some of the firewall verification approaches [START_REF] Liu | Firewall queries. Principles of Distributed Systems[END_REF][START_REF] Liu | Firewall policy queries[END_REF] is query analysis. This kind of analysis provides a way to assist firewall administrators in understanding the behavior of a firewall by computing the result of user-defined queries such as "Which hosts in the subnetwork 192.168.1.1/22 can receive packets from a host in the subnetwork 172.20.1.1/24 ?". We have previously shown that the semantics of a firewall is a regular relation. Thus, any query expressed as a first order formula built from:

• variables, ground terms or terms whose head is the symbol packet and whose subterms are variables or ground terms; • membership constraints w.r.t. to one of the relations defined in Definition 2 and • membership constraints w.r.t. to a linear term (which means being a ground instance of) can be rewritten into a tree automaton recognizing the set of solutions of the query, that is values of free variables making the formula true.

NETWORK SECURITY POLICIES

A network security policy is generally deployed by using several firewalls. If each of the firewalls present in the network has the expected properties checked, for example, by performing the analyses presented in Section 3.3, this is not necessarily the case for their composition. Indeed, firewall composition introduces a new security element which could disturb the behavior of standalone firewalls after connecting them together: routing. Although routing rules can generate major security faults, these rules are often neglected in network security policy analyses. For example, they can lead to loops in the paths followed by packets and consequently to congestions and even to service denial. Moreover, the combination between the routing and the firewall rules can lead to packets handled differently depending on the route they follow and thus, to ambiguous network security policies.

Indeed, the effects induced by the interaction between the routers and the firewalls make the semantics of the global network security policy hard to understand, particularly in large networks with a complex topology. We propose in this section to go a step further in network security policies analysis and extend the approach proposed in the previous section to take into account the network topology and the routing rules.

Policy specifications

In order to analyse a network security policy, one should first specify the network topology. More precisely, one must specify the subnetworks, the location of the security hosts (i.e. the nodes in which firewalls, as logical entities, are deployed) and the connectivity between the subnetworks and the security hosts. A subnetwork can be seen as a logical unit consisting of a set of network hosts which can mutually communicate without going through a security host. It often corresponds to a particular section of an organization and it is usually represented by a symbolic name and by an IP address range (called domain). Security hosts are interconnection nodes in the network which can be connected to subnetworks (a security host connected to a subnetwork is its gateway5 ) and to other security hosts. The picture in Figure 3 gives an example of a topology. For readability reasons, we consider in this figure and in the subsequent related examples that IP addresses are built from only one octet (that is 8 bits) and that the domain of Internet is 129/2.

In order to formally specify such a topology we add to the signature given in Section 3.2 a sort Net representing subnetwork names and a sort SH representing security hosts names.

Definition 5 (Network Topology).

A network topology τ is given by:

• a finite set net1, . . . , netn : Net of subnetwork names;

• a finite set s1, . . . , sm :

SH of security host names; together with

• a total map ∆ : T Net T Binary X which associates any subnetwork name net i with a linear term of T Binary X called its domain;

• a total map GW : T Net T SH which associates any subnetwork name net i with a security host called its gateway such that for any security host s and any distinct subnetwork names net1, net2 ∈ GW -1 (s), the terms ∆(net1) and ∆(net2) are not unifiable (that is to say, address ranges of subnetworks connected to the same security host must be disjoint); • a relation CON over T SH × T SH describing the connection between the security hosts.

Example 3. The topology depicted in Figure 3 is formally defined by: ;

• GW = 8 > > < > > : printers → sh3 servers → sh3 secretariat → sh2 dpt info → sh1 9 > > = > > ;
;

• CON = {(sh1, sh2), (sh2, sh1), (sh2, sh3), (sh3, sh2)}.

Given a network topology, defining a network security policy consists in defining for each security host a set of NAT and filtering rules (a firewall). The firewalls associated with the security hosts describe a set of "local" policies which are combined by the topology.

Definition 6 (Network security policy).

A network security policy ℘ over a network topology τ is a total mapping which associates any security host sh of τ with a firewall ℘(sh).

Example 4. Let τ be the topology defined in Example 3. We define a network security policy ℘ over τ as follows:

• the aim of the security host sh1 is to hide the private IP address space of the subnetwork dpt info and its machines except for the printer 2 and the server 1 which serves as a proxy for other machines of dpt info.

(i) packet " from(193 /3 [x ], x ′ ) dest(129 /2 [y], y ′ ) « → drop (ii) packet(from(129 /2 [x ], x ′ ), y) → drop (iii)
packet(x , y) → accept meaning that: (i) the hosts in the secretariat cannot initiate an Internet communication; (ii) no communication can be initiated by a host outside the organization (i.e. from Internet); (iii) all the other packets are transmitted by the security host (as they are).

• The third security host sh3 focuses on traffic sent from or received by the subnetworks printers and servers.

It is associated to a firewall f3 = ℘(sh3) containing the following filtering rules:

8 > > > < > > > : (iv) packet " from(193 /3 [x ], x ′ ) dest(57 /4 [x ], x ′ ) « → accept (v) packet(from(97 /3 [x ], x ′ ), y ′ ) → accept (vi) packet(from(17 /4 [x ], x ′ ), y ′ ) → accept (vii)
packet(x , y) → drop meaning that (iv) hosts from secretariat can reach the printers but not the servers; (v) the security host does not block traffic sent from 97/3 = 57/4 ∪ 49/4 (that is from subnetworks printers and servers); (vi) packets from dpt info (seen by sh3 as a subnetwork whose domain is 17/4) are allowed and (vii) any other traffic is forbidden.

To entirely characterize the network traffic under a given security policy, one must define a routing strategy to determine the paths that packets must follow to reach their destinations.

Definition 7 (Routing strategy).

Given a network topology τ , a routing strategy is a map ζ : T SH T Binary

X

T SH such that:

(i) for any (sh, t1, sh ′ 1 ) and (sh, t2, sh ′ 2 ) ∈ ζ, there is no σ such that σ(t1) = σ(t2) and (ii) for any (sh, t, sh ′ ) ∈ ζ, there are no net ∈ GW -1 (sh)

and substitution σ such that σ(∆(net)) = σ(t).

A routing strategy ζ associates to any security host a routing map which indicates the next security host to which a given packet must be forwarded depending on its destination. We impose (i) a deterministic routing, i.e. all security hosts route any incoming packet to at most another one security host and (ii) that packets whose destination is a directly reachable subnetwork must be delivered (and then must not be routed to another security host). Moreover, the aim of a routing strategy is to transmit any packet from (security) host to (security) host until it reaches one which is able to take a definitive decision (i.e. deliver the message to its final destination or drop it). According to this point of view, a routing strategy must satisfy certain conditions. First, it must create no loop when it transmits a request (packet). Second, it must eventually transmit any packet to a (security) host which is able to take a decision if one can be taken (if no security host can take a decision, the packet is lost or, in a network jargon, the packet is non-routable). Thus, we say that a routing strategy ζ is sound w.r.t. a topology τ if it satisfies the conditions mentioned above. More formally, ζ is sound w.r.t. τ = (Net, SH, ∆, GW, CON ) iff for any t ∈ S net∈T Net rec(∆(net)) and sh ∈ T SH :

• there exist a finite sequence (sh i , ti, sh i+1 )i=1...n of tuples from ζ and a sequence of substitutions (σi)i=1...n+1 such that sh1 = sh and for all 1 ≤ i ≤ n: (sh i , sh i+1 ) ∈ CON , t = σi(ti) and t = σn+1(∆(net)) for some net such that GW(net) = shn+1 and • there exist no sequence (sh i , ti, sh i+1 )i=1...n and no (σi)i=1...n such that sh1 = shn+1 = sh and for all 1 ≤ i ≤ n: (sh i , sh i+1 ) ∈ CON and t = σi(ti).

In what follows all routing strategies are considered to be sound w.r.t. the topology for which they are designed.

Example 5. Following the previous example, we define the routing strategy below:

• ζ(sh1) =  125/1[x] → sh2 ; 64/2[x] → sh2 32/3[x] → sh2 ; 1/4[x] → sh2 ζ(sh3) =  128/1[x] → sh2 ; 1/2[x] → sh2 64/3[x]
→ sh2 specifying that any packet sent to an address which is not directly reachable from sh1 (resp. sh3) is routed to sh2 and

• ζ(sh2) = ˘97/3[x] → sh3 ; 17/4[x] → sh1
The questions we are interested in are the same as for single firewalls. Which packets reach their final destination? Which ones are dropped? However, the analysis becomes more complicated in this case. Indeed, comparing to the case of a single firewall where the decision of accepting or dropping a packet is taken locally, in the case of a network topology, there is potentially an important number of intermediate steps between the moment a packet is sent and the moment it is received at its final destination (or dropped).

In other terms, a packet can be in different states: sent, received, about to be filtered by a given security host, . . . The following figure represents an example of successive states in which a packet p can be: To analyse the traffic under a network security policy, our approach consists in labeling packets to indicate their current state and describing their state evolution as a rewriting process. To represent states, we introduce the following symbols: To conform with the classical idea that a security policy evaluates access requests to decisions, we use, for any network topology, the following vocabulary:

p sent from dpt info
sent : Net × SrcAddr ×
• network access requests refer to ground terms of the form sent(net, from(t1 , t2 ), dest(t3 , t4 )) for some net ∈ T Net and ground terms t1 , t2 , t3 and t4 such that t1 = σ(t) for t = ∆(net) and some ground substitution σ and • decisions refer to either drop or ground terms of head received.

We denote by Request the set of network access requests and by Decision the set of decisions.

As for single firewalls, any network security policy ℘ is associated to a function which takes as input a packet together with the subnetwork it is sent from and returns drop (if the packet is dropped during its transmission) or the corresponding delivered packet together with the recipient subnetwork. 4.

The rewrite system Flow ℘,ζ can be built for any network security policy ℘ and routing strategy ζ and computes the successive states of a given packet during its traversal of the network. Note that, by construction and due to the conditions imposed on ζ, Flow ℘,ζ is deterministic in the sense that for any ground term t, there exists at most one t ′ such that t → Flow ℘,ζ t ′ .

To make clear the role of each rule scheme, the figure is divided into five categories corresponding to the functionality the corresponding rules specify. The rule scheme (B) expresses that two hosts from the same subnetwork can communicate without going through a security host. (R1) expresses that a packet which is sent from a given subnetwork net toward another subnetwork must pass through the gateway of net. (R2) describes the packet forwarding from a security host to the one selected by the routing rules. (R3) indicates that if no routing rule applies and if the packet destination belongs to a subnetwork connected to the current security host, then the packet must be delivered to its recipient. (DN AT1) and (SN AT1) describe the address translation process when the packet matches a NAT rule whereas (DN AT2) and (SN AT2) express that a packet that does not match any NAT rule should only change its state. Finally, (F drop ) (resp. (Faccept)) specifies that a packet is dropped or forwarded according to the filtering rules of the current security host.

Policy properties

In this section, we discuss some crucial policy properties and see how the rewrite-based encoding we proposed allows us to reason about these properties.

As mentioned previously, completeness is the ability to take a decision for every network access request. In the case of a single firewall, for verifying this property it is sufficient to check that the set of filtering rules covers all possible packets. However, the case of a network security policy is more complicated. Indeed, incompleteness is obtained due an incomplete firewall or due to the fact that a packet is never neither dropped nor delivered to its final destination (in the latter case, we say that the packet is lost). Notice that a network security policy can be complete even if the firewalls it is made of are not complete and conversely, it can be incomplete even if all the firewalls it contains are complete.

Proposition 3. For any network security policy ℘ and routing strategy ζ, the ζ-completeness of ℘ is decidable.

More precisely, we have the following property: Proposition 4. Given a network security policy ℘ over a network topology τ and a routing strategy ζ, the sets:

(i) (→ * Flow ℘,ζ ) -1 (drop) and (ii) (→ * Flow ℘,ζ ) -1 (Decision \ drop)
are effectively regular.

Proof. The proofs of Propositions 3 and 4 are based on the fact that Flow ℘,ζ is a constrained growing rewrite system. The method [START_REF] Jacquemard | Decidable approximations of term rewriting systems[END_REF] used for computing a tree automaton which recognizes the set (→ * R ) -1 (L) for any regular tree language L and growing rewrite system R can be extended to constrained growing rewrite systems (the proof is given in Appendix A). Since {drop} and Decision \ {drop} are regular sets, we can build the tree automata which recognize (→ * Flow ℘,ζ ) -1 (drop) and (→ * Flow ℘,ζ ) -1 (Decision\drop). The completeness of a security policy can be verified by checking that the union of these two automata covers Request.

Even if a routing strategy is sound, the presence of address translation rules may cause routing loops. Indeed, some packets can be caught into a loop involving two or more NAT steps which are contradictory. For example, a security host s may translate a packet p into p ′ and route it to s ′ which may translate p ′ into p before routing it to s. Routing loops may significantly impact the quality of traffic and may even create a denial of service. We say that a routing strategy is safe under a security policy if the policy creates no routing loop. It is easy to see that the size of rewritten terms is not increased during the rewriting process by Flow ℘,ζ and thus only loops can lead to the non-termination of the rewrite system. Consequently, we obtain: Proposition 5 (Safe routing). Given a security policy ℘ over a topology τ together with a routing strategy ζ, ζ is safe under ℘ iff Flow ℘,ζ is terminating.

We have considered so far only security policies w.r. Source NAT

(SN AT1) post(s, x, y) → route(s, r, y) x ∈ rec(l → r/Post f ) for any s ∈ SH, f = ℘(s), l → r ∈ Post f (SN AT2) post(s, x, y) → route(s, x, y) x ∈ S r∈Post f rec(r)
for any s ∈ SH, f = ℘(s) Moreover, with the growing complexity of networks, the notions of performance and efficiency of the routing process appear and thus, the routes should be continuously calculated to take into account the situation of the traffic and to find the best paths, that is the shortest, the most reliable or those balancing best the network load. That is why adaptive routing, or dynamic routing, is widely used.

In this context, it is crucial that any packet has the same sort independently of the selected routing path it follows; it should be either delivered to the same recipient or dropped in all the cases. In other terms, routing should be a strategy for achieving a goal and should not alter the goal. We call consistency the property ensuring that the semantics of a security policy is the same for any (sound) routing strategy. To ensure the termination of the exploration precess, packets are labeled with the set of branches they have already explored. Thus, we obtain a rewrite systems which rewrites any request into all the possible decisions according to any sound routing strategies. More precisely, we obtain a system verifying the following proposition.

Proposition 6. Let ℘ be a network security policy over a network topology τ . Flow℘ is terminating iff any sound routing strategy is safe under ℘. In a such case, ℘ is consistent iff Flow℘ is ground confluent.

Proof. One can easily show that r * -→ Flow℘ d ∈ Decision iff there is a strategy ζ such that ℘ ζ (r) = d. Starting from that, the equivalence between the consistency of ℘ and the ground confluence of Flow℘ stands iff for any routing strategies ζ and ζ ′ , D( ℘ ζ ) = D( ℘ ζ ′ ). Since we consider only sound strategies, when a request cannot be solved, only two cases can occur: either the request involves a non-routable address or the strategy is not safe. In the former case, the request cannot be solved for any sound strategy. Thus, if all strategies are safe, they have all the same domain.

Example 6. Let us consider the policy described in Example 4. We have automatically prove (using A3PAT (CiME) [START_REF] Contejean | A3PAT, an approach for certified automated termination proofs[END_REF] and AProVE [START_REF] Giesl | AProVE 1.2: Automatic termination proofs in the dependency pair framework[END_REF]) that Flow℘ is terminating and thus that any sound routing strategy is safe under ℘. We also attempted a paper proof for the consistency of ℘ but the property is not verified in this case. The following rewriting derivations prove that ℘ is not consistent. It shows that, under some specific routing strategy, hosts from the secretariat can exploit the server 1 to attack the subnetwork servers.

We should mention that the specification of the network traffic as a rewrite system offers us two other possibilities non detailed in this paper. Indeed, semantic (dis)unification techniques [START_REF] Jouannaud | Solving equations in abstract algebras: a rule-based survey of unification[END_REF] provide a way to perform query analyses similar to the ones briefly discussed for standalone firewalls and to detect covert channels by solving the following equation modulo Flow℘: sent(n, from(x, x ′ ), dest(y, y ′ )) = drop ∧ sent(n, from(x1, x2), dest(y1, y2))

= received(n ′ , from(x, x ′ ), dest(y, y ′ ))

In order to use specific tools and techniques to check the properties of the rewrite system Flow℘, one must represent it as an unconstrained rewrite system. For that, we use the fact that automata used in our constrained rewrite systems are all based on prefix-automata. Since for any prefix-based automaton A, we can compute a finite set of linear terms {t1, . . . , tn} such that ∪irec(ti) = L(A) and (ti, tj) not unifiable for any i = j, we can transform any rule of our con-strained rewrite systems into an equivalent finite set of rules which do not overlap. We obtain a finite left-linear rewrite system containing only trivial overlaps (between rules corresponding to the routing).

CONCLUSION

We have proposed in this paper an approach to describe firewalls using rewrite systems and automata. We have shown that this approach can be used to perform several kinds of analyses not only for standalone firewalls but also for routed networks of firewalls. In both cases we consider firewalls that can handle NAT rules.

We have shown that this rewrite based specification of firewalls is adapted for verifying usual properties related to the semantics of a firewall (such as completeness) and to perform firewall comparisons. We can also detect the so-called misconfigurations and perform query analyses. Moreover, all these analyses can be performed in the same formalisms and using the same tools.

The same rewrite based approach has been used to specify a network topology together with routing rules and firewall policies. The obtained rewrite system provides an executable specification of the network traffic under the security policy and, because of its form (left-linear, etc.), can be used to effectively perform completeness, reachability and consistency verifications. Some properties, like the consistency, are considered w.r.t. a routing policy or for any routing policy.

The modeling hypotheses assumed in this paper allow us to apply the obtained results in real cases. In particular, the automata operations needed here can be performed quite efficiently. Furthermore, one of the main advantages of using rewrite systems is the possibility to use automatic tools for verifying their properties. Indeed, termination of rewrite systems can be proved using A3PAT (CiME) [START_REF] Contejean | A3PAT, an approach for certified automated termination proofs[END_REF], AProVE [START_REF] Giesl | AProVE 1.2: Automatic termination proofs in the dependency pair framework[END_REF] or TTT [START_REF] Korp | Tyrolean termination tool 2[END_REF] for example while confluence can be checked using ACP (Automated Confluence Prover) [START_REF] Aoto | Proving confluence of term rewriting systems automatically[END_REF] and ground confluence with CrC Maude [START_REF] Durán | A Church-Rosser checker tool for conditional order-sorted equational Maude specifications[END_REF]. Moreover, reachability analysis can be performed using Autowrite [START_REF] Durand | Autowrite: A tool for term rewrite systems and tree automata[END_REF][START_REF] Durand | Autowrite version 4[END_REF] (which implements the reachability problem for left-linear growing term rewrite system) or Timbuk [START_REF] Feuillade | Reachability analysis over term rewriting systems[END_REF] and efficient simulations of network traffics can be done using Tom [START_REF] Balland | Tom: Piggybacking rewriting on java[END_REF], ELAN [START_REF] Borovanský | An overview of elan[END_REF] or Maude [START_REF] Clavel | All About Maude -A High-Performance Logical Framework[END_REF].

We have already started the implementation of the approach presented here. The rewrite systems could be automatically generated starting from a given topology and a security policy and the preliminary results are quite promising. Once again, the particular shape of the rules we used allowed relatively quick automatic termination proofs (around 3s for 200 generated rules).

There are numerous perspectives to this work. Let us just mention that we plan to extend the approach in order to take into account statefull firewalls and to model proxy abilities. More precisely, to completely model TCP connections, we will consider sequences of packets instead of single packets. This should allow us to capture other vulnerabilities such as, for example, denial of services caused by unshared memories of firewalls. Moreover, since proxy abilities essentially con-sist in rewriting sequences of packets, rewrite systems seem to be particularly suitable to model them.

Figure 3 :

 3 Figure 3: Example of network topology

  Route G G p ready to be (pre)translated by sh1 DN AT p ′ ready to be filtered by sh1

  Routep ′′ ready to be routed by sh1

Definition 9 (

 9 Completeness). A network security policy ℘ over a network topology τ is complete w.r.t. a routing strategy ζ, or simply ζ-complete, if for any r ∈ Request, there exists d ∈ Decision such that ℘ ζ (r) = d.

Figure 4 :

 4 Figure 4: Rewrite system Flow ℘,ζ computing the traffic under a network security policy ℘ w.r.t. ζ

  sent(secretariat, from(195 , 32 ), dest(49 , 25 )) * route(sh2 :: #, from(195 , 32 ), dest(49 , 25 )) * Ö Ö route(sh3 :: sh2 :: #, from(195 , 32 ), dest(49 , 25 )) * drop pre(sh1 :: sh2 :: #, from(195 , 32 ), dest(49 , 25 )) * route(sh1 :: #, from(17 , 8080 ), dest(49 , 25 )) * route(sh2 :: sh1 :: #, from(17 , 8080 ), dest(49 , 25 )) * route(sh3 :: sh2 :: sh1 :: #, from(17 , 8080 ), dest(49 , 25 )) * received(servers, from(17 , 8080 ), dest(49 , 25 ))

  →R v. If u →R v and v is irreducible w.r.t R, then v is a normal form of u.

		incoming packet	Translation of destination address (DNAT) 1	Filtering rules 2	accept to forward	Translation of source address (SNAT) 3	output packet
			Firewall	drop
				X
			Figure 1: Firewall processing model
	that for every rule l → r is associated to a set of membership
	constraints x ∈ A where x is in Var(l) and A is a regular tree
	language. If l → r is associated to {x1 ∈ A1, . . . , xn ∈ An},
	we write l → r	x1 ∈ A1, . . . , xn ∈ An. The binary
	relation →R induced by a constrained rewrite system R is defined as follows: for any terms t, t ′ , t →R t ′ iff there exists
	a rule l → r a substitution σ such that t |ω = σ(l) and t ′ = t [σ(r)] ω and x1 ∈ A1, . . . , xn ∈ An of R, ω ∈ Pos(t) and such that σ(xi) ∈ Ai for every i.
	Given a rewrite system R, → * R denotes the reflexive transi-
	tive closure of the relation induced by R. For any term v, → -1 R (v) denotes the set {u | u →R v}. For any set of ground terms U ⊆ T , → -1 R (U) denotes the set {u | ∃v ∈ U, u →R v}. A rewrite system R is confluent iff for any terms u, w, v, if u → * R v and u → * R w, then there exists t such that v → * R t and w → * R t. u is irreducible w.r.t R iff there is no v such
	that u

  address src IP address dest Protocol Port src Port dst Decision 192.168.20.1/24 121.130.1.1/28

				tcp	80	any	Accept
	8 <	any Src/Dest	any Address range	any Port range New address : port any any	Drop
	NAT:	Dest	192.168.5.128/25	any	121.130.1.15:80
	:	Src	192.168.20.1/24	80	121.130.1.1:80
		Figure 2: Example of a firewall

  rules of Filter f are of the form p → d where p is a linear term of sort Packet and d a (ground) term of sort Decision; • rules of Pre f and Post f are, respectively, of the form: dest(ip, port) → dest(ip ′ , port ′ ) from(ip, port) → from(ip ′ , port ′ ) where ip, port are linear terms and ip ′ , port ′ are ground terms.

	Example 2. The firewall described in Example 1 can be
	specified as follows. Filter f is the following ordered rewrite
	system:
	8
	<

• : packet " from(192 .168 .20 .1 /24 [x ], 80 ) dest(121 .130 .1 .1 /28 [y], z ) « → accept packet(x , y) → drop while Pre f and Post f consist, respectively, of the rules dest(162 .168 .5 .128 /25 [x ], y) → dest(121 .130 .1 .15 , 80 ) and from(192 .168 .20 .1 /24 [x ], 80 ) → from(121 .130 .1 .1 , 80 ).

  Definition 8 (Semantics of a security policy w.r.t. a routing strategy). Given a network security policy ℘ over a topology τ and a routing strategy ζ sound w.r.t. τ , we call semantics of ℘ w.r.t. ζ and we denote by ℘ ζ the (partial or total) function associating any request r ∈ Request with a decision d ∈ Decision, when it exists, such that r Flow ℘,ζ d with Flow ℘,ζ the term rewrite system defined in Figure

*

-→

  Definition 10 (Consistency). A network security policy ℘ over a network topology τ is consistent iff for any routing strategies ζ and ζ ′ sound w.r.t. τ , ℘ ζ = ℘ ζ ′ .

	@ @ P P P P P P P P P
	We express the consistency of a policy as a property over a
	new rewrite system. Given a network security policy ℘, we
	define Flow℘ as the left-linear rewrite system describing all

possible packet traversal scenarios w.r.t. any sound routing strategy, i.e. which rewrites any request r into d ∈ Decision iff there exists a strategy ζ such that ℘ ζ (r) = d and which rewrites it into a normal form which is not a decision if there exists no ζ such that r ∈ D( ℘ ζ ). The way the rewrite system Flow℘ is build starting from the rules in Figure 4 is detailed in Appendix B. Roughly speaking, it chooses nondeterministically all the possible routes in order to reach all the possible decisions. If we have explored a path which does not lead to a decision, then the term backtracks: p * v v m m m m m m m m m * p ′ = ℘ ζ for some ζ p ′′ = ℘ ζ for all ζ

192.168.20.1/24 = [192.168.20.1, 192.168.20.255], 121.130.1.1/28 = [121.130.1.1, 121.130.1.15]

A subnetwork is a logically visible subdivision of a network characterized by an IP ranges (its domain).

R; {x → x} is the rewrite system R in which the rule x → x has been added as the last rule.

Note that without loss of generality, we can consider that any subnetwork has only one gateway. If one wants to describe a topology in which a subnetwork is connected to several security hosts, it suffices to add an intermediate security host.

APPENDIX A. EXTENSION OF JACQUEMARD'S RE-SULT TO CGRS

Without restriction, we can consider that any CGRS is a set of rules of one of the following forms

f (x1, . . . , xn) → r[x1, . . . , xn] x1 ∈ A1, . . . , xn ∈ An [START_REF] Al-Shaer | Conflict classification and analysis of distributed firewall policies[END_REF] knowing that any unconstrained variable x can be seen as a variable constrained by x ∈ A where A is the automaton recognizing all ground terms. Thus, we consider that any variable is constrained.

Let be L a regular language recognized by AL and R a CGRS. The automaton recognizing (→ * R ) -1 (L) is built as follows:

where the disjoint sum (⊎) of two automata over the same signature is the automaton whose set of states, set of final states and set of rules are the union of corresponding sets of the two automata, provided that they are all disjoint. Then, we transform ∆ k (k ≥ 0) into ∆ k+1 by applying the following rules:

i is a final state of Ai 2. for all 1 ≤ j ≤ m, there exists a substitution θ : X → Q such that θ(rj) * -→∆ k qj and for each xi occurring in g(r1, . . . , rm), we have θ(xi) = q ′ i .

(ii)

The desired automaton is Reach = (Q, QL, ∆) where QL is the set of final states of AL.

B. REWRITE SYSTEM ASSOCIATED TO A SECURITY POLICY

Given a network security policy ℘, we define Flow℘ as the rewrite system built out from the following signature:

→ route(q, x, y). Roughly speaking, the term t1, . . . , tn s indicates that the packet is currently treated by the security host s and that the packet went through s i iff ti = ⊤. If the packet is translated, then the trace is reinitialized since from the network point of view this is another packet.


Gaelle Lachenal

Karin Pernet-Gallay

Mathilde Chivet

Fiona J Hemming

Agnès Belly

Gilles Bodon

Béatrice Blot

Georg Haase

Yves Goldberg

Rémy Sadoul
email: remy.sadoul@ujfgrenoble.fr.

Release of exosomes from differentiated neurons and its regulation by synaptic glutamatergic activity

Keywords: exosomes, multivesicular bodies, tetanus toxin, synaptic activity

A bstract E xosomes are microvesicles released into the extracellular medium upon fusion to the plasma membrane of endosomal intermediates called multivesicular bodies. T hey represent ways for discarding proteins and metabolites and also for intercellular transfer of proteins and R N As. In the nervous system, it has been hypothesized that exosomes might be involved in the normal physiology of the synapse and possibly allow the trans-synaptic propagation of pathogenic proteins throughout the tissue. As a first step to validate this concept, we used biochemical and morphological approaches to demonstrate that mature cortical neurons in culture do indeed secrete exosomes. Using electron microscopy, we observed exosomes being released from somato-dendritic compartments. T he endosomal origin of exosomes was demonstrated by showing that the C -terminal domain of tetanus toxin specifically endocytosed by neurons and accumulating inside multivesicular bodies, is released in the extracellular medium in association with exosomes. F inally, we found that exosomal release is modulated by glutamatergic synaptic activity, suggesting that this process might be part of normal synaptic physiology. T hus, our study paves the way towards the demonstration that exosomes take part in the physiology of the normal and pathological nervous system.

Introduction

Cell to cell communication can occur through exchange of membrane vesicles. Some are generated inside endosomes and released upon fusion to the plasma membrane of endosomal intermediates called multivesicular bodies (MVBs) [START_REF] Pan | Electron microscopic evidence for externalization of the transferrin receptor in vesicular form in sheep reticulocytes[END_REF]. In this latter case, the released intralumenal vesicles are referred to as exosomes. Since their original discovery in reticulocytes, exosomes were found to be secreted by an increasing number of cells and could be isolated from most body fluids including cerebral spinal fluid (Vella et al., 2008a). However, in most cases their physiological relevance has been difficult to show due to a lack of information on their biogenesis, origin and regulation.

MVB intraluminal vesicles contain proteins meant for degradation, which occurs upon fusion of the limiting membrane of MVBs with lysosomes [START_REF] Futter | Multivesicular endosomes containing internalized EGF-EGF receptor complexes mature and then fuse directly with lysosomes[END_REF].

Until a decade ago, their release as exosomes was mainly regarded as a way of eliminating membrane material from cells, or cell compartments, lacking lysosomes.

Exosomes also represent an alternative pathway for secretion of soluble proteins lacking signal sequences, or of membrane proteins [START_REF] Qu | Nonclassical IL-1 beta secretion stimulated by P2X7 receptors is dependent on inflammasome activation and correlated with exosome release in murine macrophages[END_REF][START_REF] Zhang | A membrane form of TNF-alpha presented by exosomes delays T cell activation-induced cell death[END_REF]. Other functions deal with intercellular communication, as in the case of naïve dendritic cells, which become immuno-competent after binding and endocytosis of exosomes secreted by other activated dendritic cells. [START_REF] Morelli | Endocytosis, intracellular sorting, and processing of exosomes by dendritic cells[END_REF][START_REF] Thery | Indirect activation of naive CD4+ T cells by dendritic cell-derived exosomes[END_REF]. Exosomes released by mast cells were reported to contain RNAs including microRNAs and mRNAs, which modulate protein expression of receiving cells [START_REF] Skog | Glioblastoma microvesicles transport RNA and proteins that promote tumour growth and provide diagnostic biomarkers[END_REF][START_REF] Valadi | Exosome-mediated transfer of mRNAs and microRNAs is a novel mechanism of genetic exchange between cells[END_REF]. Thus, exosomes represent a way of transferring material between cells, allowing emitting cells to modify protein expression of receiving cells.

Exosomes have been proposed to be a novel way for intercellular communication contributing to the normal physiology of the nervous system and to the trans-synaptic transmission of pathogenic proteins [START_REF] Fevrier | Exosomes: a bubble ride for prions?[END_REF][START_REF] Smalheiser | Exosomal transfer of proteins and RNAs at synapses in the nervous system[END_REF]Vella et al., 2008b). In line with this, several reports have described release of exosomes by cultured astrocytes [START_REF] Taylor | Regulation of heat shock protein 70 release in astrocytes: role of signaling kinases[END_REF], microglial cells [START_REF] Potolicchio | Proteomic analysis of microglia-derived exosomes: metabolic role of the aminopeptidase CD13 in neuropeptide catabolism[END_REF], oligodendrocytes [START_REF] Krämer-Albers | Oligodendrocutes secrete exosomes containing major myelin and stress-protective proteins: Trophic suppor for axons ?[END_REF] and developping neurons [START_REF] Faure | Exosomes are released by cultured cortical neurones[END_REF]. However there has been no definite proof that mature neurons can secrete exosomes or that this process is regulated by neuronal activity. Here we demonstrate that i) fully differentiated cortical and hippocampal neurons in culture do indeed secrete vesicles having the biochemical and morphological features of exosomes, ii) these vesicles do correspond to intralumenal vesicles of MVBs since they contain on their surface TTC, the C-terminal domain of tetanus-toxin, which is endocytosed by neurons and accumulates inside MVBs and iii) exosomal secretion by neurons is regulated by calcium influx and by glutamatergic synaptic activity. Thus our results definitively endorse the role of exosomes in the normal physiology of the central nervous system.

M aterial and M ethods

Reagents:

Polyclonal anti-Alix has been previously described [START_REF] Chatellard-Causse | Alix (ALG-2-interacting protein X), a protein involved in apoptosis, binds to endophilins and induces cytoplasmic vacuolization[END_REF].

Polyclonal anti-L1 CAM was a kind gift of F. Rathjen (Max-Delbrück-Centrum, Berlin, Germany). Polyclonal anti-GluR2 and anti-GluR2/3 were purchased from Millipore and Chemicon respectively. Monoclonal antibody against the N-terminal part of GluR2 used for electron microscopy was from Chemicon. Monoclonal anti-GFP was from Covance, and monoclonal antibody against flotillin-1 was obtained from BD Transduction Laboratories.

Ionomycine, picrotoxin, CNQX, MK801 were purchased from Sigma and bicucullin from Fluka.

TTC proteins: construction of pGEX plasmids coding for GST-GFP-TTC or GST-GFP have been described in [START_REF] Bordet | Neuronal targeting of cardiotrophin-1 by coupling with tetanus toxin C fragment[END_REF]. Proteins were expressed in BL21 E. coli and purified on a glutathion-Sepharose 4b column (Amersham) as described [START_REF] Bordet | Neuronal targeting of cardiotrophin-1 by coupling with tetanus toxin C fragment[END_REF]. After dialysis against PBS containing 0.5 M NaCl and 5% glycerol, proteins were centrifuged at 100 000 g for 1 h to remove insoluble proteins.

Fusion proteins were incubated on neurons at 4 g/ml in culture medium.

Primary cultures of cortical and hippocampal neurons:

Cells were prepared from embryonic day 19 (E19) rat embryos as described (Fauré et al, 2006). After dissociation cortical neurons were seeded at 10 5 cells/cm 2 onto 100 mm dishes precoated with poly-D-lysine (50 μg/ml, Sigma). Hippocampal neurons, cells were seeded at 1.3 x 10 4 cells/cm 2 . Cells were cultured in Neurobasal (Gibco) supplemented with 2% B27 (Gibco), 1 mM sodium pyruvate, 2 mM glutamine and antibiotics in a humidified incubator at 37°C and 5% CO 2 . 25% freshly made medium containing cytosine -D-arabinoside (AraC) at a final concentration of 10 M (cortical neurons) or 5 M (hippocampal neurons) was added every 4 th day.

Immunostaining of 15 DIV cultures with a monoclonal antibody against GFAP, revealed staining of only 1 to 2% of cells, demonstrating minimal contamination by astrocytes.

Purification of exosomes:

Exosomes were purified from 15 DIV cortical neurons or from 21 DIV hippocampal neurons. Cells were washed two times in K5 medium (5 mM KCl, 1.8 mM CaCl 2 , 0.8 mM MgSO 4 , 110 mM NaCl, 26 mM NaHCO 3 , 1 mM NaH 2 PO 4 , 0.7% D-glucose and 15 mM HEPES, pH 7.4). Cells were then incubated in the same medium, with or without stimulation, for the indicated times of harvest, after which media were collected and cleared of debris by two successive centrifugation steps (2 000 g for 10 min, 20 000 g for 20 min) and filtration through a 0.22 m filter (GVA, Millipore).

Exosomes were recovered by centrifugation for 50 min at 100 000 g. They were resuspended in Laemmli buffer for Western blot analysis or further separated over a sucrose gradient. For this, the 100 000 g pellets were resuspended in sucrose 0.211 M, 3mM imidazole pH 7.4, and loaded onto a continuous 0.211 M to 2.255 M sucrose gradient. Gradients were centrifuged 18 h at 100 000 g, and one ml fractions were collected, diluted in 3 mM Imidazole, pH 7.4, and centrifuged for 1 h at 100 000g.

Pellets were resuspended in Laemmli buffer and analysed by Western-blot.

For short term harvests each lane corresponds to exosomes pelleted at 100 000 g from the medium of 1.2 x 10 7 cells (estimated at the time of seeding). Gradient analyses were performed using vesicles recovered from media of 3.6 x 10 7 cells. Cells were lysed in RIPA buffer and the equivalent of 6 x10 3 cells/ lane were loaded.

Treatments included: depolarisation by incubation in K25 (25 mM KCl, 1.8 mM CaCl 2 , 0.8 mM MgSO 4 , 90 mM NaCl, 26 mM NaHCO 3 , 1 mM NaH 2 PO 4 , 0.7% Dglucose and 15 mM HEPES, pH 7.4). All other treatments were performed for the times indicated in K5 medium: ionomycin was used at 2 μM, BAPTA-AM at 50 μM, bicucullin and picrotoxin at 40 μM, MK801 at 1 μM and CNQX at 100 μM.

Semi-quantificative analysis of W estern blots:

Autoradiographs were scanned (Duoscan f40, AGFA) at 800dpi. Total grey values were obtained using Metamorph software (Meta Imaging Series Version 7.5.6.0, MDS Analytical Technologies). For each experiment, triplicates were made from at least three different cultures. Histograms represent the means of ratios between each grey value of one exosomal pellet to the corresponding lysate.

Electron microscopy:

Exosome pellets were immediately fixed by 2% paraformaldehyde, applied to formvar-carbon-coated EM grids and stained with 5% uranyl acetate for 1 min. For immunogold labelling, grids were incubated with primary antibodies as indicated, which were then revealed using protein A gold. The exosomes were then stained with uranyl acetate as described above.

For morphological analysis, cultures of cortical or hippocampal neurons were stimulated for 1 min with 2 μM ionomycin. Neurons were then fixed immediately in 2.5% glutaraldehyde in cacodylate buffer 0.1 M pH 7.2, for at least 2 h. Neurons were post-fixed by 1% osmium tetroxyde in cacodylate buffer 0.1 M for 1 h, stained overnight in 0.5% uranyl acetate, washed and dehydrated in a graded series of ethanol before inclusion in Epoxy resine (Fluka, Sigma). Ultrathin sections of 70 nm were cut with an ultramicrotome (Leica, ultracut S) and stained with uranyl acetate 5% and lead citrate.

For immunogold labelling, cells were incubated overnight with GFP-TTC, washed three times in K5 medium, incubated with 2 μM ionomycin for 1 min and fixed with 2% paraformaldehyde. Cells were then incubated with anti-GFP antibodies and protein A coupled to gold particles before inclusion as described above.

For cryomicroscopy, GFP-TTC was incorporated as described above and the cells fixed with 2% paraformaldehyde, 0.2% glutaraldehyde in cacodylate buffer 0.1M. Cells were scratched off the substrate and centrifuged at 1200 rpm for 5 min. Pellets were then embedded in gelatine, cryo-protected in 2.3 M sucrose and frozen in liquid nitrogen. Sections of 70 nm were cut using a cryo-ultramicrotome (Reichert Ultracut S, Leica) and immunolabelling was performed according to Tokuyasu [START_REF] Tokuyasu | Application of cryoultramicrotomy to immunocytochemistry[END_REF]. Observations were made using a transmission electron microscope (JEOL JEM 1200 EX) at 80 kV, equipped with a digital camera (Veleta, SIS).

Results

E xosomal release from mature neurons is regulated by calcium.

Exosomes are homogeneous in size (40-100 nm) and shape and even though their protein composition depends on the cell type of origin, some proteins like Alix or flotillin-1 have emerged as exosomal marker proteins [START_REF] Mathivanan | ExoCarta: A compendium of exosomal proteins and RNA[END_REF]. We have previously demonstrated that primary neurons from E 19 rat cortex cultured for 9 days release exosomes and that this release is stimulated during prolonged depolarisation (3 h) with medium containing 25 mM KCl [START_REF] Faure | Exosomes are released by cultured cortical neurones[END_REF]. These cultures are not fully differentiated, meaning that neurite outgrowth still occurs and that very few synapses can be observed. In order to show that exosomal release is not only a property of developing neurons, we used here cortical neurons cultured for 15 days to allow full differentiation [START_REF] Chiappalone | Dissociated cortical networks show spontaneously correlated activity patterns during in vitro development[END_REF]. After washing, the cultures were incubated in harvesting medium containing 5 mM KCl (K5) or in the same medium containing 25 mM KCl (K25). Media were harvested after 3 h, vesicles pelleted by ultracentrifugation and further separated using a continuous sucrose gradient. As shown in Fig. 1, immunoblotting of each fraction using an antibody against flotillin-1 revealed weak immunoreactivity in fraction 5 from K5 cell-supernatants and strong reactivity peaking between fractions 4 and 7 from K25 supernatants. This corresponds to densities of 1.09 and 1.15 g/ml sucrose, as expected for exosomes (Fig. 1). Alix was mainly detected in fractions 4 to 6 of K25 supernatants. The cell adhesion molecule L1, a transmembrane protein, which in the central nervous system is only expressed by neurons [START_REF] Maness | Neural recognition molecules of the immunoglobulin superfamily: signaling transducers of axon guidance and neuronal migration[END_REF], was present in exosomal fractions of the same supernatants showing that exosomes are released by neurons. Immunoreactivity against GluR2/3 showed that subunits of AMPA receptors are also secreted by way of exosomes. These results demonstrate that mature neurons secrete exosomes and that this process is enhanced by depolarisation.

In order to examine whether this secretion can be regulated, we next used a harvesting time of 5 min to avoid long term effects of treatments on endosomal trafficking. Using 100 000 g centrifugation, we found that harvested media contained pelletable material positive for Alix, flotillin-1 and L1 (Fig. 2). In this case the amount of material was too small to allow separation over sucrose gradients; we therefore used electron microscopy to demonstrate that the 100 000g pellets contained exosomes. Indeed, released vesicles harvested after 5 min had the size (50-100 nm) and erythrocyte-like shape typical of exosomes. (Fig. 2D). The neuronal origin of these vesicles was demonstrated by their labelling with antibodies against L1 and the AMPA receptor subunit GluR2 (Fig. 2D, bottom panel).

Using a 5 min harvest, we found that incubation of neurons with the calcium inonophore ionomycin to induce calcium influx, significantly increased exosomal release (Fig. 2A andB). Similar results were found using 21 DIV hippocampal neurons (Fig. 2C). Preincubation of cortical neurons for 15 min with BAPTA-AM, to chelate intracellular calcium, partially blocked the ionomycin effect, thus demonstrating that the enhancement of exosomal release observed during a 5 min incubation with the ionophore is indeed due to an increase in intracellular calcium (Fig. 2E andF).

E lectron-microscopic examination of cultured neurons reveals the presence of released exosomes in close apposition to the plasma membrane.

Electron microscopic examination of 15 DIV cortical neurons treated 1 min with ionomycin showed the presence of extracellular clusters of vesicles in close vicinity of the plasma membrane of dendrites (Fig. 3B right panel) and of the soma (Fig. 3B left panel). Similar clusters were seen, albeit less frequently, on the surface of untreated 15 DIV (not shown) or 8 DIV cultures (Fig. 3A). The size (40 to 80 nm) was compatible to the one of vesicles harvested from culture supernatants (Fig. 2D). Moreover the size and number of vesicles were also in the same range as those observed inside MVBs (Fig. 3A andB). In rare cases, profiles of MVB compartments in continuity with the plasma membrane could be observed (Fig. 3C). Dense material probably contained in MVBs was released together with exosomes.

G F P-T T C is released by way of exosomes.

In order to further prove that exosomes harvested by centrifugation and observed in association with the plasma membrane originate in neuronal endosomal compartments, we made use of TTC, the C terminal 451-amino-acid fragment of the Tetanus toxin heavy chain. Numerous observations have shown that the recombinant protein fused to GFP or enzymes, binds specifically to-and is endocytosed by neurons similarly to the native toxin [START_REF] Bordet | Neuronal targeting of cardiotrophin-1 by coupling with tetanus toxin C fragment[END_REF] [START_REF] Francis | Tetanus toxin fragment C as a vector to enhance delivery of proteins to the CNS[END_REF]). Here we produced GFP-tagged TTC (GFP-TTC) and GFP as recombinant GST fusion proteins in bacteria. Cortical neurons cultured for 15 DIV were then incubated for 1h at 37°C with GFP-TTC or GFP before extensive washing. Using epi-fluorescence, endocytosed GFP-TTC was seen inside punctuate structures in both soma and dendrites, whereas GFP alone was undetectable (not shown). To test whether GFP-TTC is secreted in association with exosomes, neurons pre-incubated with GFP-TTC or GFP, were extensively washed and incubated in fresh medium. The media were harvested after 5 min., exosomes centrifuged at 100 000 g and analysed by Western-blotting using anti-GFP and antiflotillin-1 antibodies. GFP-TTC, but not GFP, was present in these 100 000 g pellets (Fig. 4A). The amount of released GFP-TTC pelleted by ultracentrifugation was significantly increased upon treatment of neurons with 2 M ionomycin further suggesting that GFP-TTC is released in association with exosomes (Fig. 4C). We next used density separation to further prove that after endocytosis by neurons, GFP-TTC is secreted in association with exosomes. Neurons were preincubated with GFP-TTC, extensively washed and vesicles harvested during 2 h were further separated on a sucrose gradient. Western blotting analysis using antibodies against GFP revealed a peak of GFP-TTC in the 1.12 g/ml fraction, in which flotillin positive exosomes are concentrated (Fig. 4B). As expected from the result shown in Fig. 4A, no GFP could be detected in any fractions of exosomes prepared from neurons which had been preincubated with GFP alone (not shown). The most straight-forward explanation as to why GFP-TTC is detected at this sucrose density is that it is bound to exosomes. These data prove that exosomes secreted by neurons stem from intracellular compartments, which contain endocytosed proteins.

In order to demonstrate that these endosomes are indeed MVBs, we used immunogold to label cryosections of cultured neurons pre-incubated with GFP-TTC.

As shown in Fig. 4D, some of the anti-GFP labelling was found inside MVB compartments which is in good agreement with data from Schiavo and collaborators using recombinant TTC coupled to horse radish peroxydase [START_REF] Deinhardt | Tetanus toxin is internalized by a sequential clathrin-dependent mechanism initiated within lipid microdomains and independent of epsin1[END_REF].

Anti-GFP labelling before inclusion and sectioning of the cultured neurons preincubated with GFP-TTC, demonstrated the presence of immunogold labelling on exosomes present in extracellular clusters at the neuron surface (Fig. 4E). Thus, our experiments strongly suggest that the packets of exosomes seen in association with dendrites of 15 DIV cultured neurons correspond to intralumenal vesicles of MVBs released upon fusion of the latter with the plasma membrane.

E xosome secretion is regulated by glutamatergic activity

We finally tested whether secretion of exosomes might be regulated by synaptic activity. For this we used two antagonists of GABA A receptors, bicucullin or picrotoxin, to block inhibitory activity in the cultures and thereby enhance glutamatergic spontaneous activity. As shown in Fig. 5A andB, massive increase in release of exosomes detected by flotillin-1, Alix and L1 was detectable after a 10 min treatment with bicucullin. Antibodies against the Na+/K+ ATPase, a plasma membrane resident protein, did not reveal the presence of the protein in the same fractions, thus demonstrating that the vesicles harvested from neurons treated with or without bicucullin do not contain plasma membrane contaminants (not shown). Addition of the AMPAR antagonist CNQX to the cultures together with bicucullin inhibited this increase, demonstrating that secretion is modulated by synaptic AMPA receptor activity. MK-801, which antagonises NMDA receptors also blocked the bicucullin induced increase in exosome secretion (Fig. 5A andB). Therefore exosome secretion is modulated by synaptic AMPA-and NMDA-receptors. Picrotoxin also increased the release of exosomes immuno-revealed using anti-flotillin and GluR2 further demonstrating that this process is regulated by glutamatergic activity (Fig. 5C).

Discussion

Vesicles released from living cells are the subject of numerous studies as they represent ways of secreting cytoplasmic proteins, membrane proteins and RNAs [START_REF] Belting | Nanotubes, exosomes, and nucleic acid-binding peptides provide novel mechanisms of intercellular communication in eukaryotic cells: implications in health and disease[END_REF]. Secretion of membrane particles was demonstrated to occur directly from the plasma membrane of neuroepithelial cells [START_REF] Marzesco | Release of extracellular membrane particles carrying the stem cell marker prominin-1 (CD133) from neural progenitors and other epithelial cells[END_REF], microglia [START_REF] Bianco | Astrocyte-derived ATP induces vesicle shedding and IL-1 beta release from microglia[END_REF], astrocytes [START_REF] Bianco | Acid sphingomyelinase activity triggers microparticle release from glial cells[END_REF] or glioblastoma cells [START_REF] Skog | Glioblastoma microvesicles transport RNA and proteins that promote tumour growth and provide diagnostic biomarkers[END_REF]. Vesicles can also be released from intracellular compartments of unknown origin as in the case of enlargeosomes released by PC12 cells [START_REF] Borgonovo | Regulated exocytosis: a novel, widely expressed system[END_REF]. The best-characterised membrane vesicles are exosomes, which correspond to intralumenal vesicles of MVBs released after fusion of the latter to the plasma membrane [START_REF] Simons | Exosomes -vesicular carriers for intercellular communication[END_REF]. Exosomes represent a way of intercellular exchange of both RNAs and proteins, which allows emitting cells to modify protein expression in receiving cells. In the adult nervous system exosomes were hypothesized to supplement the known mechanisms of anterograde and retrograde signalling across synapses i.e. represent a novel way for intercellular exchange of material within neural networks [START_REF] Smalheiser | Exosomal transfer of proteins and RNAs at synapses in the nervous system[END_REF] [START_REF] Aguzzi | The transcellular spread of cytosolic amyloids, prions, and prionoids[END_REF]Vella et al., 2008b). Even appealing this hypothesis faces the lack of demonstration of exosomal release by mature neurons. Among the reports claiming secretion of exosomes by neurons [START_REF] Ghidoni | Cystatin C is released in association with exosomes: A new tool of neuronal communication which is unbalanced in Alzheimer's disease[END_REF][START_REF] Putz | Nedd4 family-interacting protein 1 (Ndfip1) is required for the exosomal secretion of Nedd4 family proteins[END_REF][START_REF] Vingtdeux | Alkalizing drugs induce accumulation of amyloid precursor protein by-products in luminal vesicles of multivesicular bodies[END_REF], only [START_REF] Ghidoni | Cystatin C is released in association with exosomes: A new tool of neuronal communication which is unbalanced in Alzheimer's disease[END_REF] separated by density centrifugation exosomes from other vesicles harvested from culture supernatants. None of the reports used markers to ensure the neuronal origin of the secreted vesicles. Furthermore, no demonstration was made of the endosomal origin of the putative exosomes. Finally all these reports used embryonic neurons cultured for only 3 to 7 days; our previous demonstration of exosome release by neurons made use of embryonic cortical neurons cultured for 8 to 9 days [START_REF] Faure | Exosomes are released by cultured cortical neurones[END_REF]. In such cultures, neurite outgrowth is still ongoing and exosomal release might simply reflect the fusion of late endosomeslysosomes at growth cones, a process necessary for neurite elongation [START_REF] Arantes | A role for synaptotagmin VII-regulated exocytosis of lysosomes in neurite outgrowth from primary sympathetic neurons[END_REF]). Here we used several appoaches to show that cortical neurons cultured for 15 days, which have undergone synaptogenis and made functional networks [START_REF] Chiappalone | Dissociated cortical networks show spontaneously correlated activity patterns during in vitro development[END_REF] release exosomes. We also show that exosomal release is regulated by synaptic glutamatergic activity and might thus be part of normal synaptic physiology.

Our demonstration that the features of vesicles released by differentiated neurons correspond to those of exosomes is five fold: 1) their floating between 1.09 and 1.15 g/ml of sucrose; 2) their characteristic Alix and flotillin-immunoreactivities; 3) their size and shape as observed by electron microscopy; 4) their association with the Cterminal half of tetanus toxin which is endocytosed specifically by neurons and accumulates inside MVBs; 5) the presence of clusters of vesicles near dendrites, which have the size and shape similar to those found inside MVBs and are labelled with GFP-TTC.

As in the case for exosomes secreted from 8 DIV cultures [START_REF] Faure | Exosomes are released by cultured cortical neurones[END_REF], exosomes released by 15 DIV neurons carried the cell adhesion molecule L1 and GluR2/3 subunits of AMPA receptors. The presence of both proteins inside MVBs, which was reported by others [START_REF] Utvik | Neuronal enriched endosomal protein of 21 kDa colocalizes with glutamate receptor subunit GLUR2/3 at the postsynaptic membrane[END_REF][START_REF] Yap | The somatodendritic endosomal regulator NEEP21 facilitates axonal targeting of L1/NgCAM[END_REF], is compatible with our conclusion that exosomes characterised in our study indeed correspond to MVB intralumenal vesicles of neurons. We verified that this is indeed the case by making use of GFP-TTC. In primary cultures, this protein is specifically endocytosed by neurons, a property afforded by TTC which binds to cell surface gangliosides and a GPI-linked receptor [START_REF] Bordet | Neuronal targeting of cardiotrophin-1 by coupling with tetanus toxin C fragment[END_REF][START_REF] Herreros | Lipid rafts act as specialized domains for tetanus toxin binding and internalization into neurons[END_REF]. In agreement with published results, we observed by EM that the endocytosed protein accumulates inside neuronal MVBs. Enrichment of GFP-TTC in sucrose fractions containing exosomes harvested from neurons having endocytosed GFP-TTC demonstrated that the water soluble protein is bound to exosomes. The protein was also detected by EM on exosomes present in extracellular clusters close to the neuronal surface. Altogether these findings demonstrate that endocytosed GFP-TTC is secreted by way of exosomes and that neuronal exosomes characterised throughout our study stem from MVBs.

Thus, our finding that 15 DIV mature cortical neurons secrete exosomes at the level of soma and dendritic shafts was crucial to demonstrate that this process might be part of the physiology of differentiated neuron and is unrelated to growth cone development.

Even if several cell stimuli lead to an increase in exosome secretion by non neuronal cells [START_REF] Thery | Membrane vesicles as conveyors of immune responses[END_REF], there is today no clear indication that MVB fusion is regulated. In most cell types, a rise in cytosolic calcium is necessary to induce regulated secretion [START_REF] Gerber | Molecular determinants of regulated exocytosis[END_REF]. The lack of information about a possible calcium dependent fusion of MVBs to the plasma membrane is due to the length of exosome harvest necessary to detect exosomes (ranging from several hours to several days) (see for example [START_REF] Fader | Induction of autophagy promotes fusion of multivesicular bodies with autophagic vacuoles in k562 cells[END_REF][START_REF] Ostrowski | Rab27a and Rab27b control different steps of the exosome secretion pathway[END_REF][START_REF] Savina | Rab11 promotes docking and fusion of multivesicular bodies in a calcium-dependent manner[END_REF]. Such a long-term rise in calcium could be misleading in that it affects endosomal traffic and potentially the number of MVBs without regulating secretion per se. The best evidence, so far, for a role of calcium in exosomal release was given by Qu et al., who reported, a slight increase in exosomal release by macrophages during a 15 min ATP stimulation [START_REF] Qu | P2X7 receptor-stimulated secretion of MHC class II-containing exosomes requires the ASC/NLRP3 inflammasome but is independent of caspase-1[END_REF]. Here we managed to show a strong increase in exosomal release from mature neurons within 5 min of ionomycin treatment, that is abolished by BAPTA-AM. Using EM we also found that the number of extracellular clusters near neuronal surfaces is increased upon 1 min treatment with ionomycin. Even if this is to our knowledge, the best suggestion so far that calcium regulates fusion of MVBs to the plasma membrane, the definite proof will await real time video microscopy to study this process.

By analogy to other cells, one might consider exosomes as a way of discarding proteins. In the cortex and hippocampus, regulation of the number of ionotropic glutamate receptors expressed at the post-synaptic membrane is crucial to modulate efficacy of synapses. It is now well documented that this regulation involves calcium regulated endocytosis and exocytosis from endosomal pools of receptors but little is known about how degradation contributes to this equilibrium [START_REF] Kennedy | Organelles and trafficking machinery for postsynaptic plasticity[END_REF][START_REF] Newpher | Glutamate receptor dynamics in dendritic microdomains[END_REF]. The presence of GluR2 subunits in neuronal exosomes together with the enhanced secretion of exosomes following glutamatergic synaptic activation, underlines exosomal release as a possible mechanism for the local elimination of receptors at synapses undergoing plastic changes. The loss of AMPA receptors upon extensive synaptic activation could be a mechanism of homeostatic synaptic scaling, which is necessary to adjust the strength of all of a neuron's excitatory synapses to stabilize firing {Turrigiano, 2008 #5243}. As distal dendrites are devoid of lysosomes, regulation of the pool of surface synaptic receptors by exosome secretion would avoid retrograde transport of MVBs to lysosomes in proximal dendrites and soma. In vivo, MVBs are relatively sparse and mostly found within dendritic shafts but rarely inside spines [START_REF] Cooney | Endosomal Compartments Serve Multiple Hippocampal Dendritic Spines from a Widespread Rather Than a Local Store of Recycling Membrane[END_REF]. However, movements or maturation of MVBs in spines is tightly regulated by synaptic activity or neurotrophic factors [START_REF] Popov | A cell adhesion molecule mimetic, FGL peptide, induces alterations in synapse and dendritic spine structure in the dentate gyrus of aged rats: a three-dimensional ultrastructural study[END_REF][START_REF] Rind | Synaptic targeting of retrogradely transported trophic factors in motoneurons: comparison of glial cell line-derived neurotrophic factor, brain-derived neurotrophic factor, and cardiotrophin-1 with tetanus toxin[END_REF]. One important step will now be to test whether fusion of MVBs to the plasma membrane occurs at the level of spines or of dendritic shafts.

Exosomes released by mast cells and dendritic cells where shown to be captured by other cells which can make use of the exosomal proteins and RNAs [START_REF] Morelli | Endocytosis, intracellular sorting, and processing of exosomes by dendritic cells[END_REF][START_REF] Thery | Indirect activation of naive CD4+ T cells by dendritic cell-derived exosomes[END_REF]. If such mechanisms allow material transfer between neurons they would be ideally suited to regulate protein expression and thereby plasticity inside neuronal networks [START_REF] Smalheiser | Exosomal transfer of proteins and RNAs at synapses in the nervous system[END_REF]. In line with this, a recent report, Korkut et al. demonstrated a vesicular trans-synaptic communication of Wnt at the Drosophila neuromuscular junction and suggested that this occurs through exosome transfer [START_REF] Korkut | Trans-synaptic transmission of vesicular Wnt signals through Evi/Wntless[END_REF]. Exosomal transfer would also allow the spreading of pathogenic agents throughout the central nervous system during the course of neurodegenerative diseases [START_REF] Aguzzi | The transcellular spread of cytosolic amyloids, prions, and prionoids[END_REF]Vella et al., 2008b). The fact that TTC is secreted by way of exosomes adds some weight to this hypothesis since in vivo the recombinant protein behaves like intact Tetanus toxin, being endocytosed at synapses, retrogradely transported inside endosomes and crossing synapses [START_REF] Cordero-Erausquin | Dorsal horn neurons presynaptic to lamina I spinoparabrachial neurons revealed by transynaptic labeling[END_REF][START_REF] Maskos | Retrograde trans-synaptic transfer of green fluorescent protein allows the genetic mapping of neuronal circuits in transgenic mice[END_REF] [START_REF] Deinhardt | Tetanus toxin is internalized by a sequential clathrin-dependent mechanism initiated within lipid microdomains and independent of epsin1[END_REF]. Our present work showing that differentiated neurons secrete exosomes stemming from MVBs in a way regulated by synaptic activity is a first step towards the demonstration of their function in the normal and pathological nervous system.

L egends to F igures F igure 1: W estern blot analysis of secreted vesicles separated on a continuous density gradient.

After washing, 15 DIV cortical neurons were incubated in fresh K5 medium or depolarising medium containing 25 mM KCl (K25). 3 h later, vesicles harvested from 3.6 x10 7 cells were pelleted at 100 000 g. The vesicles were then separated on a continuous sucrose gradient. One ml fractions were collected and analysed by Western blot using antibodies against L1, GluR2/3, Alix and Flotillin-1. (TCL: Total cell lysates; Inp: 10% of the vesicles pelleted at 100 000 g before separation on the sucrose gradient.) C . Hippocampal neurons (21 DIV) were incubated for 5 min in fresh medium (Ctrl) or in fresh medium containing 2 μM ionomycin (Iono). Exosomes released during these 5 min incubations were pelleted at 100 000 g and analysed by Western-blot using the indicated antibodies. (TCL: Total cell lysate) D. Characterisation of exosomes released during 5 min.

Electron microscopy examination of vesicles secreted by 15 DIV cortical neurons during 5 min and pelleted at 100 000 g. (bar: 100nm).

Bottom panels: Immunogold labelling of the same preparation using antibodies against L1 CAM (left) and GluR2 (right).

E . B APT A-A M inhibits the increase of exosomal release due to ionomycin.

Cortical neurons were preincubated for 15 min in medium with or without 50 M BAPTA-AM. Neurons were then washed and incubated in fresh medium containing 2 M ionomycin during the 5 min harvest. Exosomes were pelleted at 100 000 g and analysed by Western blots using the antibodies indicated. A. Cortical neurons were incubated at 37°C with GFP-TTC or GFP (4 g/ml), before extensive washing. Exosomes secreted for 5 min were pelleted by 100 000 g centrifugation (100 000 g pellet) and analysed by Western blot using anti-GFP and anti-flotillin-1 antibodies. (TCL: Total cell lysates).

B. Cortical neurons (15 DIV) were incubated with GFP-TTC, extensively washed and depolarised by incubation with fresh medium containing 25 mM KCl. After 2 h, culture supernatants were harvested and vesicles pelleted at 100 000 g (Inp). Vesicles were further separated on a sucrose density gradient. 1 ml fractions were collected and analysed by Western blot using anti-GFP and anti-flotillin-1 antibodies. Sucrose (g/ml)

1.28

F

  igure 2: E xosomal secretion is regulated by calcium. A .,B., C .: increase of exosomal release by ionomycin A . Cortical neurons (15 DIV) were incubated for 5 min in fresh medium (Ctrl,) or in fresh medium containing 2 μM ionomycin. Exosomes released during these 5 min incubations were pelleted at 100 000 g and analysed by Western-blot using the indicated antibodies (Crtl: control medium; Iono: ionomycin; TCL: Total cell lysates) B. L1, Flotillin-1 and Alix immuno-reactivities as shown in A were quantified by densitometry (Wilcoxon test, * : 0.01<p<0.05, ** 0.001<p<0.01).

F

  . L1, flotillin-1 and Alix immunoreactivities as shown in E were quantified using densitometry. (Wilcoxon test, *: 0.01<p<0.05, **: 0.001<p<0.001 F igure 3. C lusters of exosomes are released by cortical neurons in culture. A. Electron microscopy of cortical neurons (8 DIV) in culture shows extracellular clusters of vesicles having the size and shape of MVB intraluminal vesicles, which are loosely associated with the plasma membrane. B. The same kind of figures can be seen on soma and dendrites of cortical neurons at 15 DIV, washed and incubated 1 min in fresh medium containing 2 mM ionomycin before fixation. C : Figures of exocytosis, which could represent fusion of MVBs with the plasma membrane. Bar: 200 nm for A,B,C F igure 4. G F P-T T C is secreted in association with neuronal exosomes.

C.

  Increased secretion of GFP-TTC bound exosomes induced by ionomycin: 15 DIV neurons were incubated 1h at 37°C with GFP-TTC before extensive washing. Neurons were incubated with fresh medium containing 2 M ionomycin during the 5 min time of harvest. Exosomes were pelleted by 100 000 g centrifugation and analysed by Western blot using anti-GFP and anti-flotillin-1 antibodies. (TCL: Total cell lysates). Right hand panel: Flotillin and GFP-TTC immunoreactivities were estimated using densitometry. (Wilcoxon test, *: 0.01<p<0.05) D. Cortical neurons (15 DIV) were pre-incubated with GFP-TTC, washed and processed for cryosections. GFP was detected using an anti-GFP and Protein A coupled to immunogold. (bars: 200 nm). E. Cortical neurons (15 DIV) pre-incubated with GFP-TTC as in A and B were fixed and labelled with GFP antibodies and Protein A coupled to gold beads before embedding. Sections were prepared and examined by EM. Arrows show GFP labelling on exosomes in clusters close to the plasma membrane. (bars: 200 nm). F igure 5. E xosomal release is regulated by glutamatergic synaptic activity. A . Cortical neurons (15 DIV) were washed and incubated 10 min in fresh medium (Crtl) or the same medium containing 40 μM bicucullin, in absence (0) or in presence of 1 μM MK801 or of 100 μM CNQX. Thereafter, media were collected and exosomes pelleted at 100 000 g (100 000g pellet) and analysed by Western blot using the antibodies indicated. TCL: Total cell Lysate. B. L1, Alix and flotillin immunoreactivities as shown in A were quantified (Anova test, * : 0.01<p<0.05, ** 0.001<p<0.01).C . Cortical neurons (15 DIV) were incubated in K5 medium containing 40 μM picrotoxin. The incubation media were harvested after 10, 30 and 90 min, exosomes pelleted at 100 000 g and analysed by Western blot using the indicated antibodies.

  Figure 1 Click here to download Figure: Fig1.pdf

  Figure 2 Click here to download Figure: Fig2.pdf

Figure 3

 3 Figure 3

Figure 3

 3 Figure 3 Click here to download Figure: Fig3.pdf

  Figure 4 Click here to download Figure: Fig4 [Converti].pdf

Figure 5

 5 Figure 5 Click here to download Figure: Fig5.pdf

A cknowledgements: This work was supported in part by INSERM, the Université Joseph Fourier, and grants from the Association Française contre les Myopathies, the Association pour la Recherche contre le Cancer and the Association France Alzheimer. G.L. was supported by a fellowship from the Fondation pour la Recherche Médicale. A. B. was supported by the Association France Alzheimer We thank K. Sadoul and A. Depaulis for critical reading of the manuscript, C. Chatellard Causse and T. Grömer for numerous suggestions throughout this work.