Najah Ben Said

Takoua Abdellatif

Saddek Bensalem

Marius Bozga

A Model-Based Approach to Secure Multiparty Distributed Systems

Within distributed systems with completely distributed interactions between parties with mutual distrust, it is hard to control the (illicit) flowing of private information to unintended parties. Unlike existing methods dealing with verification of low-level cryptographic protocols, we propose a novel model-based approach based on model transformations to build a secure-by-construction multiparty distributed system. First, starting from a component-based model of the system, the designer annotates different parts of it in order to define the security policy. Then, the security is checked and when valid, a secure distributed model, consistent with the desired security policy, is automatically generated. To illustrate the approach, we present a framework that implements our method and use it to secure an online social network application.

Introduction

Model-based development aims at both reducing development costs and increasing the integrity of system implementations by using explicit models employed in clearly defined transformation steps leading to correct-by-construction implementation artifacts. This approach is beneficial, as one can first ensure system requirements by dealing with a high-level formally specified model that abstracts implementation details and then derive a correct implementation through a series of transformations that terminates when an actual executable code is obtained.

Nonetheless, ensuring end-to-end security requirements in distributed systems remains a difficult and error-prone task. In many situations, security reduces to access control to prevent sensitive information from being read or modified by unauthorized users. However, access control is insufficient to regulate the propagation of information once released for processing by a program especially with non-trivial interactions and computations. Thus access control offers no guarantees about whether an information is subsequently protected and deciding how to set access control permissions in complex systems is a difficult problem in itself. Equally, using cryptographic primitives that provides strong confidentiality and integrity guarantees, is also less helpful to ensure that the system obeys an overall security policy.

Information flow control is a much robust alternative which tracks information propagation in the entire system and prevent secret or confidential information from being publicly released. Information flow control relies on annotating system data and/or actions with specific levels of security and use specific methods for checking non-interference, that is, absence of leakage, between different security levels. Nonetheless, providing annotations and establishing their correctness is equally difficult especially for distributed implementations, where only code is available and no higher-level abstractions.

In this paper we introduce a model-based development approach for dealing with information flow control in distributed systems. Our contribution can be summarized as follows. First, we provide a high-level component-based model and associated security annotations to allow system designers to configure the system security in an intuitive way. They do not need to be experts in security or cryptographic protocols. Second, we provide a security checker that applies information flow techniques and verifies formally the correctness of the provided configuration. Third, a distributed model is automatically generated and respects the designer configured security policy. The mapping between the high-level policy and the distributed model is formally proven.

In the paper, we use the secureBIP framework [START_REF] Ben Said | Model-driven information flow security for component-based systems[END_REF] as underlying componentbased modeling framework. secureBIP is an extension of the BIP framework [START_REF] Basu | Modeling heterogeneous real-time systems in BIP[END_REF] with information flow security. Given security annotations for data and interactions, secureBIP captures two types of non-interference, respectively event and data non-interference. For events (that is, occurrences of interactions), noninterference states that the observation of public events does not reveal any information about the occurrence of secret events. For data, it states that there is no leakage of secret data into public ones.

We provide model transformations allowing to transform high-level secure-BIP models into a distributed models while preserving event and data noninterference. In this way, information flow security needs to be verified once, for the high-level model, and then it holds by construction on the distributed model and later on the final implementation. The proposed transformation extends previous work [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] on distributed implementation of BIP components models, which essentially addressed functional and performance aspects, while being totally agnostic about security-related issues.

The paper is structured as follows. Section 2 presents a running example to be used along the paper. Section 3 recalls the main concepts of the secureBIP framework, associated non-interference definitions and security conditions. Next, section 4 contains the new automated distribution approach to derive secure distributed models. Finally, section 5 discusses related work and section 6 concludes and presents some perspectives for future research. Proofs of technical results are given in a technical report 3 .

Throughout the paper, we consider a simplified social network application, called Whens-App, and illustrated in Figure 1. The application is intended for organizing virtual events where participants can meet and exchange data. As social network application, Whens-App entails several of security requirements. In this paper we focus on requirements related to information flow security: assuming that components are trustful and the network is unsecure, (1) the interception and observation of exchanged data messages must not reveal any information about event organization and (2) confidentiality of classified data is always preserved and kept secret inter-and intra-components. We will show that both requirements are ensured by using security annotations for tracking events and data in the system. Then, we show how the the annotated model can be automatically and systematically transformed towards a distributed implementation while preserving the security properties.

Secure Component Model

Systems are constructed from atomic components, that is, finite state automata or 1-safe Petri nets, extended with data and ports. Communication between components is achieved using multi-party interactions with data transfer.

Definition 1 (atomic component

). An atomic component B is a tuple (L, X, P , T ) where L is a set of locations, X is a set of variables, P is a set of ports and T ⊆ L × P × L is a set of port labelled transitions. For every port p ∈ P , we denote by X p the subset of variables exported and available for interaction through p. For every transition τ ∈ T , we denote by g τ its guard, that is, a Boolean expression defined on X and by f τ its update function, that is, a parallel assignment {x := e x τ } x∈X to variables of X.

Let D be an universal data domain, fixed. A valuation of a set of variables Y is a function y : Y → D. We denote by Y the set of all valuations defined on Y . The semantics of an atomic component B is defined as the labelled transition system sem(B)

= (Q B , Σ B , -→ B
) where the set of states Q B = L × X, the set of labels Σ B = P × X and transitions -→ B are defined by the rule:

Atom τ = p -→ ∈ T x p ∈ Xp gτ (x) x = fτ (x[Xp ← x p ]) ( , x) p(x p ) ----→ B ( , x )
That is, ( , x ) is a successor of ( , x) labelled by p(x p ) iff (1) τ = p -→ is a transition of T , (2) the guard g τ holds on the current state valuation x, (3) x p is a valuation of exported variables X p and (4) x = f τ (x[X p ← x p ]) that is, the next-state valuation x is obtained by applying f τ on x previously modified according to x p . Whenever a p-labelled successor exists in a state, we say that p is enabled in that state. Composite components are obtained by composing atomic components B i = (L i , X i , P i , T i ) i=1,n through multiparty interactions. We consider that atomic components have pairwise disjoint sets of locations, ports, and variables i.e., for any two i = j from {1..n}, we have L i ∩ L j = ∅, P i ∩ P j = ∅, and X i ∩ X j = ∅.

A multiparty interaction a is a triple (P a , G a , F a ), where P a ⊆ n i=1 P i is a set of ports, G a is a guard, and F a is a data transfer function. By definition, P a uses at most one port of every component, that is, |P i ∩P a | ≤ 1 for all i ∈ {1..n}. Therefore, we simply denote P a = {p i } i∈I , where I ⊆ {1..n} contains the indices of the components involved in a and for all i ∈ I, p i ∈ P i . G a and F a are both defined on the variables exported by the ports in P a (i.e., p∈Pa X p ).

Definition 2 (composite component). A composite component C = γ(B 1 , . . . , B n ) consists of the composition of B 1 , . . . , B n by a set of interactions γ. Given sem(B i ) = (Q i , Σ i , --→ Bi ) i=1,n , the semantics of C is defined as the labelled transition system sem(C) = (Q C , Σ C , -→ C ) where the set of states Q C = ⊗ n i=1 Q i , the set of labels Σ C = γ and transitions -→ C
are defined by the rule:

Comp a = ({pi}i∈I , Ga, Fa) ∈ γ Ga({xp i }i∈I ) {x p i }i∈I = Fa({xp i }i∈I ) ∀i ∈ I. ( i, xi) p i (x p i ) -----→ B i ( i , x i )∀i ∈ I. ( i, xi) = ( i , x i ) (( 1, x1), . . . , ( n, xn)) a -→ C (( 1 , x 1 ), . . . , ( n , x n ))
For each i ∈ I, x pi above denotes the valuation x i restricted to variables of X pi . The rule expresses that C can execute an interaction a ∈ γ enabled in state (( 1 , x 1 ), . . . , ( n , x n )), iff (1) for each p i ∈ P a , the corresponding atomic component B i can execute a transition labelled by p i , and ( 2) the guard G a of the interaction holds on the current valuation x pi of exported variables on ports in a. Execution of a triggers first the data transfer function F a which modifies exported variables X pi . The new values obtained, encoded in the valuation x pi , are then used by the components' transitions. The states of components that do not participate in the interaction remain unchanged. We call a trace any finite sequence of interactions w = a 1 a 2 • • • ∈ γ * executable from a given initial state q 0 . The set of all traces w from state q 0 is denoted by traces(C, q 0 ). Figure 3 presents a simplified composite component for an instance of the Whens-App application with two event creators and three event receivers. Interactions are represented using connecting lines between the interacting ports. Binary interactions (push store) and (report get) include data transfers between components, that is, assignments of data across interacting components.

Information Flow Security

We consider transitive information flow policies expressed on system variables and we focus on the non-interference properties. We restrict ourselves to confidentiality and we ensure that no illegal flow of information exists between variables having incompatible security levels.

Formally, we represent security domains as finite lattices S, where S denotes the security levels and the flows to relation. For example, a security domain with two levels High (H), Low (L) and where information is allowed to flow from Low to High is {L, H}, {(L, L), (L, H), (H, H)} .

Let C = γ(B 1 , . . . B n ) be a composite component, fixed. Let X (resp. P ) be the set of all variables (resp. ports) defined in all atomic components (B i ) i=1,n . Let S, be a security domain, fixed.

Definition 3 (security assignment σ). A security assignment for component C is a mapping σ : X ∪ P ∪ γ → S that associates security levels to variables, ports and interactions such that, moreover, the levels of ports and interactions match, that is, for all a ∈ γ and for all p ∈ P it holds σ(p) = σ(a).

The security levels for ports and variables track the flow of information along computation steps within atomic components. The security levels for interactions track the flow of information along inter-component communication. We consider that deducing event-related information represent a risk that should be handled while controlling the system's information flow in addition to data flows. Endto-end security is defined according to transitive non-interference.

Let σ be a security assignment for C, fixed. For a security level s ∈ S, we define γ ↓ σ s the restriction of γ to interactions with security level at most s that is formally, γ ↓ σ s = {a ∈ γ | σ(a) s}. For a security level s ∈ S, we define w| σ s the projection of a trace w ∈ γ * to interactions with security level lower or equal to s. Formally, the projection is recursively defined on traces as

| σ s = , (aw)| σ s = a(w| σ s ) if σ(a) s and (aw)| σ s = w| σ s if σ(a) s. The projection operator | σ s is naturally lifted to sets of traces W by taking W | σ s = {w| σ s | w ∈ W }.
For a security level s ∈ S, we define the equivalence ≈ σ s on states of C. Two states q 1 , q 2 are equivalent, denoted by q 1 ≈ σ s q 2 iff (1) they coincide on variables having security levels at most s and (2) they coincide on control states having outgoing transitions labeled with ports with security level at most s. We are now ready to define the two types of non-interference respectively event non-interference (ENI) and data non-interference (DNI).

Definition 4 (event/data non-interference). The assignment σ ensures event (ENI) and data non-interference (DNI) of γ(B 1 , . . . , B n ) at security level s iff,

(EN I) ∀q0 ∈ Q 0 C : traces(γ(B1, . . . , Bn), q0)| σ s = traces((γ ↓ σ s )(B1, . . . , Bn), q0) (DN I) ∀q1, q2 ∈ Q 0 C , ∀w1 ∈ traces(C, q1), w2 ∈ traces(C, q2), ∀q 1 , q 2 ∈ QC : q1 ≈ σ s q2 ∧ w1| σ s = w2| σ s ∧ q1 w 1 --→ C q 1 ∧ q2 w 2 --→ C q 2 ⇒ q 1 ≈ σ s q 2
Moreover, σ is said secure for a component γ(B 1 , . . . , B n ) iff it ensures both event and data non-interference, at all security levels s ∈ S.

Both variants of non-interference express some form of indistinguishability between several states and traces of the system. For instance, an attacker that can observe the system's variables and occurences of interactions at security level s 1 must not be able to distinguish neither changes on variables or occurrence of interactions having higher or incomparable security level s 2 .

The running example presented in Figures 2 and3 is annotated with two levels of security Low (in black) and High (in red). With this assignement, the exchange of information during the event and some related data are High whereas the event initiation is Low.

Noninterference Checking

In our previous work [START_REF] Ben Said | Model-driven information flow security for component-based systems[END_REF], we established sufficient syntactic conditions that reduce the verification of non-interference to local constrains checking on transitions (intra-component) and interactions (inter-components). We recall these conditions hereafter as they are going to be used later in section 4 for establishing security correctness of the decentralized component model. Indeed, these conditions offer a syntactic way to ensure both event and data non-interfrence and therefore to obtain preservation proofs for along decentralization.

Definition 5 (security conditions). Let C = γ(B 1 , . . . , B n ) be a composite component and let σ be a security assignment. We say that C satisfies the security conditions for security assignment σ iff:

(i) the security assignment of ports, in every atomic component B i is locally consistent, that is, for every pair of causal transitions:

∀τ 1 , τ 2 ∈ T i : τ 1 = 1 p1 -→ 2 , τ 2 = 2 p2 -→ 3 ⇒ ( 1 = 2 ⇒ σ(p 1 ) σ(p 2 )
) and for every pair of conflicting transitions:

∀τ 1 , τ 2 ∈ T i : τ 1 = 1 p1 -→ 2 , τ 2 = 1 p2 -→ 3 ⇒ σ(p 1 ) = σ(p 2 )
(ii) all assignments x := e occurring in transitions within atomic components and interactions are sequential consistent, in the classical sense: ∀y ∈ use(e) : σ(y) σ(x) (iii) variables are consistently used and assigned in transitions and interactions:

∀τ ∈ ∪ n i=1 T i , ∀x, y ∈ X : x ∈ def (f τ ), y ∈ use(g τ ) ⇒ σ(y) σ(p τ ) σ(x) ∀a ∈ γ, ∀x, y ∈ X : x ∈ def (F a ), y ∈ use(G a ) ⇒ σ(y) σ(a) σ(x) (iv) all atomic components B i are port deterministic: ∀τ 1 , τ 2 ∈ T i : τ 1 = 1 p -→ 2 , τ 2 = 1 p -→ 3 ⇒ (g τ1 ∧ g τ2 ) is unsatisfiable
The first family of conditions (i) is similar to Accorsi's conditions [START_REF] Accorsi | Automatic information flow analysis of business process models[END_REF] for excluding causal and conflicting places for Petri net transitions having different security levels. Similar conditions have been considered in [START_REF] Focardi | Bridging language-based and process calculi security[END_REF][START_REF] Frau | Petri net security checker: Structural noninterference at work[END_REF] and lead to more specific definitions of non-interferences and bisimulations on annotated Petri nets. The second condition (ii) represents the classical condition needed to avoid information leakage in sequential assignments. The third condition (iii) tackles covert channels issues. Indeed, (iii) enforces the security levels of the data flows which have to be consistent with security levels of the ports or interactions (e.g., no low level data has to be updated on a high level port or interaction). Such that, observations of public data would not reveal any secret information. Finally, condition (iv) enforces deterministic behavior on atomic components.

The following result, proven in [START_REF] Ben Said | Model-driven information flow security for component-based systems[END_REF], states that the security conditions are sufficient to ensure both event and data non-interference.

Theorem 1. Whenever the security conditions hold, the security assignment σ is secure for the composite component C.

For example, the security conditions hold for the security assignment considered for the running example in Figures 2 and3. Notice that local consistency is ensured in both atomic components: the security level can only increase from Low to High along causal transitions and no choices exist between Low and High transitions. Equally, notice that no High data is assigned on Low interactions.

Automatic Decentralization Method

In this section, we describe the decentralization method for our component-based model and provide formal proofs for information-flow security preservation. The decentralization method extends the method for decentralization of BIP models [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. The existing method transforms BIP models with multiparty interactions (and priorities) into functionally equivalent BIP models using only send/receive (S/R) interactions. S/R interactions are binary, point-to-point, directed interactions from one sender component (port), to one receiver component (port) implementing asynchronous message passing.

From a functional viewpoint, the main challenge when transforming a BIP model into a decentralized S/R BIP model is to enable parallelism for execution of atomic components and concurrently enabled interactions. That is, in a distributed setting, every atomic component executes independently and communication is restricted to asynchronous message passing. The existing method for decentralizing BIP relies on structuring the distributed components according to a hierarchical architecture with two4 layers:

the atomic components layer includes transformed atomic components. Whenever an atomic component needs to interact, it publish an offer, that is the list of its enabled ports, then wait for a notification indicating which interaction has been chosen, and then resume its execution. the interaction protocols (IP) layer deals with distributed execution of interactions by implementing specific protocols. Every IP component handles a subset of interactions, that is, check them for enabledness and schedule them for execution accordingly. The interface between this layer and the component layer provides ports for receiving offers and notifying the ports selected for execution.

The existing methods in [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] have been designed without taking into account security concerns. In the following, we will show that they can be extended such that to preserve information flow security. Roughly speaking, this is achieved by using a slightly different transformation for atomic components as well as by imposing few additional restrictions on the structure of the interaction protocol layer. We show that the security assignment from the original model is naturally lifted to the decentralized model and consequently, non-interference is preserved along the transformation.

Let

C = γ(B 1 , • • • B n
) be a composite component and σ be a secure assignment for C which satisfies the security conditions for non-interference.

Atomic Components Layer

The transformation of atomic components consists in breaking atomicity of transitions. Precisely, each transition is split into two consecutive steps: (1) an offer that publishes the current state of the component, and (2) a notification that triggers an update function and resume local computation. The intuition behind this transformation is that the offer transition correspond to sending information about component's intention to interact to some IP component and the notification transition corresponds to receiving the answer from an IP component, once an interaction has been completed. Update functions can be then executed concurrently and independently by components upon notification reception.

In constrast to the transformation proposed in [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF], several changes are needed to protect information flow. Distinct offer ports o s and interaction counters n s are introduced for every security level. Thus, offers and corresponding notifications have the same security level, and moreover, no information about execution of interactions is revealed through the observation of interaction counters. Definition 6 (transformed atomic component). Let B = (L, X, P, T ) be an atomic component within C. The corresponding transformed S/R component is B SR = (L SR , X SR , P SR , T SR ):

-L SR = L ∪ L ⊥ , where L ⊥ = {⊥ | ∈ L} -X SR = X ∪ {e p } p∈P ∪ {n s |s ∈ S}
where e p is a fresh boolean variable indicating whether port p is enabled, and n s is a fresh integer variable called interaction counter for security level s.

-P SR = P ∪ {o s | s ∈ S}. The offer ports o s export the variables X os = {n s } {{e p } ∪ X p | σ(p)
= s} that is the interaction counter n s , the newly added variable e p and the variables X p associated to ports p with security level s. For other ports, the set of variables exported remains unchanged. -For each state ∈ L, let S be the set of security levels assigned to ports labeling all outgoing transitions of . For each security level s ∈ S , we include the offer transition τ os = (⊥ os -→ ) ∈ T SR , where the guard g os is true and f os resets variables e p to false, for all ports p with security level s.

-For each transition τ = p -→ ∈ T we include a notification transition τ p = ( p -→ ⊥ ) where the guard g p is true and the function f p applies the original update function f τ on X, sets e r variables to g τr for every port r ∈ P such that τ r = r -→ ∈ T and increments n s .

We introduce now the extended security assignment for transformed atomic components B SR . Intuitively, all existing variables and ports from B keep their original security level, whereas the newly introduced ones are assigned such that to preserve the security conditions of the trasformed component.

Definition 7 (security assignement σ SR for B SR ). The security assignment σ SR is the extension of the original security assignment σ to variables X SR and ports P SR from B SR as follows: Actually, security conditions are preserved along the proposed transformation of atomic components with respect to extended security assignement. The following lemma formalizes this result. Lemma 1. B SR satisfies the security conditions with security assignment σ SR .

σ SR (x) =      σ(p) if x = ep and p ∈ P s if x = ns and s ∈ S σ(x) otherwise, for x ∈ X SR σ SR (p) = s if p =
Proof. easy check, security conditions hold by definition of B SR and σ SR .

Interaction Protocol Layer

This layer consists of a set of components, each in charge of execution of a subset of interactions from the original component model. Every such IP component is a controller that, iteratively, receives offers from the transformed atomic components, computes enabled interactions and schedule them for execution.

In this paper, we consider IP components handling a conflict-free partitioning of interactions, as in [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF]. Two interactions a 1 and a 2 are in conflict iff either (i) they share a common port p (i.e p ∈ a 1 ∩ a 2 ) or (ii) there exist two conflicting transitions at a local state of a component B i that are labeled with ports p 1 and p 2 , where p 1 ∈ a 1 and p 2 ∈ a 2 . Conflict-free partitioning allows IP components to run fully independently of each other, that is, local decisions taken on every IP component about executing one of its interactions do not interfere with others.

Moreover, in order to ensure information flow security, we impose an additional restriction on partitioning, that is, the subset of interactions handled within every IP component must have the same security level. Intuitively, this restriction allows us to enforce by construction the security conditions for all IP components and later, for the system composition.

Bearing this in mind, let us observe that if the original system satisfies the security conditions then the partitioning of interactions according to their security level is conflict-free. That is, no conflict exists between interactions with different security levels -this simply follows from the condition (i) on the labeling of conflicting transitions. Therefore, for the sake of simplicity of presentation, we restrict hereafter our construction to the partitioning according to security levels. For every security level s we consider one IP component IP s handling the subset of interactions γ s = {a ∈ γ | σ(a) = s} with security level s.

Definition 8 (IP s component for γ s ). Interaction protocol component IP s handling interactions γ s is defined according to [START_REF] Bonakdarpour | Automated conflict-free distributed implementation of component-based models[END_REF], Definition 7.

The extended security assignement σ SR for IP s variables and ports is defined as follows. All ports are annotated with security level s. Regarding variables, σ SR maintains the same security level for all variables having their level greater than s in the original model and upgrades the others to s. That is, all variables within the IP s component will have security level at least s. This change is mandatory to ensure consistent transfer of data in offers (resp. notifications) between atomic components and IP s . Definition 9 (security assignment σ SR for IP s ). The security assignment σ SR is built from the original security assignment σ. For variables X IP and ports P IP of the IP s component that handles γ s , we define

σ SR (x) = σ(x) if x ∈ Xp and s σ(x) s otherwise σ SR (p) = s if p ∈ P IP
The above definition enforces the security conditions for IP s .

Lemma 2. IP s satisfies the security conditions with security assignment σ SR .

Proof. Trivial check for conditions (i, iv). The condition (ii) on sequential consistency is also valid, even if some (replicated) variables within IP s are upgraded to level s. On one hand, these variables, if any, were exclusively used (e.g., within guards, or left-hand sides of assignments) and never defined in interactions from γ s . On the other hand, all defined variables have the security level greater than s. Same reasoning applies for the condition (iii) with respect to ports.

System Composition

As a final step, the decentralized model The security assignment σ SR is naturally lifted from offer/notification ports to the interactions of γ SR . Intuitively, every S/R interaction involving component IP s has security level s. The construction is illustrated for the running example in Figure 5. We omitted the representation of ports and depict only the interactions and their associated data flow. In particular, consider the x variable of Event Receiver which is upgraded to H when sent to IP H and not sent back on the notification of the push interaction.

C
The following theorem states our main result, that is, the constructed twolayer S/R model satisfies the security conditions by construction. Proof. From lemma 1 and 2 all security conditions related to transformed components and IP components are satisfied. The only remaining condition (iii) concerns the assignement of data along S/R interactions. As all the variables in IP s have been eventually upgraded to level s, the assignment within offer interactions is consistent. Similar for notifications at level s, their assignement is restricted by construction to variables having security level at least s.

Related Work

Model-based security aims at simplifying security configuration and coding. The work in [START_REF] Basin | Model driven security: From UML models to access control infrastructures[END_REF] considers modeling security policies in UML and targets automating security code generation for business applications using JEE and .net. The work of [START_REF] Chollet | Security specification at process level[END_REF] uses a model-based approach to simplify secure code deployment on heterogeneous platforms. Compared to these, our work is not restricted to point-to-point access control and deals with information flow security. The work on designing web services from [START_REF] Accorsi | Static information flow analysis of workflow models[END_REF] relies on Petri-nets for modeling composed services and annotations for the flow of interactions. Our component model is more general and deals with both data and event-non-interference.

Information flow control for programming languages dates back to Denning who originally proposed a language for static information flow checking [START_REF] Denning | Certification of programs for secure information flow[END_REF]. Since then, information-flow control based on type systems and associated compilation tools has widely developed [START_REF] Goguen | Security policies and security models[END_REF][START_REF] Heintze | The slam calculus: Programming with secrecy and integrity[END_REF][START_REF] Volpano | A sound type system for secure flow analysis[END_REF]. Recently, it extends to provably-secure languages including cryptographic functions [START_REF] Laud | Semantics and program analysis of computationally secure information flow[END_REF][START_REF] Adão | Cryptographically sound implementations for communicating processes[END_REF][START_REF] Courant | Computationally sound typing for noninterference: The case of deterministic encryption[END_REF][START_REF] Laud | On the computational soundness of cryptographically masked flows[END_REF][START_REF] Fournet | Cryptographically sound implementations for typed information-flow security[END_REF]. With few exceptions, all these approaches are restricted to sequential imperative languages and ignore distribution/communication aspects. Among the exceptions, JifSplit [START_REF] Zdancewic | Secure program partitioning[END_REF] takes as input a security-annotated program, and splits it into threads by assuming that the communication through the network is secure. Furthermore, in [START_REF] Fournet | A security-preserving compiler for distributed programs: From information-flow policies to cryptographic mechanisms[END_REF] the communication's security is enforced by adding cryptographic mechanisms. The drawback of these is that the security aspect guides the system distribution. In practice, a separation of concerns is required and the system architecture must be independent of security constraints. Our approach is different since our starting point is a component-based model and the security constraints are expressed with annotations at the architecture level.

Operating systems like Flume [START_REF] Krohn | Information flow control for standard OS abstractions[END_REF], HiStar [START_REF] Zeldovich | Making information flow explicit in HiStar[END_REF] and Asbestos [START_REF] Vandebogart | Labels and event processes in the Asbestos operating system[END_REF] ensure information flow control between processes by associating security labels to processes and messages. DStar [START_REF] Zeldovich | Securing distributed systems with information flow control[END_REF] extends HiStar to distributed applications. These approaches may appear attractive since transparent to the developer. Nevertheless, the granularity of processes may be too coarse to establish end-to-end security for distributed applications with complex interactions.

Component-based design is appealing for verification of security since the system structure and communications are explicitly represented. However, existing work focus merely on point-yo-point access control. The work of [START_REF] Parrend | Security benchmarks of OSGi platforms: toward hardened OSGi[END_REF] considers dependencies between service components but not advanced properties like implicit information flow. In [START_REF] Kuz | Camkes: A component model for secure microkernel-based embedded systems[END_REF], authors provide APIs to configure the security of component connectors. The work in [START_REF] Abdellatif | Automating information flow control in component-based distributed systems[END_REF] deals with non-interference on component-based models using annotation propagation inside component code. In our work, we achieve complete separation between the abstract highlevel component model on which non-interference is verified, and the low-level platform-dependent model where security is enforced by construction.

Conclusion and Future Work

We introduced a tool-supported approach to automatically secure information flow in distributed systems. Starting from an abstract component-based model with multiparty interactions, we verify security policy preservation, that is, noninterference property at both event and data levels. Then, we generate a distributed model where multiparty interactions are replaced with protocols based on asynchronous message passing. The distributed model is proved "secure-byconstruction". This work is being extended towards code generation and deployment on distributed platforms. More specifically, we envisage to use web services as a target for the S/R distributed model and to rely on web services security standards to ensure the required protection of the information flow, following idea from [START_REF] Ben Said | A robust framework for securing composed web services[END_REF]. On longer term, we plan to to extend both the security model and the associated transformations for relaxed versions of non-interference i.e, allowing runtime re-labelling, declassification, intransitive.

Fig. 1 .

 1 Fig. 1. Overview of the Whens-App application

Fig. 2 .

 2 Fig. 2. Example of atomic components

Figure 2

 2 Figure 2 presents the atomic components used in the Whens-App application model. The Event Creator (left) coordinates an event lifetime (invite, open and cancel transitions), get raw information from participants (store) and delivers some information digests (report). The Event Receiver (right) enters an event (receive, enter), share information (push) and receive event digests (get). [Colors are explained later]Composite components are obtained by composing atomic components B i = (L i , X i , P i , T i ) i=1,n through multiparty interactions. We consider that atomic components have pairwise disjoint sets of locations, ports, and variables i.e., for any two i = j from {1..n}, we have L i ∩ L j = ∅, P i ∩ P j = ∅, and X i ∩ X j = ∅.A multiparty interaction a is a triple (P a , G a , F a ), where P a ⊆

Fig. 3 .

 3 Fig. 3. Example of composite component

eFig. 4 .

 4 Fig. 4. Transformation of atomic components illustrated on the Event Receiver

Fig. 5 .

 5 Fig. 5. Decentralized model for the WhensApp example

Theorem 2 .

 2 The decentralized component C SR = γ SR (B SR 1 , ..., B SR n , (IP s ) s∈S ) satisfies security conditions for the security assignment σ SR .

  SR is obtained as the composition γ SR (B SR 1 , ..., B SR n , (IP s ) s∈S ) involving the transformed components B SR i and components IP s . The set γ SR contains S/R interactions and is defined as follows: for every component B SR i participating in interactions having security level s, include in γ SR the offer interaction (B SR i .o s , IP s .o i ) associated with the transfer of data from the component port o s to the IP component port o i .for every port p in component B SR i with security level s, include in γ SR the notification interaction (IP s .p, B i .p) associated with the transfer of the subset of X p variables having security level at least s from the IP component port p to the component port p. Actually, these are the only variables that could have been modified by an interaction having level s.

	ER SR 1 , ER SR 2 , ER SR 3
	o L	enter	get	o H
	receive		push
	IP L
	invite ij receive i receive j	push i store ij
	open ij enter i enter j		get i report ij
	invite		store
	o L	open	report	o H
		EC SR 12 , EC SR 23

no. TR-2014-6 on http://www-verimag.imag.fr/Rapports-Techniques,28.html

In general, a third conflict resolution layer is used, however, it has a confined impact on information flow and is ommited here for the sake of simplicity of the presentation

The research leading to these results has received funding from the European Community's Seventh Framework Programme [FP7/2007-2013] under grant agreement ICT-318772 (D-MILS).


L B Younis

A A Mohamad
email: mohamad@ucalgary.ca

A K Mojtabi

Double diffusion natural convection in open lid enclosure filled with binary fluids

Keywords: Natural convection, Double diffusion, Free surface

Double diffusion natural convection in an enclosure filled with a liquid and subjected to differential heating and differential species concentration is investigated. Four models were developed to address the hydraulic effect of the upper lid on the rate of heat and mass transfer and on the flow structures. It is found that free surface yields higher rate of heat and mass transfer. Also, there is noticeable difference between the results of twoand three-dimensional results. Hence, the effect of upper lid condition cannot be underestimated. The effect of boundary condition on the rate of heat transfer is more profound for natural convection without double diffusion effects.

Introduction

Double diffusive convection has been subject of an intensive research due to its importance in various engineering and geophysical problems. For instance, pollution desperation in lakes and reveres, solute intrusion in sediments in coastal environments, nuclear waste disposals, contaminant transport in ground water, chemical processes and species transport through biological membranes are a few examples to mention. In such process the thermal and concentration buoyancy forces either aid or oppose each other, depending on the type of alloy and process of heating.

The subject of natural convection for single fluid flow and double diffusion has been studied extensively [START_REF] Batchelor | Heat transfer by free convection across a closed cavity between vertical boundaries at different temperatures[END_REF][START_REF] Eckert | Natural convection in an air layer enclosed between two vertical plates with different temperatures[END_REF][START_REF] Elder | Laminar free convection in a vertical slot[END_REF][START_REF] Emery | Heat transfer across vertical layers[END_REF][START_REF] Elder | Numerical experiments with free convection in a vertical slot[END_REF][START_REF] Gill | The boundary-layer regime for convection in a rectangular cavity[END_REF][START_REF] Newell | Heat transfer by laminar natural convection within rectangular enclosures[END_REF][START_REF] Ozoe | Natural convection in an inclined rectangular channel at various aspect ratios and angles-experimental measurements[END_REF][START_REF] Thangam | Transition from shear to side-ways diffusive instability in a vertical slot[END_REF][START_REF] Tanny | The dynamics and structure of double diffusive layers in side-wall heating experiments[END_REF][START_REF] Jeevarage | Experimental study of double diffusive instability in sidewall heating[END_REF][START_REF] Bennacer | Cooperating thermosolutal convection in enclosures-I. Scale analysis and mass transfer[END_REF][START_REF] Bennacer | Cooperating thermosolutal convection in enclosures-II. Heat transfer and flow structure[END_REF][START_REF] Shyy | Double-diffusive flow in enclosures[END_REF][START_REF] Ghorayeb | Double diffusive convection in a vertical rectangular cavity[END_REF][START_REF] Leong | On a physically-realizable benchmark problem in internal natural convection[END_REF][START_REF] Leong | Experimental Nusselt numbers for a cubical-cavity benchmark problem in natural convection[END_REF][START_REF] Bergeon | Double diffusive instability in an inclined cavity[END_REF][START_REF] Sezai | Double diffusive convection in a cubic enclosure with opposing temperature and concentration gradient[END_REF]. Yet, most work done considers flow inside closed enclosures. In some applications, such as pollution dispersion in lakes, chemical deposition, melting and solidification process, it is more appropriate to model the process of heat and mass transfer in open lid cavities, which is the subject of the present work. The governing equations are elliptical in nature and the boundary conditions effects are very important on the solution of the domain of integrations. Enclosed enclosure imposed shear stress at the boundary, which has a dissipative effect and restricts the fluid particle motion. While, free surface (shear stresses equal to zero) increases the freedom of motion at the boundary, which may change the dynamics of the flow due to the elliptical nature of the problem. Three-and two-dimensional models are developed to investigate the flow structure, heat and mass transfer process in enclosures with free upper surface. Also, the results compared with that of a closed lid enclosure. This step is taken to critically evaluate the effect of upper boundary on the flow structure. The hypothesis is that the Navier-Stokes equation is elliptical in nature and shear at the upper boundary should have significant effect on the flow and on the rate of energy and mass transfer. Complex flow patterns may form due to difference in the rate of heat and mass transfer, competition between thermal and concentration boundary layers development and density reversal in the mixing zone. Complex flow is expected when the thermal/concentration buoyancy force opposes the concentration/thermal buoyancy force. Hence, flow bifurcation is expected and flow may become three-dimensional. Two-dimensional flow patterns may be justified for a certain range of controlling parameters in an enclo-sure imposed to thermal and concentration gradients along vertical boundaries. Double diffusive, natural convection in differentially heated enclosures with aiding thermal and concentration gradients were considered in references. Most of the mentioned works were assumed that the flow is two-dimensional. Sezai and Mohamad [START_REF] Sezai | Double diffusive convection in a cubic enclosure with opposing temperature and concentration gradient[END_REF] explored the three-dimensional flow in cubic enclosures filled with a saturated porous medium where the flow was driven by opposing buoyancy forces due to thermal and concentration gradients. Their results revealed that for certain range of controlling parameters (porous thermal Rayleigh (Ra * ), Lewis (Le) and buoyancy ratio parameters) the flow might become three-dimensional. The flow became three-dimensional for the concentration to thermal buoyancy ratio (N ) equal to -0.5, Ra * = 10 and Le > 20. Also, threedimensional flow pattern is predicted for N = -0.5, Le = 10 and Ra * > 20. The rate of mass transfer was more sensitive for flow bifurcations from 2-D to 3-D than the rate of heat transfer. When the flow becomes three-dimensional, multiple dipole vortices form in the transverse planes, similar to those created by injection of fluid into stratified medium. On the other hand, the results of Mohamad and Bennacer [START_REF] Mohamad | Natural convection in a confined saturated porous medium with horizontal temperature and vertical solutal gradients[END_REF] on doubled diffusion in an enclosure heated differentially and species gradient imposed vertically, cross gradient conditions, showed that the flow is three-dimensional in general, but the difference between results of 2-D and 3-D simulation is not that significant as far as the rate of heat and mass transfer is concerned.

The present study address the effect of upper boundary on the flow structure and on the rate of heat and mass transfer in a cubic cavity filled with binary fluid and imposed to temperature and species gradients horizontally. Three-and two-dimensional models are developed to investigate the flow structure, heat and mass transfer process in enclosures with free upper surface. Also, the results were compared with that of closed enclosure. This step is taken to critically evaluate the effect of upper boundary on the flow structure.

Complex flow patterns may form due to differences in the rate of heat and mass transfer, competition between thermal and concentration boundary layers development and density reversal in the mixing zone. Such a phenomenon is more probable when the thermal/concentration buoyancy force oppose each other and order of magnitude of the opposing forces becomes unity. Hence, flow bifurcation is expected and flow may become three-dimensional. When the flow becomes three-dimensional, multiple dipole vortices form in the transverse planes, similar to those created by injection of fluid into stratified medium. Also, the results indicate that the rates of heat and mass transfer are substantially higher for the open lid enclosure compared with results of closed lid enclosure. This may be explained due the fact that the shear at the upper boundary reduces the fluid parcels velocity, consequently reduces the advected rate of heat and mass transfers.

Problem definition and governing equations

The problem under consideration is an open lid rectangular cross section enclosure filled with a binary fluid, Fig. 1. The rectangular enclosure of sides L x , L y and L z . Different temperature and concentrations were imposed between the left (T 1 , C 1 ) and right vertical walls (T 2 , C 2 ), where the C 1 > C 2 and T 1 > T 2 . Adiabatic and impermeable boundary conditions were imposed on the remaining boundaries. Except at the upper boundary where the shear stress is assumed to be negligible, i.e., the effect of surface tension is neglected. This assumption can be justified for water-air interface and for thick layer of fluid body, i.e., volume per surface area ≫1. Also, it is assumed that the free surface is non-deformable. Further more, the rate of heat exchange between the fluid in the container and ambient through the free surface is neglected. This assumption is difficult to justify, but for stagnant air the heat transfer coefficient is order of 10 W m -2 K -1 , which translates to small value of Biot number, therefore the assumption may be justified. However, for analysis process and to isolate the effect of Biot number, the effect of heat transfer from the upper boundary is assumed to be negligible. Therefore, the upper boundary is assumed to be adiabatic. The flow is assumed to be laminar and steady. The binary fluid of Prandtl number of 10 (aqua solution) was assumed to be Newtonian and incompressible with Boussinesq approximation is valid. The Soret and Dufour effects were assumed to be negligible.

Using the following dimensionless variables:

X = x/L x , Y = y/L x , Z = z/L x , V = vL x /ν, P = pL 2 x /ρν 2 , Θ = (T -T 2 )/(T 1 -T 2 ), Φ = (C -C 2 )/(C 1 -C 2 )
, where ν is the kinematical viscosity of the fluid and v is the velocity vector. The equations governing the conservation of mass, momentum and energy in non-dimensional form can be written as:

Continuity: ∇. V = 0 (1)
Momentum:

( V . ∇) V = -∇P + ∇ 2 V + Ra Pr (Θ + N Φ) k (2)
Energy:

V .∇Θ = 1 Pr ∇ 2 Θ ( 3
)
Species conservation:

V .∇Φ = 1 Le Pr ∇ 2 Φ ( 4
)
where k is the unit vector in Z direction, Ra = (gβ T T L 3 )/να is the thermal Rayleigh number, Pr = ν/α is the Prandtl number, N is the ratio of the buoyancy forces, Ra s /Ra Le, Ra s = (gβ c CL 3 )/νD is the solutal Rayleigh number, Le = α/D is the Lewis number, α and D are the thermal and molecular diffusities, respectively. In the limit of vanishing capillary number Ca = |γ | T ≪ 1 surface deformations cannot occur so that the boundary conditions at the open top surface (Z = A z ) are

∂U ∂Z + Ma ∂Θ ∂X = 0 (5a) ∂V ∂Z + Ma ∂Θ ∂Y = 0 (5b) W = 0 (5c) ∂Θ ∂Z + Bi Θ = 0 (5d) ∂Φ ∂Z = 0 ( 5e
)
where Ma = -(∂σ/∂T ) T L/µα is the Marangoni number and Bi = hL x /k is the Biot number with h being the surface heat transfer coefficient. As mentioned before, the effect of Ma and Bi numbers are neglected.

At the rigid walls no-slip and no penetration boundary conditions are imposed for the velocities,

U = V = W = 0 on X = 0, A x (6a)
U = V = W = 0 on Y = 0, A y (6b)
U = V = W = 0 on Z = 0 (6c)
Since the side walls are of the cavity are heated at X = 0 and cooled at X = A x and all other walls are adiabatic, we impose Θ = 1 and Φ = 1 on X = 0 (7a)

Θ = 0 and Φ = 0 on X = A x (7b)
∂Θ/∂Y = 0 and ∂Φ/∂Y = 0 on Y = 0, 1

∂Θ/∂Z = 0 and ∂Φ/∂Z = 0 on Z = 0 (7d)

Method of solution

Eqs. ( 1)-( 7) are discretized using staggered, nonuniform control volumes. Third order accurate numerical scheme, QUICK scheme is used in approximating the advection terms with the flux limiter known as ULTRA-SHARP is used to eliminate the non-physical oscillations inherent in the QUICK scheme. SIMPLEC algorithm [START_REF] Van Doormaal | Enhancements of the SIMPLE method for predicting incompressible fluid flows[END_REF] is used to couple momentum and continuity equations. The momentum equations are solved by applying one iteration of the strongly implicit procedure (SIP) of [START_REF] Stone | Iterative solution of implicit approximations of multidimensional partial differential equations[END_REF]. The pressure correction equation is solved iteratively by applying the conjugate gradient (CG) method until the sum of absolute residuals has fallen by a factor of ten. The coefficient matrix resulting from the discretization of the energy equation is non-symmetric and solved iteratively by Bi-CGSTAB method. SSOR preconditioning is used for accelerating the convergence rates of both CG and Bi-CGSTAB methods with full multigrid method [START_REF] Hortmann | Finite volume multigrid prediction of laminar natural convection: bench-mark solutions[END_REF]. Generally, under relaxation factors of 0.7, 0.7, 0.7, 1.0, 0.9 and 0.9 were applied to U , V , W , P , T and C, respectively. 120 × 120 × 40 control volumes are used on the finest level with denser grid clustering near boundaries using the sine function for the grid distribution.

To ensure convergence of the numerical algorithm the following criteria is applied to all dependent variables over the solution domain

|φ m ij k -φ m-1 ij k | |φ m ij k | 10 -5 (8)
where φ represents a dependent variable U , V , W , P and T , the indexes i, j , k indicate a grid point and the index m the current iteration at the finest grid level.

The method is detailed in the work of Sazai and Mohamad [START_REF] Sezai | Double diffusive convection in a cubic enclosure with opposing temperature and concentration gradient[END_REF]. Also, the code extensively tested for double diffusion problem [START_REF] Sezai | Double diffusive convection in a cubic enclosure with opposing temperature and concentration gradient[END_REF][START_REF] Mohamad | Natural convection in a confined saturated porous medium with horizontal temperature and vertical solutal gradients[END_REF].

Results and discussions

Two-and three-dimensional results are produced for free surface cubic enclosure and are compared with solid lid enclosure. Since the number of controlling parameters is quite few and the main objective of the work is to understand the effect of the upper surface conditions on the dynamics of fluid flow in the enclosure and on the rate of heat and mass transfer. Therefore, some parameters are fixed, such as Pr is set to 10 (aqua solution) and Lewis number is varied within the practical range, i.e., 1, 10 and 50. Also, the results are presented for Ra of 10 4 and 10 5 , where the flow becomes unstable for high Rayleigh numbers and the flow is mainly controlled by molecular diffusion for low Raleigh numbers. All the results are presented for wide range of N (species buoyancy to thermal buoyancy ratio), N changed from thermal controlled to species buoyancy controlled flows. The following sections discuss, first the average of rates of heat and mass transfer followed by flow structure.

For Le = 1.0, thickness of the thermal boundary layer and species concentration boundary layer are the same. Hence, the result must show that Nu av equal to Sh av . Also, at N = -1.0, the buoyancy force due to the thermal gradient must cancel the buoyancy force due to the concentration gradient, for opposing case, and Nusselt and Sherwood numbers should equal to unity, conduction condition. The results shown in Fig. 2 testify these facts. The difference in the rate of heat and mass transfer between solid and free surface lids increases for thermally driven flow, N = 0. and for species concentration driven flow, N -2.0. For N = 0, the rates of heat are about 2.45, 2.25, 2.25 and 2.07 for 2-D free lid, 2-D solid lid, 3-D free lid and 3-D solid lid, respectively. The results indicate that the flow is three-dimensional because there is a difference in prediction of the rate of heat transfer for 2-D and 3-D models and for same boundary conditions (free or solid). The rate of heat transfer increase for a free surface compared with solid surface are about 9% and about 8%, for 2-D and 3-D predictions, respectively. In general, the rate of heat transfer predicted for 3-D models is less than 2-D models. This can be explained by the fact that the fluid parcels in 3-D model form spiral path as they travel from hot boundary to cold boundary, i.e., more dissipative path. For The difference between flow structures for free and solid boundary is illustrated in Fig. 3 for Ra = 10 5 at three different lateral planes (X = 0.25, X = 0.5 and X = 0.75). The difference is not that significant. The strength of the upper vortices at the mid lateral plane for free surface is stronger than that of solid surface. These results indicate that the effect of upper boundary is not that significant at least for the investigated parameters.

For double diffusion problems (Le > 1) with opposing conditions, N should be negative and less than one. Also, it is noticed that for N less than -2, the flow is mainly controlled by buoyancy induced due to species concentration gradient. In general, a hysteresis is noticed for N order of -1.0. For these values of N , the flow structure is sensitive to the initial con- The transition region is similar to the transient region between laminar and turbulent flow. It should mention that the results converge to a solution but the solution is not unique. Also, the difference between 3-D and 2-D models predictions on the rate of heat and mass transfer is quite significant for the range of N between -1.6 and -0.6. Figs. 5(a) and 5(b) show the rate of heat transfer and mass transfer for Ra = 10 4 and for Le = 50, respectively. The trend of prediction is similar to Fig. 4, except that the difference between 2-D and 3-D predictions is significant for wide range of N values (from -1.6 to -0.4). For the mentioned range of N , the prediction of the 3-D model is mainly conduction, Nu av is order of unity, while 2-D model prediction is mainly convection dominated solution.

Conclusions

The effect of upper boundary conditions on the flow and rate of heat and mass transfer is addressed in this work, for enclosures filled with a liquid and subjected to differential heating and species concentrations. Four cases were studies, 2-D and 3-D with free surface and with non-permeable, solid surface. The results showed that the difference between four cases become significant for thermally controlled flow. The rate of heat and mass transfer are high for a 2-D enclosure with a free surface. The rate of heat and mass transfer for 3-D with solid surface is the lowest of all the cases. The difference in the rate of heat transfer between the highest and lowest values for different cases can be order of 20% for N = 0 (thermally driven flow) and Ra = 10 4 . Flow and rate of heat and mass transfer become sensitive for initial condition for a range of N , depending on the value of the controlling parameter. The strength of upper edge vortices becomes more profound for free surface enclosures.

As a summary the effect of the upper lid conditions is important and cannot be underestimated, especially for thermally driven flows.

Fig. 1 .

 1 Fig. 1. Schematic of the problem.

Fig. 2 .

 2 Fig. 2. Comparison between predictions of different models for the rate of heat and mass transfer for Ra = 10 4 .

Fig. 3 .

 3 Fig. 3. Stream trace for Ra = 10 5 , Le = 1.0, N = 0.0 for free surface lid and solid surface lid at X = 0.25 (top), X = 0.5 (middle) and X = 0.75 (bottom).

Fig. 4 .

 4 Fig. 4. (a) Average rate of heat transfer as a function of N for Ra = 10 4 and Le = 10. (b) Average Sherwood number as a function of N for Ra = 10 4 and Le = 10. Ra = 10 5 the rate of heat transfer predicted for 3-D free surface and 3-D solid lid was about 4.70 and 4.51, respectively. For Ra = 10 6 , the rate of heat transfer predicted for 3-D free surface and 3-D solid lid was 8.76 and 8.65, respectively.The difference between flow structures for free and solid boundary is illustrated in Fig.3for Ra = 10 5 at three different lateral planes (X = 0.25, X = 0.5 and X = 0.75). The difference is not that significant. The strength of the upper vortices at the mid lateral plane for free surface is stronger than that of solid surface. These results indicate that the effect of upper boundary is not that significant at least for the investigated parameters.For double diffusion problems (Le > 1) with opposing conditions, N should be negative and less than one. Also, it is noticed that for N less than -2, the flow is mainly controlled by buoyancy induced due to species concentration gradient. In general, a hysteresis is noticed for N order of -1.0. For these values of N , the flow structure is sensitive to the initial con-

Fig. 5 .

 5 Fig. 5. (a) Nusselt number as a function of N for Ra = 10 4 and Le = 50. (b) Sherwood number as a function of N for Ra = 10 4 and Le = 50.


François Hamel

Nikolai Nadirashvili

Parallel and circular flows for the two-dimensional Euler equations *

We consider steady flows of ideal incompressible fluids in two-dimensional domains. These flows solve the Euler equations with tangential boundary conditions. If such a flow has no stagnation point in the domain or at infinity, in the sense that the infimum of its norm over the domain is positive, then it inherits the geometric properties of the domain, for some simple classes of domains. Namely, if the domain is a strip or a halfplane, then such a flow turns out to be parallel to the boundary of the domain. If the domain is the plane, the flow is then a parallel flow, that is, its trajectories are parallel lines. If the domain is an annulus, then the flow is circular, that is, the streamlines are concentric circles. The results are based on qualitative properties and classification results for some semilinear elliptic equations satisfied by the stream function. * This work has been carried out in

Steady flows of a two-dimensional ideal fluid

We consider the incompressible Euler equations

v • ∇ v + ∇p = 0 in Ω, div v = 0 in Ω, (1.1)
in smooth two-dimensional connected subsets (domains) of R 2 . The vector field v is denoted by

v = (v 1 , v 2 )
and the scalar function p stands for the pressure. Both v and p are assumed to be (at least) of class C 1 (Ω) and the equations (1.1) are actually satisfied in Ω. The flow v is assumed to satisfy the boundary conditions v • n = 0 on ∂Ω, (

where n is the outward unit normal to Ω on ∂Ω. In other words, v is tangential on ∂Ω.

Due to the boundary conditions and the incompressibility condition div v = 0, the vector field v admits a stream function u satisfying

v = ∇ ⊥ u = - ∂u ∂x 2 , ∂u ∂x 1 .
(1.

3)

The function u, which is (at least) of class C 2 (Ω), is well-defined and unique up to an additive constant.

By definition, u is constant along the streamlines of the flow. The streamlines are the trajectories parametrized by the family of ordinary differential equations ξ(t) = v(ξ(t)). More precisely, for x ∈ Ω, let us denote ξ x the solution of ξx (t) = v(ξ x (t)),

ξ x (0) = x.
The function ξ x is of class C 1 and it is defined in a maximal open interval I x ⊂ R.

Throughout the paper, one assumes that the flow v has no stagnation point in Ω or at infinity, in the sense that inf Ω |v| > 0, (1.4) where | | denotes the Euclidean norm in R 2 . The goal of this review paper is to see that the smooth solutions v of (1.1)-(1.2) inherit the geometrical properties of the domains Ω, for some simple classes of domains Ω, as soon as they satisfy assumption (1.4) and possibly some further boundedness hypotheses. Namely, on the one hand, the flows turn out to be parallel flows in domains which are invariant by translation, such as strips, half-planes and the whole plane itself. On the other hand, the flows are circular in annular domains.

Parallel flows in strips

We deal in this section with two-dimensional strips (with bounded cross sections). Up to rotation and scaling, we only consider the strip Ω 2 ⊂ R 2 defined by

Ω 2 = R × (0, 1) = x = (x 1 , x 2 ) ∈ R 2 ; 0 < x 2 < 1 (2.1)
The flow v is called a shear or a parallel flow if there is a unit vector e = (e 1 , e 2 ) such that v is parallel to e. Thanks to the incompressibility condition div v = 0, this means that v can be written as

v(x) = V (x • e ⊥ ) e,
where V : R → R is a scalar function and e ⊥ = (-e 2 , e 1 ).

It is easy to see that the flow v is a shear flow if and only if the pressure p is a constant. The first main result says that the flow is parallel to the boundary in the whole domain under the assumption (1.4).

Theorem 2.1 [START_REF] Hamel | Shear flows of an ideal fluid and elliptic equations in unbounded domains[END_REF] Let Ω = Ω 2 be the strip defined by (2.1) and let v ∈ C 2 (Ω 2 ) solve the Euler equations (1.1) in Ω = Ω 2 together with the boundary conditions (1.2) on ∂Ω 2 . If v satisfies the assumption (1.4) in Ω 2 , then v is a parallel flow, that is,

v(x) = (v 1 (x 2 ), 0) in Ω 2 .
(2.

2)

The conclusion states that all streamlines of the flow are parallel lines which are parallel to ∂Ω 2 and therefore parallel to the x 1 -axis. Equivalently, this means that the stream function u defined in (1.3) depends only on the x 2 variable.

Theorem 2.1 means that any C 2 (Ω 2 ) non-parallel flow which is tangential on ∂Ω 2 must have a stagnation point in Ω 2 or at infinity. These stagnation points may well be in Ω 2 or only at infinity. For instance, on the one hand, for any α = 0, the non-parallel cellular flow of the type

v(x) = ∇ ⊥ sin(αx 1 ) sin(πx 2 ) = -π sin(αx 1 ) cos(πx 2 ), α cos(αx 1 ) sin(πx 2 ) , (2.3)
which solves (1.1)-(1.2) with pressure given by

p(x) = π 2 4 cos(2αx 1 ) + α 2 4 cos(2πx 2 ),
has a countable number of stagnation points in Ω 2 . On the other hand, the non-parallel flow

v(x) = ∇ ⊥ sin(πx 2 ) e x 1 = -π cos(πx 2 ) e x 1 , sin(πx 2 ) e x 1 , which solves (1.1)-(1.2) with p(x) = - π 2 2 e 2x 1 has no stagnation point in Ω 2 (|v| > 0 in Ω 2 ), but inf Ω 2 |v| = 0.
The condition (1.4) is then a simple condition for a flow solving (1.1)-(1.2) to be a parallel flow in a two-dimensional strip. We should however keep in mind that this condition is obviously not equivalent to being a shear flow, since any parallel flow v(x) = (v 1 (x 2 ), 0) in Ω 2 for which v 1 does not have a constant strict sign does not satisfy the condition inf Ω 2 |v| > 0 (however, under the conditions of Theorem 2.1, the first component

v 1 (x) = v 1 (x 2 ) in (2.2) has a constant strict sign in Ω 2 ).
The C 2 smoothness of the flow v is a technical assumption which plays a role in the proof. It implies that the stream function u defined by (1.3) is of class C 3 (Ω 2 ) and that the function f appearing in the elliptic equation ∆u + f (u) = 0 satisfied by u is itself of class C 1 and therefore locally Lipschitz-continuous, see (6.2) below. This smoothness property of f is used to guarantee that u satisfies some qualitative monotonicity and symmetry properties based on the maximum principle. We refer to Section 6 for further details.

Remark 2.2 Notice that in Theorem 2.1 the flow v is not assumed to be a priori bounded in Ω 2 . However, since v is (at least) continuous in Ω 2 and the interval [0, 1] is bounded, the conclusion of Theorem 2.1 implies that v is necessarily bounded.

Remark 2.3 Theorem 2.1 does not hold in dimension 3. More precisely, consider the cylinder

Ω = x = (x 1 , x 2 , x 3 ) ∈ R 3 ; x 2 2 + x 2 3 < 1 together with the vector field v(x) = (1, -x 3 , x 2 )
and the scalar function p(x) = (x 2 2 + x 2 3 )/2 defined in Ω. Then the pair (v, p) solves the Euler equations

(1.1)-(1.2) with 1 ≤ |v| ≤ √ 2 in Ω,
but the flow v is not a parallel flow.

Parallel flows in half-planes

Up to rotation and translation, we consider in this section the case of the half-plane Ω = R 2 + defined by

R 2 + = R × (0, +∞) = x = (x 1 , x 2 ) ∈ R 2 ; x 2 > 0 .
As in the strip Ω 2 , the flows v solving (1.1)-(1.2) turn out to be parallel to the boundary of the half-plane R 2 + under the assumption (1.4), here together with an additional uniform boundedness.

Theorem 3.1 [14] Let v ∈ C 2 (R 2 + ) solve the Euler equations (1.1) in Ω = R 2 + together with the boundary conditions (1.2) on ∂R 2 + . If v satisfies the assumption (1.4) in R 2 + and if v ∈ L ∞ (R 2 + ), then v is a parallel flow, that is, v(x) = (v 1 (x 2 ), 0) in R 2 + ,
and the first component v 1 has a constant strict sign in R 2 + .

The conclusion implies that all streamlines of the flow are parallel lines which are parallel to ∂R 2 + and therefore parallel to the x 1 -axis. Equivalently, this means that the stream function u defined in (1.3) depends only on the x 2 variable. Some comments are now in order on the conditions (1.4) and v ∈ L ∞ (R 2 + ), namely,

0 < inf R 2 + |v| ≤ sup R 2 + |v| < +∞. (3.1)
None of the two strict inequalities in (3.1) can be dropped for the conclusion to hold in general. More precisely, first, any cellular flow v of the type (2.3), which solves (1.1)-(1.2) with Ω = R 2 + , satisfies sup R 2 + |v| < +∞ and inf R 2 + |v| = 0, and it is not a parallel flow. Second, the flow

v(x) = ∇ ⊥ x 2 cosh(x 1 )) = (-cosh(x 1 ), x 2 sinh(x 1 )), which solves (1.1)-(1.2) with p(x) = - cosh(2x 1 ) 4 + x 2 2 2 , satisfies inf R 2 + |v| > 0 and sup R 2 + |v| = +∞,
∀ A > 0, 0 < inf R×(0,A) |v| ≤ sup R×(0,A) |v| < +∞.
4 Parallel flows in the plane Let us now consider in this section flows solving the Euler equations (1.1) in the whole plane Ω = R 2 .

In this case, there is no boundary and there is no obvious streamline. However, the following result implies that, under the only conditions (3.1) in the plane R 2 , the C 2 (R 2 ) solutions of (1.1) are still parallel flows, which are parallel to some non-zero vector e (the vector e depends on the flow v, and it can be now any vector unlike in strips or half-planes).

Theorem 4.1 [15] Let v be a C 2 (R 2 ) flow solving (1.1) with Ω = R 2 . If v satisfies the assumption (1.4) in R 2 and if v ∈ L ∞ (R 2 )
, then v is a parallel flow, that is, there exist a non-zero vector e and a function V : R → R with constant strict sign such that

v(x) = V (x • e ⊥ ) e in R 2 .
The conclusion means that all streamlines of the flow are parallel lines which are parallel to the direction e. In other words, the stream function u defined in (1.3) depends only on the orthogonal variable x • e ⊥ . Like Theorems 2.1 and 3.1, Theorem 4.1 can also be viewed as a Liouville-type rigidity result since the conclusion says that the argument of the flow is actually constant (the argument of the flow is any continuous function φ : R 2 → R satisfying

v(x) |v(x)| = (cos φ(x), sin φ(x)) in R 2 , see (6.
3) in Section 6 for further details), and that the pressure p is constant as well.

Let us now comment the two main assumptions (1.4) and v ∈ L ∞ (R 2 ) made in Theorem 4.1. Firstly, the assumption (1.4) means that the flow v has no stagnation point in R 2 or at infinity. In other words, Theorem 4.1 implies that any C 2 (R 2 ) ∩ L ∞ (R 2 ) flow which is not a parallel flow must have a stagnation point in R 2 or at infinity, that is, it must satisfy inf R 2 |v| = 0). Without the condition (1.4), the conclusion of Theorem 4.1 does not hold in general. For instance, for any (α,

β) ∈ R * × R * , the C 2 (R 2 ) ∩ L ∞ (R 2 ) cellular flow v defined in R 2 by v(x 1 , x 2 ) = ∇ ⊥ sin(αx 1 ) sin(βx 2 ) = -β sin(αx 1 ) cos(βx 2 ), α cos(αx 1 ) sin(βx 2 ) , which solves (1.1) with p(x) = β 2 4 cos(2αx 1 ) + α 2 4 cos(2βx 2 ),
has countably many stagnation points in R 2 , and it is not a parallel flow. However, as for Theorems 2.1 and 3.1, the sufficient condition (1.4) is obviously not equivalent to being a shear flow. Indeed, any continuous shear flow v(x) = V (x • e ⊥ ) e for which V changes sign (or more generally if inf R |V | = 0) does not satisfy the condition (1.4). Secondly, without the boundedness of v, the conclusion of Theorem 4.1 does not hold either in general. For instance, the C 2 (R 2 ) flow v defined in R 2 by v(x) = ∇ ⊥ x 2 cosh(x 1 )) = (-cosh(x 1 ), x 2 sinh(x 1 )), which solves (1.1) with

p(x) = - cosh(2x 1 ) 4 + x 2 2 2 , satisfies inf R 2 |v| = 1 > 0 but it is not bounded in R 2
, and it is not a parallel flow. Theorem 4.1 has some immediate consequences regarding non-vanishing periodic flows and the stability of non-vanishing parallel flows under small L ∞ perturbations. These consequences are stated in the following corollary. In the statement, we say that a flow v is periodic if there is a basis (e 1 , e 2 ) of

R 2 such that v(x) = v(x + k 1 e 1 + k 2 e 2 ) in R 2 for all x ∈ R 2 and (k 1 , k 2 ) ∈ Z 2 . Corollary 4.2 (i) Let v be a C 2 (R 2 ) periodic flow solving (1.1) in Ω = R 2 . If |v(x)| = 0 for all x ∈ R 2 ,
then v is a parallel flow. In other words, if v is not a parallel flow, then it has stagnation points. (ii) Let v be a bounded parallel flow solving (1.1) in Ω = R 2 and satisfying (1.4). There Here, the notion of parallel flows does not make sense anymore. A meaningful notion is that of circular flows. Namely, a flow v in Ω a,b is called a circular flow if v(x) is parallel to the vector e θ (x) for every x ∈ Ω a,b , that is, v • e r = 0 in Ω a,b . Together with the incompressibility assumption, this means that v can be written as The conclusion means that all streamlines of the flow are concentric circles. In other words, the stream function u defined in (1.3) is radially symmetric and, thanks to the condition |v| > 0 and the continuity of v in Ω a,b , the function u is also strictly monotone with respect to the radial variable |x|.

is ε > 0 such that, if v is a C 2 (R 2 ) flow solving (1.1) in Ω = R 2 and satisfying v -v L ∞ (R 2 ) ≤ ε, then v is a parallel flow.
v(x) = V (|x|) e θ (x) in Ω a,b , for some function V : [a, b] → R.
The as |x| → 0 or as |x| → ∞, respectively. We also mention other rigidity results for the stationary solutions of (1.1), such as the analyticity of the streamlines under a condition of the type v 1 > 0 in the unit disc [START_REF] Koch | Partial analyticity and nodal sets for nonlinear elliptic systems[END_REF], and the local correspondence between the vorticities of the solutions of (1.1) and the co-adjoint orbits of the vorticities for the non-stationary version of (1.1) in annular domains [START_REF] Choffrut | Local structure of the set of steady-state solutions to the 2D incompressible Euler equations[END_REF].

6 Semilinear ellliptic equations satisfied by the stream function

In this section, we explain the main lines of the proofs of Theorems 2.1, 3.1, 4.1 and 5.1.

They are based on the study of the geometric properties of the streamlines of the flow v, that is, on the qualitative planar or radial symmetry properties of the stream function u defined in (1.3). The streamlines are indeed the connected components of the level sets of u.

In the strip Ω 2 defined in (2.1) and in the half-plane R 2 + , the goal is to show that the stream function u depends only on the variable x 2 . In the whole plane R 2 , Theorem 4.1 means that the function u is one-dimensional. Lastly, in the annulus Ω a,b defined in (5.1), the goal is to show that u is radially symmetric.

To achieve this goal, one uses the trajectories of the gradient flow, which are parametrized by the solutions of the equations σx (t) = ∇u(σ x (t)), σ x (0) = x, with x ∈ Ω and σ x (t) ∈ Ω. These trajectories are orthogonal to the streamlines, since v = ∇ ⊥ u. An important observation is that, due to (1.4), the function

g : t → u(σ x (t))
is increasing on its interval of definition, and furthermore

g (t) ≥ (inf Ω |v|) 2 > 0.
When Ω is the strip Ω 2 , it is shown in [START_REF] Hamel | Shear flows of an ideal fluid and elliptic equations in unbounded domains[END_REF] that the stream function u is bounded in Ω 2 and that each function σ x is defined in a compact interval. The same property holds if Ω is the annulus Ω a,b , see [START_REF] Hamel | Circular flows for the Euler equations in two-dimensional annular domains[END_REF]. When Ω is the half-plane R 2 + , each function σ x is defined in a closed semi-infinite interval. Finally, if Ω is the whole plane R 2 , then each function σ x is defined in the whole interval R, see [START_REF] Hamel | A Liouville theorem for the Euler equations in the plane[END_REF].

Furthermore, in all these four cases, it is shown that the streamlines foliate the set Ω is a monotone way, in the sense that

Ω = y∈Σx Γ y , (6.1)
where x is any point in Ω, Σ x is the trajectory of the gradient flow in Ω and containing x, and Γ y is the streamline containing y. The above formula, which is a key-point is the proofs, is based on a continuation argument and on the property that, due to (1.4), the streamlines of two close points stay close to each other in the sense of the Hausdorff distance. It follows from these arguments that, when Ω is the strip Ω 2 or the half-plane R 2 + , then the projection on the x 1 -axis of each streamline is equal to that whole axis and furthermore that each streamline is bounded in the x 2 direction when Ω = R 2 + . However, this property does not imply yet that each streamline is a line parallel to the x 1 -axis.

Another key-observation is the fact that, due to (1.1), the vorticity

∂v 2 ∂x 1 - ∂v 1 ∂x 2 = ∆u
is constant along any streamline of the flow v. Since u is strictly monotone along any trajectory Σ x of the gradient flow, it then follows from (6.1) that the stream function u satisfies a semilinear elliptic equation of the type ∆u + f (u) = 0 in Ω, (

where f is a C 1 function defined on the range of u in Ω (the range of u in Ω is a compact interval when Ω = Ω 2 or Ω a,b , it is a closed semi-infinite interval when Ω = R 2 + and it is equal to R when Ω = R 2 ).

Regarding the case of the strip Ω 2 = R × (0, 1), each trajectory Σ x of the gradient flow in Ω 2 ends on the two connected components of the boundary. Since u is strictly monotone along Σ x and is constant along the two connected components of ∂Ω 2 , it follows that u is bounded from above and below in Ω 2 by its two constant values on the two connected components of ∂Ω 2 . Therefore, up to changing v into -v and up to normalization of u, Theorem 2.1 reduces to the following Liouville type result. Then u depends only on the variable x 2 , that is, there is a function

U : [0, 1] → R such that u(x 1 , x 2 ) = U (x 2 ) in Ω 2 ,
and U > 0 in (0, 1).

As a matter of fact, under the assumptions of Theorem 6.1, it follows from [3, Theorem 1.1'] applied to u, resp. to c -u(x 1 , 1 -x 2 ), that

u x 2 = ∂u ∂x 2 > 0 in (x 1 , x 2 ) ∈ R 2 ; 0 < x 2 < 1/2 , resp. u x 2 > 0 in (x 1 , x 2 ) ∈ R 2 , 1/2 < x 2 < 1
(notice that such a monotonicity is known only in dimension 2 without any further assumptions on f ). Therefore, u x 2 ≥ 0 in Ω 2 . The new result in Theorem 6.1 is the fact that the monotonicity property u x 2 ≥ 0 in Ω 2 implies that u is one-dimensional, that is, u depends only on x 2 . The proof of this property is based on the maximum principle and on a sliding method [START_REF] Berestycki | On the method of moving planes and the sliding method[END_REF], namely one can show that

u(x) ≤ u λτ (x) := u(x 1 + λτ 1 , x 2 + λτ 2 ) for every (τ 1 , τ 2 ) ∈ R × (0, +∞), λ ∈ (0, 1/τ 2 ) and x ∈ R × [0, 1 -λτ 2 ]
. By letting τ 2 → 0 + , it then immediately follows that u is both non-decreasing and non-increasing with respect to the variable x 1 in Ω 2 , that is, u depends only on x 2 . As a consequence, the flow v is parallel to the x 1 -axis. Actually, it turns out that the last part of the argument based on the sliding method holds in any dimension n ≥ 2: Theorem 6.2 [START_REF] Hamel | Shear flows of an ideal fluid and elliptic equations in unbounded domains[END_REF] Let n ≥ 2, let c > 0, let f : [0, c] → R be a Lipschitz continuous function and let u be a C 2 (Ω n ) solution of the equation (6.2) in the n-dimensional slab Ω n defined by

Ω n = R n-1 × (0, 1) = x = (x 1 , . . . , x n ) ∈ R n , 0 < x n < 1 , such that u = 0 on {x n = 0} and u = c on {x n = 1}.
Suppose also that u is non-decreasing with respect to the variable x n , namely

u xn = ∂u ∂x n ≥ 0 in Ω n .
Then u depends only on x n , that is, there is a function U

: [0, 1] → R such that u(x 1 , . . . , x n ) = U (x n ) in Ω n ,
and U (x n ) > 0 for all 0 < x n < 1.

In the case of the half-plane Ω = R 2 + , one can show from (6.1) that, up to changing v into -v and up to normalization of u, the function u vanishes on ∂R 2 + and is positive in R 2 + , see [START_REF] Hamel | Shear flows of an ideal fluid and elliptic equations in unbounded domains[END_REF]. To conclude the proof of Theorem 3.1, we use some monotonicity and one-dimensional symmetry results [START_REF] Berestycki | Further qualitative properties for elliptic equations in unbounded domains[END_REF][START_REF] Farina | Flattening results for elliptic PDEs in unbounded domains with applications to overdetermined problems[END_REF] for positive solutions with bounded gradient of semilinear elliptic equations (6.2) in R 2 + with Dirichlet boundary conditions: namely, u then depends only on x 2 and the flow v is parallel to the x 1 -axis.

Regarding Theorem 4.1 in the case of the whole plane R 2 , there is no boundary and therefore no boundary condition for the stream u. As a consequence, u is not constant along a given obvious line, unlike in the case of the strip Ω 2 or the half-plane R 2 + . One then uses a completely different method. Namely, one considers the C 2 (R 2 ) argument φ of the flow, defined by

v(x) |v(x)| = (cos φ(x), sin φ(x)) for all x ∈ R 2 .
The argument φ is uniquely defined in a continuous way, up to an additive multiple of 2π.

From the equation (6.2) satisfied by the stream function u, it turns out that the argument φ satisfies the equation div(|v| 2 ∇φ) = 0 in R 2 . (6.3)

Notice that this equation is uniformly elliptic thanks to the assumption (1.4) and the boundedness of v in Theorem 4.1. The difficult key-point consists in proving that the argument φ grows at most as ln R in balls of large radius R, see [START_REF] Hamel | A Liouville theorem for the Euler equations in the plane[END_REF]. Finally, one uses a compactness argument and some results of Moser [START_REF] Moser | On Harnack's theorem for elliptic differential equations[END_REF] on the at-least-algebraic growth of the oscillations of the non-constant solutions of uniformly elliptic equations of the type (6.3) to conclude that the argument φ is actually constant. This immediately means that the flow v is a parallel flow. for some non-zero vector e, then the end of the proof of Theorem 4.1 would be much simpler: indeed, in that case, the argument φ of the flow is automatically bounded and the results of Moser [START_REF] Moser | On Harnack's theorem for elliptic differential equations[END_REF] imply that φ is constant. One can also conclude with another argument which does not use (6.3). Namely, the assumption v • e > 0 in R 2 implies that the stream function u is monotone in the direction e ⊥ . Since u satisfies the semilinear elliptic equation of the type

∆u + f (u) = 0 in R 2
with f ∈ C 1 (R), it then follows that u is one-dimensional, as in the proof of a related conjecture of De Giorgi [START_REF] Giorgi | Convergence problems for functionals and operators[END_REF] in dimension 2 (see [START_REF] Berestycki | Further qualitative properties for elliptic equations in unbounded domains[END_REF][START_REF] Ghoussoub | On a conjecture of De Giorgi and some related problems[END_REF] and see also [START_REF] Alberti | On a long-standing conjecture of E. De Giorgi: old and recent results[END_REF][START_REF] Ambrosio | Entire solutions of semilinear elliptic equations in R 3 and a conjecture of De Giorgi[END_REF][START_REF] Del Pino | On the De Giorgi conjecture in dimension N ≥ 9[END_REF][START_REF] Farina | Liouville-type theorems for elliptic equations[END_REF][START_REF] Farina | The state of the art for a conjecture of De Giorgi and related problems[END_REF][START_REF] Savin | Regularity of flat level sets in phase transitions[END_REF] for further references in that direction). Finally, since u is one-dimensional, the vector field v is a parallel flow.

Finally, regarding Theorem 5.1 in the case of the annuli Ω a,b defined in (5.1), the stream function u satisfies a semilinear elliptic equation of the type (6.2) in Ω a,b and it is equal to two different constants on the two connected components of the boundary ∂Ω a,b . By using a moving plane method as in [START_REF] Fraenkel | An introduction to maximum principles and symmetry in elliptic problems[END_REF][START_REF] Gidas | Symmetry and related properties via the maximum principle[END_REF], one then concludes that u is radially symmetric and strictly monotone with respect to |x|, meaning that v is a circular flow. We refer to [START_REF] Hamel | Circular flows for the Euler equations in two-dimensional annular domains[END_REF] for further details and further results in punctured discs and complements or discs.

Question 3 . 2

 32 and it is not a parallel flow. An interesting open question would be to see whether the conclusion of Theorem 3.1 still holds if condition (3.1) is replaced by the following weaker one

Theorems 2 .

 2 1 and 3.1 show that, in strips and in half-planes, the C 2 flows solving the Euler equations (1.1) and the boundary conditions (1.2), together with the no-stagnationpoint assumption (1.4) (and a boundedness assumption in half-planes), are automatically parallel flows whose streamlines are all parallel lines to the boundary. Actually, in these two geometrical configurations, since the flows are assumed to be tangential on the boundary and to satisfy (1.4), the boundary ∂R 2 + (for Theorem 3.1) and each connected component of ∂Ω 2 (for Theorem 2.1) are streamlines of the flow. The conclusions of Theorems 2.1 and 3.1 mean that all other streamlines are parallel to these obvious streamlines.

Remark 4 . 3

 43 Other Liouville-type and rigidity theorems are known for the Navier-Stokes equations in the plane R 2 , namely any bounded solution of the Navier-Stokes equations in the plane is constant, see[START_REF] Koch | Liouville theorems for the Navier-Stokes equations and applications[END_REF].5 Circular flows in two-dimensional annuliLet us finally consider the case of two-dimensional annuli defined byΩ a,b = x ∈ R 2 ; a < |x| < b ,(5.1) where a < b are two positive real numbers. Let us also define e r (x) = x |x| and e θ (x) = e r (x) ⊥ = -x 2 |x| , x 1 |x| for any x = (x 1 , x 2 ) ∈ R 2 \{(0, 0)}. In the circular domains Ω a,b , one still considers the Euler equations (1.1) together with the tangential boundary conditions (1.2), meaning that v•e r = 0 on ∂Ω a,b .

Theorem 5 . 1 [ 16 ]

 5116 Let v ∈ C 2 (Ω a,b ) solve the Euler equations (1.1) in Ω = Ω a,b together with the boundary conditions (1.2) on ∂Ω a,b . If |v| > 0 in Ω a,b , then v is a circular flow, and the function v • e θ has a constant strict sign in Ω a,b .

Remark 5 . 2

 52 assumption |v| > 0 in Ω a,b means that the flow v has no stagnation point in Ω a,b . Theorem 5.1 then implies that any C 2 (Ω a,b ) flow which is tangential on ∂Ω a,b and is not a circular flow must have at least one stagnation point in Ω a,b .Without the assumption |v| > 0 in Ω a,b , the conclusion of Theorem 5.1 does not hold in general. Indeed, for every givenC 1 (R) function f , any non-radial solution u ∈ C 3 (Ω a,b ) of ∆u + f (u) = 0 in Ω a,b(5.2)which is constant on each connected component of ∂Ω a,b and which has a critical point gives rise to a non-circular solutionv = ∇ ⊥ u ∈ C 2 (Ω a,b ) of (1.1)-(1.2) with a stagnation point (notice that v defined as above solves (1.1) for some pressure p ∈ C 2 (Ω a,b ) because v • ∇v is curl-free thanks to (5.2) and because the integral of (v • ∇v) • e θ over the circle {x ∈ R 2 ; |x| = a} is equal to zero). For instance, letλ ∈ R and ϕ ∈ C ∞ ([a, b]) denote the principal eigenvalue and eigenfunction of the eigenvalue problem -ϕ (r) -r -1 ϕ (r) + r -2 ϕ(r) = λ ϕ(r) in [a, b] with ϕ > 0 in (a, b) and Dirichlet boundary condition ϕ(a) = ϕ(b) = 0. The function u ∈ C ∞ (Ω a,b ) defined by u(x) = ϕ(|x|) x 1 |x| (that is, u(x) = ϕ(r) cos θ in the usual polar coordinates) satisfies ∆u + λu = 0 in Ω a,b and has some critical points in Ω a,b (since min Ω a,b u < 0 < max Ω a,b u and u = 0 on ∂Ω a,b ). Then the flow v = ∇ ⊥ u ∈ C 2 (Ω a,b ) is a non-circular flow solving (1.1)-(1.2) and it has some stagnation points in Ω a,b . However, the sufficient condition |v| > 0 in Ω a,b is obviously not equivalent to being a circular flow, in the sense that there are circular flows with stagnation points. The trivial flow v = 0 is an obvious example! More generally speaking, any C 2 (Ω a,b ) circular flow v(x) = V (|x|) e θ (x) solving (1.1)-(1.2) with Ω = Ω a,b and for which V ∈ C 2 ([a, b]) does not have a constant strict sign, is then such that min Ω a,b |v| = 0. For instance, if µ ∈ R and φ ∈ C ∞ ([a, b]) denote the principal eigenvalue and eigenfunction of the eigenvalue problem -φ (r) -r -1 φ (r) = µ φ(r) in [a, b] with φ > 0 in (a, b) and Dirichlet boundary condition φ(a) = φ(b) = 0, then the vector field v defined by v = ∇ ⊥ u, with u(x) = φ(|x|), is a C 2 (Ω a,b ) non-trivial circular flow solving (1.1)-(1.2) with infinitely many stagnation points in Ω a,b : more precisely, if r * ∈ (a, b) denotes the real number such that φ(r * ) = max [a,b] φ (from elementary arguments, r * turns out to be the only critical point of φ in [a, b]), then the set of stagnation points of the flow v is the whole circle x ∈ R 2 ; |x| = r * , since v(x) = φ (|x|) e θ (x) in Ω a,b . Further results similar to Theorem 5.1 are proved in [16] for the solutions v of (1.1)-(1.2) with Ω = Ω a,b when a = 0 < b < ∞ (Ω 0,b is a punctured disc, and no boundary condition are imposed on the set {0} ⊂ ∂Ω 0,b ) and when 0 < a < b = ∞ (Ω a,∞ is the complement of a closed disc), together with some a priori bounds on the growth of |v(x)|

Theorem 6 . 1 [ 14 ]

 6114 Let c > 0, let f : [0, c] → R be a Lipschitz continuous function and let u be a C 2 (Ω 2 ) solution of the equation (6.2) in the strip Ω 2 , such that u = 0 on {x 2 = 0}, u = c on {x 2 = 1}, and 0 < u < c in Ω 2 .

Remark 6 . 3

 63 If, in addition to the condition inf R 2 |v| > 0, one assumes thatv • e > 0 in R 2

A*MIDEX project (ANR-11-IDEX-0001-02), funded by the "Investissements d'Avenir" French Government program managed by the French National Research Agency (ANR). The research leading to these results has also received funding from the European Research Council under the European Union's Seventh Framework Programme (FP/2007-2013) ERC Grant Agreement n. 321186 -ReaDi -Reaction-Diffusion Equations, Propagation and Modelling and from the ANR NONLOCAL project (ANR-14-CE25-0013).

the framework of Archimède Labex (ANR-