François Fages
email: francois.fages@inria.frsylvain.soliman@inria.fr

Thierry Martinez
email: thierry.martinez@inria.fr

David A Rosenblueth

Sylvain Soliman

Influence Systems vs Reaction Systems

In Systems Biology, modelers develop more and more reaction-based models to describe the mechanistic biochemical reactions underlying cell processes. They may also work, however, with a simpler formalism of influence graphs, to merely describe the positive and negative influences between molecular species. The first approach is promoted by reaction model exchange formats such as SBML, and tools like CellDesigner, while the second is supported by other tools that have been historically developed to reason about boolean gene regulatory networks. In practice, modelers often reason with both kinds of formalisms, and may find an influence model useful in the process of building a reaction model. In this paper, we introduce a formalism of influence systems with forces, and put it in parallel with reaction systems with kinetics, in order to develop a similar hierarchy of boolean, discrete, stochastic and differential semantics. We show that the expressive power of influence systems is the same as that of reaction systems under the differential semantics, but weaker under the other interpretations, in the sense that some discrete behaviours of reaction systems cannot be expressed by influence systems. This approach leads us to consider a positive boolean semantics which we compare to the asynchronous semantics of gene regulatory networks à la Thomas. We study the monotonicity properties of the positive boolean semantics and derive from them an efficient algorithm to compute attractors.

Introduction

In Systems Biology, modelers develop more and more reaction models to describe the biochemical reactions underlying cell processes. This approach is promoted by reaction-model exchange formats such as SBML [START_REF] Hucka | The systems biology markup language (SBML): A medium for representation and exchange of biochemical network models[END_REF] and by the subsequent creation of large reaction-based model repositories such as BioModels [START_REF] Le Novère | BioModels Database: a free, centralized database of curated, published, quantitative kinetic models of biochemical and cellular systems[END_REF], without prejudging of their interpretation by differential equations, Markov chains, Petri nets, or boolean transition systems [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF].

Modelers can also work, however, with a simpler formalism of influence systems to merely describe the positive and negative influences between molecular species, without fixing their implementation with biochemical reactions. In particular, boolean influence systems have been popularized in the 70's by Glass, Kauffman [START_REF] Glass | The logical analysis of continuous, non-linear biochemical control networks[END_REF] and Thomas [START_REF] Thomas | Boolean formalisation of genetic control circuits[END_REF][START_REF] Thomas | Biological Feedback[END_REF] to reason about gene regulatory networks, represented by ordinary graphs between genes given with a boolean transition table which defines their synchronous or asynchronous boolean transition semantics. Necessary conditions for multi-stability (cell differentiation) and oscillations (homeostasis) have been given in terms of positive or negative circuits in the influence graph [START_REF] Remy | Graphic requirements for multistability and attractive cycles in a boolean dynamical framework[END_REF][START_REF] Ruet | Local cycles and dynamical properties of boolean networks[END_REF]. Several tools such as GINsim [START_REF] Naldi | Logical modelling of regulatory networks with GINsim 2.3[END_REF], GNA [4] or Griffin [START_REF] Rosenblueth | Inference of Boolean networks from gene interaction graphs using a SAT solver[END_REF], use these properties and powerful graph-theoretic and model-checking techniques to automate reasoning about the boolean state transition graph, compute attractors and verify various reachability and path properties. The representation of boolean influence systems by Petri nets was described in [START_REF] Chaouiya | Petri net modelling of biological networks[END_REF] but leads to complicated encodings. It is also worth mentioning that influence systems with spatial information have been nicely developed in [7] as a formalism particularly suitable for describing natural algorithms in life sciences and social dynamics.

In Systems Biology, modelers often reason with both kinds of formalisms, and may find it useful to use and maintain an influence model in the process of building a reaction model, for instance in order to reduce it while preserving the essential influence circuits [START_REF] Naldi | A reduction method for logical regulatory graphs preserving essential dynamical properties[END_REF]. One reason is that it is easier to visualize influence systems, rather than reaction systems for which complicated graphical conventions such as SBGN [START_REF] Le Novere | The systems biology graphical notation[END_REF] have been developed. While it is clear that the influence graph is an abstraction of the reaction hypergraph [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF], and perhaps more surprisingly that the Jacobian influence system derived from the differential semantics of a reaction system is largely independent of the kinetics [START_REF] Fages | From reaction models to influence graphs and back: a theorem[END_REF], influence models are mostly used for their graphical representation and their boolean semantics, but more rarely as a modeling paradigm for systems biology with quantitative semantics using differential equations, or stochastic semantics.

In this paper, we introduce a formalism of influence systems with forces, which we put in parallel with reaction systems with kinetics, in order to develop a similar hierarchy of boolean, discrete, stochastic and differential semantics for influence systems, similarly to what is done for reasoning about programs in the framework of abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF][START_REF] Fages | Abstract interpretation and types for systems biology[END_REF]. We show that the expressive power of influence systems is the same as that of reaction systems under the differential semantics, but is weaker under the other interpretations, in the sense that some formal discrete behaviours of reaction systems cannot be expressed by influence systems. This approach provides an influence model with a hierarchy of possible interpretations related by precise abstraction relationships, so that, for instance, if a behavior is not possible in the boolean semantics, it is surely not possible in the stochastic semantics whatever the influence forces are. This leads us to consider a positive boolean semantics which we compare to the asynchronous semantics of gene regulatory networks à la Thomas. We study the monotonicity properties of the positive boolean semantics and derive from them an efficient algorithm to compute attractors. These concepts are illustrated with models from the literature.

In this article, unless explicitly noted, we will denote by capital letters (e.g. S) sets or multisets, by bold letters (e.g., x) vectors and by small roman or Greek letters elements of those sets or vectors (e.g. real numbers, functions). For a multiset M , let Set(M ) denote the set obtained from the support of M , and brackets like M (i) denote the multiplicity in the multiset (usually the stoichiometry). ≥ will denote the pointwise order for vectors, multisets and sets (i.e. inclusion).

Syntax

We recall here definitions from [START_REF] Fages | Inferring reaction systems from ordinary differential equations[END_REF][START_REF] Fages | From reaction models to influence graphs and back: a theorem[END_REF] for directed reactions with inhibitors: Definition 1. A reaction over molecular species S = {x 1 , . . . , x s } is a quadruple (R, M, P, f ), also noted f for R/M ⇒ P , where R is a multiset of reactants, M a set of inhibitors, P a multiset of products, all composed of elements of S, and f : R s → R, called kinetic expression, is a mathematical function over molecular species concentrations. A reaction system is a finite set of reactions.

It is worth noting that a molecular species in a reaction can be both a reactant and a product (i.e. a catalyst), or both a reactant and an inhibitor (e.g. Botts-Morales enzymes [START_REF] Katsumata | Graphic representation of Botts-Morales equation for enzymesubstrate-modifier system[END_REF]). Such molecular species are not distinguished in SBML and both are called reaction modifiers. Unlike SBML, we find it useful to consider only directed reactions (reversible reactions being represented here by two reactions) and to enforce the following compatibility conditions between the kinetic expression and the structure of a reaction.

Definition 2 ( [START_REF] Fages | Inferring reaction systems from ordinary differential equations[END_REF][START_REF] Fages | From reaction models to influence graphs and back: a theorem[END_REF]). A reaction (R, M, P, f ) over molecular species {x 1 , . . . , x s } is well formed if the following conditions hold:

1. f (x 1 , . . . , x s ) is a partially differentiable function, non-negative on R s + ; 2. x i ∈ R if and only if ∂f /∂x i (x) > 0 for some value x ∈ R s + ; 3. x i ∈ M if and only if ∂f /∂x i (x) < 0 for some value x ∈ R s + .
A reaction system is well formed if all its reactions are well formed.

Example 1. The classical prey-predator model of Lotka-Volterra can be represented by the following well-formed reaction system (without reaction inhibitors) between a proliferating prey A and a predator B:

Hierarchy of Semantics

As detailed in [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF], a reaction system can be interpreted with different formalisms that are formally related by abstraction relationships in the framework of abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and form a hierarchy of semantics. We simply recall here the definitions of the different semantics of a reaction system. The differential semantics corresponds to the association of an Ordinary Differential Equation (ODE) system with the reactions in the usual way:

dx j dt = (Ri,Mi,Pi,fi) (P i (j) -R i (j)) × f i
It is worth noting that in this interpretation, the inhibitors are supposed to decrease the reaction rate but do not prevent the reaction from proceeding with effects on the products and reactants. For instance, in Ex. 2, we get the classical Lotka-Volterra equations dB/dt = k1 * A * B -k3 * B, dA/dt = k2 * A-k1 * A * B, and the well-known oscillations between the concentrations of the prey and the predator.

The stochastic semantics for reaction systems defines transitions between discrete states describing numbers of each molecule, i.e. vectors x of N s . A transition is enabled if there are enough reactants, and the reaction propensity is defined by the kinetics:

∀(R i , M i , P i , f i ), x -→ fi S x with propensityf i if x ≥ R i , x = x -R i + P i
Transition probabilities between discrete states are obtained through normalization of the propensities of all enabled reactions, and the time of next reaction can be computed from the rates à la Gillespie [START_REF] Gillespie | Exact stochastic simulation of coupled chemical reactions[END_REF]. In this interpretation, the inhibitors are supposed to decrease the reaction propensity but do not prevent the reaction from occurring. They are thus ignored here by the stochastic transition conditions as in the differential semantics. In Ex. 1, the stochastic interpretation can exhibit some oscillations similar to the differential interpretation, and (almost surely) the extinction of the predator. The discrete, or Petri Net, semantics is similar but ignores the kinetics and is thus a trivial abstraction of the stochastic semantics by a forgetful functor:

∀(R i , M i , P i , f i ), x -→ D x if x ≥ R i , x = x -R i + P i
The boolean semantics is similar to the discrete one but on boolean vectors x of B s , obtained by the "zero, non-zero" abstraction of integers. With this abstraction, when the number of a molecule is decremented, it can still remain present, or become absent. It is thus necessary to take into account all the possible complete consumption or not of the reactants in order to obtain a correct boolean abstraction of the discrete and stochastic semantics [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF]. The boolean transition system -→ B is thus defined by:

∀(R i , M i , P i , f i ), ∀C ∈ P(Set(R i )), x -→ B x if x ⊇ Set(R i ), x = x\C ∪Set(P i )
It is worth remarking that in Ex. 2 under this boolean interpretation, one can observe either the stable coexistence of the prey and the predator, or the extinction of the predator with or without the preceding extinction of the prey.

As proven in [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF], the last three of these semantics are related by successive Galois connections, which means that if a behaviour is not possible in the boolean semantics, it is not possible in the stochastic semantics whatever the reaction kinetics are. On the other hand, the first differential semantics is not an abstraction but rather a limit of the first one for high number of molecules, as shown for instance in [START_REF] Gillespie | Exact stochastic simulation of coupled chemical reactions[END_REF].

It is worth noticing that the set of inhibitors of a reaction is just a syntactical annotation which has not been used to define the different semantics of the hierarchy. One can also consider a boolean semantics with negation where the set of inhibitors of a reaction is seen as a conjunction of negative conditions for the transition (disjunctions can be represented with several reactions). The boolean with negation transition system -→ BN is then defined by:

∀(R i , M i , P i , f i )∀C ∈ P(Set(R i ))x -→ BN x if x ⊇ Set(R i ), x ∩ M i = ∅, x = x \ C ∪ Set(P i
) However, this strict interpretation of inhibitors by negations restricts the set of possible boolean transitions and is not compatible with the differential semantics, since in that interpretation an inhibitor may just slightly decrease the rate of a reaction without preventing it from proceeding.

Influence Graph of a Reaction System

Here we recall two definitions of the influence graph associated with a reaction system, and their equivalence under general assumptions [START_REF] Fages | From reaction models to influence graphs and back: a theorem[END_REF][START_REF] Fages | Inferring reaction systems from ordinary differential equations[END_REF]. The first definition is based on the Jacobian matrix J formed of the partial derivatives J ij = ∂ ẋi /∂x j , where ẋi is defined by the differential semantics. Definition 3. The differential influence graph associated with a reaction system is the graph having for vertices the molecular species, and for edge-set the following two kinds of edges:

{A → + B | ∂ ẋ B /∂x A > 0 for some value x ∈ R s + } ∪{A → -B | ∂ ẋ B /∂x A < 0 for some value x ∈ R s + } Definition 4.
The syntactical influence graph associated with a reaction system M is the graph having for vertices the molecular species, and for edges the following set of positive and negative influences:

{A → + B | ∃(R i , M i , P i , f i ) ∈ M , (R i (A) > 0 and P i (B) -R i (B) > 0) or (A ∈ M i and P i (B) -R i (B) < 0)} ∪{A → -B | ∃(R i , M i , P i , f i ) ∈ M , (R i (A) > 0 and P i (B) -R i (B) < 0) or (A ∈ M i and P i (B) -R i (B) > 0)}
The syntactical graph is trivial to compute, in linear time, by browsing the syntax of the rules. Both definitions are equivalent under general assumptions:

Theorem 1 ( [START_REF] Fages | Inferring reaction systems from ordinary differential equations[END_REF][START_REF] Fages | From reaction models to influence graphs and back: a theorem[END_REF]). For any well-formed reaction system such that the syntactical influence graph contains no conflict (i.e. no pair of the form A → + B and A → -B), the syntactical and differential influence graphs are identical.

Reaction systems allow the description of mechanistic models of cell processes, but modelers can also work with a simpler formalism of influence systems to merely describe the positive and negative influences between molecular species, without fixing their implementation with biochemical reactions. In this section, we propose a syntax for influence systems with forces which allows us to define a hierarchy of differential, stochastic, discrete and positive boolean semantics, similarly to reaction systems. We then focus on different boolean semantics, and compare them to Thomas's setting for gene regulatory networks.

Syntax

The idea is to syntactically distinguish conjunctive from disjunctive conditions by writing influences with several sources for representing a conjunction of conditions, while the different influences on a same target express a disjunction of conditions. These syntactical conventions are a particular case of the concept of multiplexes introduced in [5] restricted here to disjunctive normal forms. Definition 5. Given S = {x 1 , . . . , x s } a set of species, an influence system I is a set of quintuples (P, N, t, σ, f ) called influences, where P ⊂ S is called the positive sources of the influence, N ⊂ S the negative sources, t ∈ S is the target, sign σ ∈ {+, -} is the sign of the influence, and f is a real-valued mathematical function of R s , called the force of the influence.

Influences of sign + will be called positive influences and those of sign -, negative influences. In addition, we distinguish the positive sources from the negative sources in an influence (positive or negative), in order to annotate the fact that in the differential semantics, the source increases or decreases the force of the influence, and in the boolean semantics with negation whether the source or the negation of the source is a condition for a change in the target.

For practical reasons we provide an ASCII syntax for influence systems which is used in Biocham4 v4: they will be written as sequences of lines, where each set is written as a comma-separated sequence of the corresponding species, where the sign is represented as an arrow separating sources from the target, -> for positive influences, and -< for negative influences, and where the positive and negative sources are separated by a / that can be omitted if there is no negative source.

Let us now define the concept of well-formed influence systems similarly to the above Def. 2 for reaction systems, with a particular condition for the target of a negative influence, as follows: Definition 6. An influence (P, N, t, σ, f ) over molecular species {x 1 , . . . , x s } is well formed if the following conditions hold:

1. f (x 1 , . . . , x s ) is a partially differentiable function, non-negative on R s + ;
2. x i ∈ P if and only if σ = + (resp. -) and ∂f /∂x i (x) > 0 (resp. < 0) for some value x ∈ R s + ; 3. x i ∈ N if and only if σ = + (resp. -) and ∂f /∂x i (x) < 0 (resp. > 0) for some value

x ∈ R s + ; 4. t ∈ P if σ = -.
An influence system is well formed if all its influences are well formed.

Hierarchy of Semantics

Given a set of species S = {x 1 , . . . , x s } and an influence system I over S, the differential semantics associates the following ODE system with I:

dx k dt = (Pi,Ni,x k ,+,fi)∈I f i - (Pj ,Nj ,x k ,-,fj )∈I f j
Intuitively, it adds up all the forces of the positive influences on x k and subtracts all forces of negative influences on x k in the derivative of x k over time. For instance, in Ex. 2, we get the same equations as for Ex. 1.

It is worth noticing that the negative sources in a well-formed influence decrease the force of the influence but do not disable it. Consequently, we define similarly the stochastic semantics of an influence system with forces, by a transition system, noted -→ S , between discrete states, i.e. vectors x of N s , with the condition that the positive sources are present in sufficient number, with a transition propensity defined by the force, and the target updated as follows:

∀(P i , N i , A i , σ i , f i ), x -→ fi S x with propensityf i if x ≥ P i , x = x σ i A i
Transition probabilities between discrete states are obtained through normalization of the propensities of all enabled transitions, and the time of next reaction can also be given à la Gillespie [START_REF] Gillespie | Exact stochastic simulation of coupled chemical reactions[END_REF]. In this interpretation, the negative sources are supposed to decrease the influence propensity but do not prevent the influence from proceeding. They are thus ignored here by the stochastic transition conditions.

The discrete (or Petri Net) semantics simply ignores the forces:

∀(P i , N i , A i , σ i , f i ), x -→ D x if x ≥ P i , x = x σ i A i
The positive boolean semantics is defined on boolean vectors x of B s , by the "zero, non-zero" abstraction of integers of the discrete semantics. Unlike reaction systems, this boolean semantics associates one transition with one influence:

∀(P i , N i , A i , σ i , f i ), x -→ B x if x ≥ P i , x = x σ i A i
This boolean semantics is positive in the sense that it ignores the negative sources of an influence and contains no negation in the influence enabling condition. In Ex. 2 we get the same boolean transitions as in Ex. 1, although in general one can expect to get more transitions (as shown below in Sec. 3.4).

With these definitions, one can obtain as in [START_REF] Fages | Abstract interpretation and types for systems biology[END_REF], a hierarchy of semantics related by simple abstraction relationships (Galois connections in the framework of abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]) which allows us to state, for instance, that if a behaviour is not possible in the positive boolean semantics, it is also not possible in the discrete or stochastic semantics for any forces.

Influence Graph of an Influence System

One can define the differential influence graph of an influence system as in Def. 3 for reaction systems, and get a similar equivalence result with the following Definition 7. The syntactical influence graph associated with an influence system M is the graph having for vertices the molecular species, and for edges the following set of positive and negative influences:

{A → + B | ∃(P i , N i , B, σ i , f i ) ∈ M , (A ∈ P i and σ i = +) or (A ∈ N i and σ i = -)} ∪{A → -B | ∃(P i , N i , B, σ i , f i ) ∈ M , (A ∈ P i and σ i = -)
or (A ∈ N i and σ i = +)} Proposition 1. For a well-formed influence system such that the syntactical influence graph contains no conflict, the syntactical and differential influence graphs are identical.

Proof.

Recall that ẋ B = (Pi,Ni,x B ,+,fi)∈I f i -(Pj ,Nj ,x B ,-,fj )∈I f j Hence ∂ ẋ B ∂x A = (Pi,Ni,x B ,+,fi)∈I ∂fi ∂x A -(Pj ,Nj ,x B ,-,fj )∈I ∂fj ∂x A
Since the SIG does not have any conflict, A → + B is in the SIG (a similar reasoning can be made for A → -B) iff

∂ ẋ B ∂x A = (Pi,Ni,x B ,+,fi)∈I,A∈Pi,A ∈Ni ∂fi ∂x A -(Pj ,Nj ,x B ,-,fj )∈I,A ∈Pj ,A∈Nj ∂fj ∂x A
Now, since the influence system is well formed, all terms of the left-hand sum are non-negative (A ∈ N i ) and strictly positive for some points x i and all terms of the right-hand sum are non-positive (A ∈ P j ) and strictly negative for some x j .

We have that A → + B in the SIG iff the above sum has at least one term, which is equivalent to the existence of some x in the state space where one of the terms above is non-null, and therefore ∂ ẋ B ∂x A > 0, i.e., A → + B is in the DIG.

Expressive Power Compared to Reaction Systems

Theorem 2. Any (well-formed) influence system with forces can be represented by a (well-formed) reaction system with kinetics, with the same boolean, discrete, stochastic and differential semantics.

Proof. Let us represent a positive influence f forP/N → t by a catalytic synthesis reaction f for P/N ⇒ P + t.

Similarly, let us represent a negative influence f for P/N -t, by an active degradation reaction f for P + t/N ⇒ P .

It is straightforward to verify that the boolean, discrete, stochastic as well as differential semantics recalled and defined above are the same.

Furthermore, the well-formedness condition is preserved. Indeed, this property only depends on the forces/kinetic expressions and on the reactants/inhibitors, which do not change through that transformation thanks to the condition that in well-formed influence systems. In addition, t ∈ P in the case of the negative influence.

This theorem shows that an influence system can be simulated by a reaction system for the different semantics. The converse does not hold for the boolean semantics, for instance. Indeed, let us consider boolean semantics of the reaction C ⇒ A + B (the kinetics is omitted). We have a transition from the state (A, B, C) = (0, 0, 1) to (1, 1, 0) which is obviously not possible in an influence system since only one variable can change in one transition. However, the converse holds for the differential semantics: Theorem 3. Under the differential semantics, (well-formed) influence and reaction systems have the same expressive power.

Proof. For each reaction (R, M, P, f ) of a given reaction system, let us add the following influences:

(Set(R), Set(M ), x i , +, (P (i) -R(i)) × f ) when P (i) -R(i) > 0 (Set(R), Set(M ), x i , -, (R(i) -P (i)) × f ) when P (i) -R(i) < 0
The associated ODE system collects all (P i -R i ) × f exactly as in the differential semantics of the original reaction system. Furthermore, it is easy to check that these influences are well formed since the original reaction is well formed and the force is only a positive integer multiplied by the original kinetic expression.

This theorem shows that as far as the differential semantics is concerned, the influence systems have the same expressive power as reaction systems and there is no theoretical reason to develop a reaction model. This does not mean that there is a canonical reaction system associated with an influence system. Generally, different implementations with reactions are possible without changing the differential semantics. They represent extra information that is irrelevant to the analysis or simulation of the differential equations, but could lead to different stochastic simulations, for instance.

Boolean Semantics with Negation

One can also consider a boolean semantics with negation for influence systems, where the negative sources are interpreted as negations in the enabling condition. Formally, the boolean with negation semantics of an influence system is then defined by the following transition system:

∀(P i , N i , A i , σ i , f i ), x -→ B x if x ≥ P i , x ∩ N i = ∅, x = x σ i A i
This interpretation allows us to represent more boolean transition semantics. Let us call a unitary transition system, a transition system that updates at most one variable of x in each transition. It is worth remarking that in this case, the state transition graph lives on a hypercube (e.g. Fig. 2 of Sec. 5).

Proposition 2. Any unitary boolean transition system can be represented by an influence system under the boolean semantics with negation.

Proof. It is sufficient to notice that since a unitary boolean transition s -→ BN s changes at most one species, say x i , from s to s , it can be represented by either a positive influence, (P, N, x i , +), if s (x i ) = 1, or a negative influence,

(P, N, x i , -), if s (x i ) = 0, with P = {x | s(x) = 1} and N = {x | s(x) = 0}.
Let us call a positive boolean transition system one that contains no negation in the conditions for enabling a transition, i.e. if a transition is enabled when s(x i ) = 0 then it is also enabled when s(x i ) = 1.

Corollary 1. Any unitary positive boolean transition system can be represented by an influence system under the positive boolean semantics.

Proof. In the influence system associated by Prop. 2 with a positive unitary transition system, any influence that has negative sources is doubled by a counterpart influence where such sources are positive (by definition of positive boolean transition system). Therefore, in the associated influence system, the negative sources can be simply ignored, as done by the positive boolean semantics.

Functional Boolean Semantics with Negation à la Thomas

The boolean semantics defined by René Thomas originally for gene networks [START_REF] Thomas | Biological Feedback[END_REF], is functional, in the sense that the next boolean state x is defined by a boolean function φ(x), not a relation. In this setting, the synchronous semantics is deterministic, and the non-deterministic asynchronous semantics is obtained by interleaving, by considering all the possible transitions that change the boolean value of exactly one of the genes at a time. A truly non-deterministic influence system such as {(A, ∅, B, +, f ), (A, ∅, B, -, g)}, for which the transition relation is not a function, cannot be represented. Thomas's setting excludes self-loops in the state transition graph and all steady states are stable (i.e. terminal states): Proposition 3. The boolean transition systems definable by Thomas's regulatory networks are the unitary boolean transition systems without self-loops.

Proof. A Thomas's transition graph is necessarily unitary and without self-loops since each transition changes the boolean value of exactly (not at most) one variable at a time. The converse follows from Prop. 2 by excluding the possibility of having self-loop transitions which change no variable. This restriction to transition functions is even more striking in Thomas's multilevel setting, where the above system can (in the discrete semantics) have transitions from (1, 1) both to (1, 0) and to (1,2). That would necessitate the corresponding logical parameter for B to be at the same time < 1 and > 1. It is worth noting that despite this restriction, the logical formalism of Thomas is successfully used in a wide variety of models [START_REF] Traynard | Logical model specification aided by model-checking techniques: application to the mammalian cell cycle regulation[END_REF][START_REF] Grieco | Integrative modelling of the influence of mapk network on cancer cell fate decision[END_REF][START_REF] Naldi | Diversity and plasticity of th cell types predicted from regulatory network modelling[END_REF][START_REF] González | Qualitative dynamical modelling of the formation of the anterior-posterior compartment boundary in the drosophila wing imaginal disc[END_REF] in systems biology.

Properties of the Positive Boolean Semantics

In this section, we focus on the positive boolean semantics of influence systems and study its properties. Recall that ≤ denotes the pointwise order on {0, 1} coordinates of vectors representing states.

Proposition 4 (Monotonicity). The positive boolean semantics of influence systems is monotonic: let I be an influence system over S = {x 1 , . . . , x s } and v 1 , v 2 be two boolean states, i.e., vectors of

B s if v 1 ≤ v 2 then ∀v 1 , v 1 -→ v 1 , ∃v 2 , v 1 ≤ v 2 and v 2 -→ v 2 v 1 v 2 v 1 v 2 ≤ ≤
Proof. One can simply notice that since there are no negations in the enabling conditions, any influence that is enabled in v 1 is also enabled in v 2 .

It is worth noticing that this monotonicity property for transitions is fundamentally different from that of monotone dynamical systems [3] which are deterministic, and therefore impose the monotonicity property on the unique image of v 1 and v 2 . In our setting, Prop. 4 states that there exists some v 2 ≥ v 1 , but the existence of negative influences in the system permits that some other images of v 2 might not be greater than v 1 . Nevertheless, we have Proposition 5 (Greatest element). Let C be a Terminal Strongly Connected Component (TSCC) of the state transition graph of a positive influence system, then C has a greatest element:

∃v 0 ∈ C, ∀v ∈ C, v ≤ v 0
Proof. Let us prove this proposition by contradiction: assume that there are two incomparable maximal elements v 1 and v 2 in C. Since C is strongly connected there is a path from v 1 to v 2 and along that path a state v 3 and its successor in the path v 4 such that v 3 ≤ v 1 and v 4 ≤ v 1 , as v 2 ≤ v 1 . Now, using Prop. 4 we get that v 1 -→ v 1 with v 4 ≤ v 1 and v 1 ∈ C since C is terminal. However v 1 is either greater or less than v 1 since it is the result of applying a single influence. If v 1 < v 1 we have a contradiction as we supposed v 1 maximal. If v 1 ≤ v 1 we get v 4 ≤ v 1 by transitivity and that is also contradictory.

Corollary 2. To enumerate the attractors, i.e., TSCCs, of a positive influence system, it is enough to check the strongly connected components (SCCs) of states that have no strictly increasing transition.

Proof. This is an immediate consequence of Prop. 5 as each TSCC can be represented by its greatest element which has no strictly increasing transition.

Notice that stable states are a particular case with no strictly decreasing transition either. Moreover, any strictly decreasing transition should be "reversible" for the SCC to be a TSCC. This allows us to rule out potential TSCC candidates without exploring their whole SCC in Alg. Iteratively solve by SAT/CP the CSP defined by Constraints return The set of solutions end function Proposition 6. Given an influence system, there is at least one TSCC of the original influence system in each TSCC of its positive semantics.

Proof. The positive semantics only adds transitions by enabling more influences, it can therefore only merge TSCCs. This result suggests finding complex attractors of non-positive systems, such as logical models à la Thomas [START_REF] Remy | Graphic requirements for multistability and attractive cycles in a boolean dynamical framework[END_REF][START_REF] Ruet | Local cycles and dynamical properties of boolean networks[END_REF], by enumerating the greatest elements of the TSCCs of their positive boolean semantics, and then looking for attractors of the original system. This approach provides an over-approximation of the attractors and is complementary to recent works which provide lower-bounds on their number [START_REF] Klarner | Computing symbolic steady states of boolean networks[END_REF].

Our algorithm shows that there is in each case a single complex attractor (i.e. not marked as stable or not terminal), accordingly to [1], and four stable steady states in the first case. Note that in [2], this influence model was further extended with differential and stochastic dynamics which could be represented in our setting by influence forces.

Influence Model of the Mammalian Circadian Clock [9]

A good example of the use of logical models à la Thomas is the recent paper by Comet et al. [START_REF] Comet | Simplified models for the mammalian circadian clock[END_REF] studying different variants of small models of the circadian rhythms in mammals. A direct import in Biocham v4 of the logical model of Section 5 of [START_REF] Comet | Simplified models for the mammalian circadian clock[END_REF] gives the following influence system with negative sources:

_ / L -> L . L -< L . _ / G , PC -> G . G , PC -< G . G / PC , L -> PC . PC / G -< PC . PC , L -< PC .
The positive semantics of this system is close to the original boolean semantics with negation à la Thomas of the model. They both have a single TSCC: the vector (1, 1, 1) that is found by the command list_tscc_candidates as sole candidate. Furthermore, only a few state transitions become reversible in the positive boolean semantics, while they are irreversible in the original boolean semantics with negation à la Thomas of the model, as depicted in Fig. 2. The approximation introduced by the positive boolean semantics can be explained by quantitative dynamics considerations. For instance, when G is on, the transcription leading to the PER-CRY complexes is stimulated, however [START_REF] Comet | Simplified models for the mammalian circadian clock[END_REF] explains that these complexes can only migrate to the nucleus in absence of light. This absence cannot be checked in a positive semantics model, however the consensus mechanistic process is rather thought to be a modulation of PER transcription by light (see for instance [START_REF] Leloup | Toward a detailed computational model for the mammalian circadian clock[END_REF] for the mammalian case). Being purely quantitative, it is not easy to take into account such a regulation in a boolean model except with the reversible activation of P C when G is on, whether L is on or not. This is what happens in our positive model as can be seen in the right panel of Fig. 2, and it is similar to what happens for the light in the original model.

The same reasoning explains the reversible inactivation of G when P C is active. Indeed there is a basal synthesis of G that cannot check, in a positive setting, that P C is inactive in order to activate the genes. Once again, the mechanistic process is a quantitative inhibition of the CLOCK-BMAL1 complexes by PER-CRY and a conservative boolean approximation of that process is reflected by the reversible activation of G in presence of P C.

In [START_REF] Comet | Simplified models for the mammalian circadian clock[END_REF], the authors also restrict the possible behaviours by introducing delays for the boolean transitions which could be considered as a further expansion of the formalism.

Discussion

In this paper, we hope to have clarified some differences between influence systems and reaction systems, and especially some subtle discrepancies between the precise boolean semantics that have been considered in the literature. As far as the modeling of one biological system is concerned, the modeler can work with one formalism and one tool to answer the questions about their model. Nevertheless, as soon as different modeling tools are to be used, or the model has to be communicated and reused for another purpose, understanding and mastering these discrepancies in the semantics of the interactions becomes crucial.

We have shown that, for influence systems and reaction systems with inhibitors, one can obtain a hierarchy of semantics which goes from the concrete stochastic semantics to a discrete Petri net, and then a positive boolean semantics in which the inhibitors of the reactions or influences are just ignored. This is consistent with the fact that the inhibitors decrease the rate or force in the quantitative semantics, but do not really prevent the reaction or influence from proceeding. This convention thus ensures that all discrete behaviours are approximated when we go up in the abstractions of the hierarchy of semantics, and that if a behaviour is not possible in the positive boolean semantics (which can be checked by model-checking methods for instance) it is not possible in the stochastic semantics for any forces. Furthermore, we have shown that in the positive boolean semantics, the monotonicity of the transition relation allows us to enumerate the complex attractors more efficiently by restricting the search to the greatest elements candidates.

On the other hand, the boolean semantics à la Thomas of influence systems, interprets inhibitors as negations, and contains a restriction on the definition of the transition relation by a function, not a relation, which limits the sources of non-determinism. We have shown that the boolean semantics with negation leads to a more expressive formalism in which any unitary boolean transition system can be encoded, but does not correspond to an abstraction of the stochastic semantics, unless the stochastic transitions interprets inhibitors as negative conditions which does not correspond to the differential semantics. With the functional restriction, we have proven that each TSCC in the positive semantics contains at least one TSCC of the semantics à la Thomas, and thus that our algorithm can be used to prune the search space in this setting also.

We have also shown that reaction systems and influence systems have the same expressive power under the differential semantics. This means that, as far as the differential equations are concerned, the details given in the reactant-product structure of a reaction system are not necessary, and that the same differential equations can be derived from an influence system with forces. Several reaction systems can be associated with an influence system with the same differential semantics. This leaves open the design of canonical forms for reaction systems, and computer tools for automatically maintaining the implementation of an influence system by a reaction system.

  k1 * A * B for A + B = >2* B . k2 * A for A = >2* A . k3 * B for B = > _ .

Example 2 .

 2 The prey-predator model of Lotka-Volterra of Ex. 1 can also be represented by the following well-formed influence system k1 * A * B for A , B -< A . k1 * A * B for A , B -> B . k2 * A for A -> A . k3 * B for B -< B . composed of four influences with positive sources only, ({A, B}, ∅, A, -, k1 * A * B), ({A, B}, ∅, B, +, k1 * A * B), ({A}, ∅, A, +, k2 * A) and ({B}, ∅, B, -, k3 * B).

Fig. 2 .

 2 Fig. 2. State transition graphs of the model under, Left: the boolean semantics with negation à la Thomas, similar to Fig. 7 of [9], Right: the positive boolean semantics, where some state transitions have become reversible.

  1 (implementation available in Biocham v4). Algorithm 1 TSCC maximal elements candidates enumeration algorithm procedure list_tscc_candidates Constraints ← {P ∧ ¬N =⇒ t | (P, N, +, t, f ) ∈ I} Enabled positive influences must not change the state Candidates ←EnumerateSolutions(Constraints) for C ∈ Candidates do if C has no strictly decreasing transition then C is a stable steady state else if C has a non-reversible strictly decreasing transition then

	C is not in a TSCC
	else
	C's SCC must be explored to check if it is a TSCC
	end if
	end for
	end procedure
	function EnumerateSolutions(Constraints)

http://lifeware.inria.fr/biocham

Acknowledgements. We are grateful to Paul Ruet for interesting discussions on Thomas's framework, and to the reviewers for their comments. This work was partially supported by ANR project Hyclock under contract ANR-14-CE09-0011, and PASPA-DGAPA-UNAM, Conacyt grants 221341 and 261225.

5.1 Influence Model of p53/Mdm2 DNA Damage Repair System [1] The p53/Mdm2 DNA damage repair system is an interesting oscillatory system which has been first modeled in [8] by a reaction system with differential equations, and then in [1] and [2] by simplified influence systems with discrete and differential semantics respectively.

We illustrate here the search for TSCCs with two versions of the influence model of [1]. In the first model, we simply transcribe the graph of Fig. 4 of the authors as a boolean influence system. We therefore ignore the multi-level aspect they developed. In the second model, we add some activations on p53 and DNAdamage, and an inhibition on cytoplasmic Mdm2, in order to take into account some basal state of the model. The influence systems and the computed TSCCs are listed in the Biocham session depicted in Fig. 1.


Keywords: DSL, network protocols, mutation analysis

Une approche langage pour améliorer la robustesse de l'implémentation de protocoles réseaux applicatifs

Résumé : Pour être sûr et robuste, le fonctionnement d'un réseau doit reposer sur des implémentations d'applications sans faille. Les protocoles réseau étant de plus en plus complexes, écrire manuellement le code qui prend en charge leurs messages devient de plus en plus difficile et sujet à erreurs. Dans ce papier, nous présent un langage métier, Zebu, pour décrire le format des messages d'un protocole réseau et les contraintes de traitement associées. D'une spécification Zebu, un compilateur génère automatiquement des talons à utiliser par une application pour l'analyze grammaticale de messages réseau. Zebu is simple d'usage, utilisant les mêmes notations que celles utilisées dans les RFCs pour décrire les grammaires de protocoles. Zebu est efficace, l'implantation mémoire étant calquée sur les besoins de l'application et les fragments du message pouvant être traités à la demande. Enfin, les applications basées sur Zebu sont robustes, le compilateur vérifiant la consistence de la spécification et les talons générés étant incluant la validation de la structure du message. En utilisant une analyze de mutation dans le contexte de SIP et RTSP, nous montrons que Zebu améliore de manière significative la robustesse des applications.

Introduction

In the Internet era, many applications, ranging from instant messaging clients and multimedia players to HTTP servers and proxies, involve processing network protocol messages. A key part of this processing is to parse messages as they are received from the network. As message parsing represents the front line of interaction between the application and the outside world, the correctness of the parser is critical; any bugs can leave the application open to attack [START_REF] Qie | Defensive programming: Using an annotation toolkit to build DoSresistant software[END_REF]. In the context of in-network application such as proxies, where achieving high throughput is essential, parsing must also be efficient.

Implementing a correct and efficient network protocol message parser, however, is a difficult task. The syntax of network protocol messages is typically specified in a RFC (Request for Comments) using a variant of BNF known as ABNF (Augmented BNF ) [START_REF] Crocker | Augmented BNF for Syntax Specifications: ABNF[END_REF]. Such a specification amounts to a state machine, which for efficiency is often implemented in an unstructured way using gotos. The resulting code is thus error-prone and difficult to maintain. Furthermore, some kinds of message processing may not use all fragments of the message. For example, a router normally only uses the header fields that describe the message destination, and ignores the header fields that describe properties of the message body [START_REF] Pelinescu-Onciul | SIP express router (SER)[END_REF]. It is thus desirable, for efficiency, to defer the parsing of certain message fragments to when their values are actually used. In this case, complex parsing code may end up scattered throughout the application.

In the programming languages community, parsers have long been constructed using automated parser generators such as yacc [START_REF] Johnson | Yacc: Yet another compiler compiler[END_REF]. Nevertheless, such tools are not suitable for generating parsers for network protocol messages, as the grammars provided in RFCs are often not context free, and such tools provide no support for deferring the parsing of some message fragments. Thus, parsers for network protocol messages have traditionally been implemented by hand. This situation, however, is becoming increasingly impractical, given the variety and complexity of protocols that are continually being developed. For example, the Gaim instant messaging client parses more than 10 different instant messaging protocols [START_REF]Gaim 1.5.0: A multi-protocol instant messaging (IM) client[END_REF]. The message grammar in the IMAP RFC is about 500 lines of ABNF, and includes external references to others RFCs. SIP (Session Initiation Protocol) [START_REF] Rosenberg | SIP: Session Initiation Protocol[END_REF], which is mainly used in telephony over IP, has a multitude of variants and extensions, implying that SIP parsers must be tolerant of minor variations in the message structure and be extensible. Incorrect or inefficient parsing makes the application vulnerable to denial of service attacks, as illustrated by the "leading slash" vulnerability found in the Flash HTTP Web server [START_REF] Qie | Defensive programming: Using an annotation toolkit to build DoSresistant software[END_REF]. In our experiments (Section 4), we have crashed the widely used SER parser [START_REF] Pelinescu-Onciul | SIP express router (SER)[END_REF] for SIP via a stream of 2416 incorrect messages, sent within 17 seconds.

To address the growing complexity of network protocol messages and the inadequacy of standard tools, some parser generators have recently been developed that specifically target the kinds of complex data layouts found in network protocol messages. These tools include DATASCRIPT [START_REF] Back | DataScript -a specification and scripting language for binary data[END_REF] and PacketTypes [START_REF] Mccann | Packet types: Abstract specifications of network protocol messages[END_REF] for binary protocols, and PADS [START_REF] Fisher | PADS: a domain-specific language for processing ad hoc data[END_REF], GAPA [START_REF] Borisov | A generic application-level protocol analyzer and its language[END_REF] and binpac [START_REF] Pang | binpac: a yacc for writing application protocol parsers[END_REF] for both binary and text-based protocols. However, none of these approaches accepts ABNF as the input language, and thus, the RFC specification must be translated to another formalism, which is tedious and error prone. Furthermore, such approaches have mainly targeted application protocol analyzers, which parse a fixed portion of the message and then proceed to some analysis phase. Thus, they do not provide fine-grained control over the time when parsing occurs. While these approaches relieve some of the burden of implementing a network protocol message parser, there still remains a gap between these tools and the needs of applications.

We propose to directly address the issues of correctness and efficiency at the parser generator level. To this end, we present a domain-specific language, Zebu, for describing HTTP-like text-based protocol message formats and related processing constraints. Zebu is an extension of ABNF, implying that the programmer can simply copy a network protocol message grammar from an RFC to begin developing a parser. Zebu extends ABNF with annotations indicating which message fields should be stored in data structures, and other semantic information, such as the type of the value expressed by a field, constraints on the range of its value, and whether certain fields are mandatory or optional. Fields can additionally be declared as lazy, which gives control over the time when the parsing of a field occurs. A Zebu specification is then processed by a compiler that generates stubs to be used by an application to process network messages. Based on the annotations, the Zebu compiler implements domain-specific optimizations to reduce the memory usage of a Zebu based application. Besides efficiency, Zebu also addresses robustness, as the compiler performs many consistency checks, and generates parsing stubs that validate the message structure.

This paper

In this paper, we present the Zebu language and an assessment of its performance and robustness in the context of the SIP and RTSP (Real Time Streaming Protocol [START_REF]Real time streaming protocol information and updates[END_REF]) network protocols. Our contributions are as follows:

We introduce a declarative language, named Zebu, for describing protocol message formats and related processing constraints. Zebu builds on the ABNF notation typically used in RFCs to describe protocol grammars.

We have defined a test methodology based on a mutation analysis for evaluating the robustness improvement induced by Zebu.

We have applied our test methodology existing and Zebu-based SIP and RTSP parsers. While the Zebubased parsers reject 100% of the invalid mutated messages, none of the existing parsers that we have tested detects more than about 25% of the injected mutants.

Finally, we show that the added safety and robustness provided by Zebu does not significantly impact performance. Indeed, our performance evaluation shows that a Zebu-based parser can be as efficient on average as a hand-crafted one.

The rest of this paper is organized as follows. Section 2 discusses specific characteristics of network protocol message parsing code, illustrating its inherent complexity. Section 3 introduces the Zebu language, and describes the verification of specifications and the generation of parsing stub functions. Section 4 assesses the robustness and performance of Zebu-based parsers. Section 5 described related work and Section 6 concludes.

Issues in developing network protocol parsers

To illustrate the growing complexity of network protocol messages and the inadequacy of existing approaches to creating the associated parsers, we consider the SIP protocol [START_REF] Rosenberg | SIP: Session Initiation Protocol[END_REF]. The SIP message syntax is similar to that of other recent text-based protocols such as HTTP and RTSP. A SIP message begins with a line indicating whether the message is a request (including a protocol method name) or a response (including a return code). A sequence of required and optional headers then follows. Finally, a SIP message can include a body containing the payload. Widely used SIP parsers include that of the SIP Express Router (SER) [START_REF] Pelinescu-Onciul | SIP express router (SER)[END_REF] and the oSIP library [START_REF] Moizard | The GNU oSIP library[END_REF] used e.g., in the open PBX Asterisk [START_REF] Spencer | Asterisk: The open source PBX[END_REF]. Both parsers are hand-written. We first present an extract of the ABNF specification of the SIP message grammar, and then describe the difficulty of hand-writing the corresponding parser. We next consider to what extent these difficulties are addressed by existing parser generation tools, and describe the issues involved in integrating a parser with a network application.

ABNF formalism

An extract of the ABNF specification of the SIP message grammar is shown in Figure 1. Lines 1 to 8 define the structure of a request line, which appears at the beginning of a message, and lines 10 to 13 define the structure of the CSeq header field, which is used to identify the collection of messages making up a single transaction.

An ABNF specification consists of a set of derivation rules, each defining a set of alternatives, separated by /. An alternative is a sequence of terminals and nonterminals. Among the terminals, a quoted string is case insensitive. Case sensitive strings must be specified as an explicit sequence of character codes, as in the INVITEm rule (line 5). ABNF includes a general form of repetition, n*m X, that indicates that at least n and at most m occurrences of the terminal or nonterminal X must be present. ABNF also defines shorthands such as n* for n*∞, *n for 0*n, * for 0*∞ and n for n*n. Therefore, 1*DIGIT in the CSeq rule (line 10) represents a sequence of digits of length at least 1. Brackets are used as a shorthand for 0*1.

Hand-writing parsers

The specification of the CSeq header in Figure 1 amounts to only four lines of ABNF. However, implementing parsing based on such an ABNF specification efficiently in a general-purpose language such as C or C++ often requires many lines of code. For example, SER and oSIP contain about 200 and 340 lines of C and C++ code, respectively, specifically for parsing the CSeq header. This CSeq-specific code includes operations for reading individual characters from the message, operations for transitioning in a state machine according to the characters that are read, calls to various generic header parsing operations, and error checking code. Among the complexities encountered is the fact that, as shown in Figure 1, a CSeq header value can stretch over multiple lines if the continuation line begins with a space or horizontal tab (WSP).

In addition to the constraints described by the ABNF specification, the parser developer has to take into account constraints on the message structure that are informally specified in the text of the RFC. For example, the CSeq header includes a CSeq number expressed as any sequence of at least one digit (1*DIGIT) and a CSeq method (Method). The SIP RFC states that the CSeq number must be an unsigned integer that is less than 2 31 and that the CSeq method must be the same as the method specified in the request line. However, existing hand-written implementations do not always check all these requirements. For example, oSIP converts the CSeq number to an integer without performing any verification. If the CSeq number contains any non-numeric characters, the result is a meaningless value.

Using parser generators

PADS and binpac use a type-declaration like format for specifying message grammars, while GAPA uses a BNF-like format. Both of these formats require reorganizing the information in the ABNF specification. We take PADS as a concrete example. Figure 2 shows a PADS specification corresponding to the four lines of ABNF describing the CSeq header. This specification is in the spirit of the HTTP specification provided by the PADS developers [START_REF]PADS distribution[END_REF].

A PADS specification describes both the grammar and the data structures that will contain the result of parsing the message. Thus, the rules of the ABNF specification are translated into what amount to structure declarations in PADS. As a PADS structure must be declared before it is used, the rule ordering is often forced to be different than that of the ABNF specification. For example, in the ABNF specification, the CSeq nonterminal is defined before the LWS, SWS, and HCOLON nonterminals, while in the PADS specification, the structure corresponding to the CSeq nonterminal is defined afterwards (line 26). PADS also does not implement the same default parsing strategies as ABNF, and thus e.g., case insensitive strings must be specified explicitly using regular expressions (line 27). Similarly, translating SIP whitespace into PADS requires writing many lines of specifications (lines 8-19), including regular expressions. Finally, the PADS specification must express the various constraints contained in the RFC text. Although PADS allows the developer to define constrained types (lines 5 to 6), which are used here in the case of the CSeq number (line 29), non-type constraints such as the relationship between the method mentioned in the request line and the method mentioned in the CSeq header must be implemented by arbitrary C code (lines 1 to 2 and line 37). Of these issues, probably the most difficult for the programmer is to convert ABNF specifications to regular expressions. Regular expressions for even simple ABNF specifications are often complex and voluminous. For example, a regular expression for a URI has been published that is 45 lines of code [START_REF] Akira | Converter from ABNF to regexp[END_REF]. While a tool has been developed to convert an ABNF specification to a regular expression [START_REF] Akira | Converter from ABNF to regexp[END_REF], in the PADS, GAPA, and binpac specifications that we have seen, the regular expressions appear to have been written by hand, and sometimes do not capture all of the constraints specified by the RFC.

Integrating a parser with an application

The ease of integrating a parser with an application depends on whether the parser parses the fields needed by the application, and whether the result of this parsing is stored in appropriate data structures. We consider the issues that arise when using the handwritten oSIP and SER parsers, and when using a parser generated by a tool such as PADS. oSIP parses the fixed set of required SIP header fields, and separates the rest of the message into pairs of a header field name and the corresponding raw unparsed data. Applications that do not use all of the information in the required header fields incur the time cost of parsing this information and the space cost of storing the result (see Section 4). Applications that use the many SIP extensions must parse these header fields themselves. The former increases the application time and space requirements, which can be critical in the case of in-network applications such as proxies, while the latter leaves the application developer on his own to develop complex parsing code.

SER provides more fine-grained parsing than oSIP, as it parses only those header fields that are requested by the application. By default, however, SER only gives direct access to the top-level subfields of a header, such as the complete URI. To extract, e.g., only the host portion of a URI, the programmer must intervene. One approach is for an application built using SER to reparse the subfield, to obtain the desired information. SER applications are written using a domain-specific language targeted towards routing, which does not provide string-matching facilities. Nevertheless, SER provides an escape from this language, allowing a SER application to invoke an arbitrary shell script. A SER application can thus invoke a script written in a language such as Perl to extract the desired information. This approach, however, incurs a high performance penalty for forking a new process, as we show in Section 4, and compromises the safety benefits of using the SER language. Another approach is to use the SER extension framework, which, à la Apache [START_REF]HTTP server project[END_REF], allows integrating new modules into the parsing process. Although efficient, this approach requires the programmer to write low level C code that conforms to rather contorted requirements. Again, incorrect behavior inside a module may compromise the robustness of the whole application.

Finally, parser generators such as PADS allow the developer to construct the parser such that it parses only as much of the message as is needed. However, the generated data structures directly follow the specified parsing rules, implying that accessing message fields often requires long chains of structure field references. Furthermore, all of the parsed data is stored, which increases the memory footprint.

Robust Parser Development with Zebu

We now present the Zebu language for describing HTTP-like text-based protocol message formats and related processing constraints. Zebu is based on ABNF, as found in RFCs, and extends it with annotations indicating which message fields should be stored in data structures and other semantic attributes. These annotations express both constraints derived from the protocol RFC and constraints that are specific to the target application. From a Zebu specification, a compiler automatically generates stubs to be used by the application to process network messages.

The features of Zebu are driven by the kinds of information that an application may want to extract from a network protocol message. We first consider the features that are needed to do this processing robustly and efficiently, and then present the corresponding annotations that the programmer must add to the ABNF specification so that the Zebu compiler can generate the appropriate stub functions. Finally, we describe the Zebu compiler, which performs both verification and code generation, and the process of constructing an application with Zebu.

Issues

A HTTP-like text-based network message consists of a command line, a collection of header fields, and a message body. The command line indicates whether the message is a request or a response, and identifies basic information such as the version of the protocol and the method of a request message. A header field specifies a protocol-specific key and an associated value, which may be composed of a number of subfields. Finally, the message body consists of free text whose structure is typically not specified by the protocol. Thus, decomposing it further falls out of the scope of Zebu.

From the contents of a message, an application may need to determine whether the message is a request or a response, to detect the presence of a particular header field, or to extract command line or header field subfields. Each of these operations involves retrieving a command line or header field, and potentially accessing its contents. In a HTTP-like text-based protocol, each command line or header field normally occupies one or more complete lines, where each line after the first begins with a special continuation character. Thus, as exemplified by the very efficient SIP parser SER, a parser can be constructed in two levels: a top-level parser that simply scans each line of the message until it reaches the desired command line or header field, and a collection of dedicated parsers that process each type of command line or header field. The dedicated parsers must respect both the ABNF specification and any constraints specified informally in the RFC. To avoid reparsing already parsed message elements for each requested parsing operation, the parser should save all parsed data in data structures for later use, ideally in the format desired by the application.

This analysis suggests that to enable the Zebu compiler to generate a useful and efficient parser, the programmer must annotate the ABNF specification obtained from an RFC with the following information: (1) An (2) A specification of any constraints on the message structure that are informally described by the RFC. (3) An indication of the message subfields that will be used by the application. The first two kinds of annotations are generic to the protocol, and can thus be reused in generating parsers for multiple applications.

The third kind of annotation is application-specific. This kind of annotation can be viewed as a simplified form of the action that can be specified when using yacc and other similar parser generators, in that it allows the programmer to customize the memory layout used by the parser to the specific needs of the application.

Annotating an ABNF specification

We present the three kinds of annotations required by Zebu, using as an example an extract of the Zebu specification of a SIP parser, as shown in Figure 3.

Parser entry points

The Zebu programmer annotates the rule for parsing the command line of a request message with requestLine, the rule for parsing the command line of a response message with statusLine, and the rules for parsing each kind of header with header. Because a command line or header field cannot contain another command line or header field, the nonterminals for these lines are no longer useful. In the case of a command line, the nonterminal is simply dropped. Thus, for example, the ABNF rule for the Request-Line nonterminal (Figure 1, line 1) is transformed into the following Zebu rule (c.f., Figure 3, line 4):

requestLine = Method SP Request-URI SP SIP-Version
In the case of a header field, the description of the key is moved from the right-hand side of the rule to the left, where it replaces the nonterminal, resulting in a rule whose structure is suggestive of a key-value pair. For example, the ABNF CSeq rule on line 10 of Figure 1 is reorganized into the following Zebu rule (c.f., Figure 3, line 38)

header CSeq = 1*DIGIT LWS Method
(The delimiter HCOLON is also dropped, as it is a constant of the protocol). Some header fields, such as the SIP To header field, can be represented by any of a set of keys. In this case, the header is given a name, which is followed by the ABNF specification of the possible variants, in braces, as shown in line 44 of Figure 3. As in ABNF, the matching of the header key, and any other string specified by a Zebu grammar, is case insensitive.

RFC constraints

The text of the RFC for a protocol typically indicates how often certain header fields may appear, whether header fields can be modified, and various constraints on the values of the header subfields.

The Zebu programmer must annotate the corresponding ABNF rules with these constraints. Constraints are specified in braces at the end of a grammar rule. Possible atomic constraints are that a header field is mandatory (mandatory) and that a header field can appear more than once in a message (multiple). For example, in the SIP specification, the header To is specified to be mandatory and read-only (line 44). More complex constraints can be expressed using C-like boolean expressions. For example, in Section 2.2, we noted that in a request message, the method mentioned in the command line must be the same as the method mentioned in the CSeq header. This constraint is described in line 7. Some constraints on header fields are specific to either request or response messages. Accordingly, the Zebu programmer must group the request line and its associated constraints in a request block, and the status line and its associated constraints in a response block. In the case of SIP, the request block (lines 2-12) indicates that for the CSeq header the method must be the same as the method in the request line (line 7), and that the Max-Forwards header is mandatory (line 10). The constraints in the response block (lines 14-18) have been elided.

Subfields used by the application

The parsing functions generated by the Zebu compiler create a data structure for each command line or header field that is parsed. By default, this data structure contains only the type of the command line or header field and a pointer to its starting point in the message text. When the application will use a certain subfield of the command line or message header, the Zebu programmer can annotate the nonterminal deriving this subfield with an identifier name. This annotation causes the Zebu compiler to create a corresponding entry in the enclosing command line or header field data structure. For example, in line 4, the Zebu programmer has indicated that the application needs to use the method in the command line, which is given the name method, and the URI, which is given the name uri.

By default, a subfield is just represented as a pointer to the start of its value in the message text. This is the case of method and uri in our example. Often, however, the application will need to use the value in some other form, such as an integer. The Zebu programmer can additionally specify a type for a named value, either at the nonterminal reference or at its definition. For example, in line 38 the CSeq number is specified as being a uint32. Nonterminals can also be specified as structures (struct), unions (union), and enumerations (enum). A structure collects all derived named subfields. As illustrated in the case of Request-URI (line 25), a structure may even be used in the case of an alternation, when the application does not need to know from what element of the alternation a named entry is derived. A union, in contrast, records which alternation was matched and in each case only includes subfields derived from the given alternation. Finally, an enumeration is a special case of union in which the only information that is recorded is the identity of the matching alternation; the matched data is not stored. In line 20, for example, Method is specified as being an enumeration, because the application only needs to know whether the method of the message is one of the standard ones or an extension method, but does not need to know the identity of the extension method in the latter case.

An application may use the information in certain subfields only in some exceptional cases. The Zebu constraint lazy allows the programmer to specify that a specific subfield should not be parsed until requested by the application. For example, in the SIP specification, Request-URI has this annotation (line 25).

The Zebu compiler

The Zebu compiler verifies the consistency of the ABNF specification and the annotations added by the programmer, and then generates stub functions allowing an application to parse the command line and header A run-time environment defining various utility functions is also provided, and amounts to around 700 lines of C code.

Verifications Although RFCs are widely published and form the de facto standard for many protocols, we have found some errors in RFC ABNF specifications. These are simple errors, such as typographical errors, but still they complicate the process of translating an ABNF specification into code, whether done by hand or using a parser generator. The Zebu compiler thus checks basic consistency properties of the ABNF specification: that there is no omission (i.e., each referenced rule is defined), that there is no double definition, and that there are no cycles. Additionally, the annotations provided by the Zebu programmer must be consistent with the ABNF specification. For example, in line 30, the nonterminal Global-Failure is annotated with uint16. This non-terminal is specified to be an alternation of strings, and thus the Zebu compiler checks that each element of this alternation represents an unsigned integer that is less than 2 16 .

Code generation An application does not use the data structures declared in a Zebu specification directly, but instead uses stub functions generated by the Zebu compiler. The use of stub functions allows parsing to be carried out lazily, so that only as much data is parsed as is needed to fulfill the request of a given stub function call. As illustrated in Figure 4a, stub functions are generated for determining the type of a message (request or response), for parsing the command line and the various headers, for accessing individual header subfields, and for managing the parsing of subfields designated as lazy. The names of these stub functions depend on the specific structure of the grammar, but follow a well-defined schema that facilitates their use by the application developer.

The parsing functions generated by the Zebu compiler use the two-level parsing strategy described in Section 3.1. Header-specific parsers use the PCRE [START_REF] Hazel | PCRE -perl compatible regular expressions[END_REF] library for matching the regular expression of a header value that has been derived from the ABNF specification. The parsing functions contain run-time assertions that check the constraints specified in the RFC. Once a header is parsed and checked, its named subfields, if any, are converted to the specified types and stored in the data structure associated with the header. The values of the named subfields can then be accessed using the "get" stub functions.

Developing an application with Zebu

The developer defines the application logic as an ordinary C program, using the stub functions to access information about the message content. Figure 4b illustrates the implementation of an application that extracts the host information from the URI stored in the From header field of an INVITE message. This kind of operation is useful in, e.g. an intrusion detection system, which searches for certain patterns of information in network messages.

The application uses the stubs generated from the SIP message grammar specification to access the required information. The application initially uses the functions sip3261_Method_getType and sip3261_-RequestLine_getMethod to determine whether the current message is an INVITE request (line 6). If so, it uses the function sip3261_parse_headers to parse the From header field (line 8), and then the functions sip3261_-header_From_getUri and sip3261_get_header_From to extract the URI (line 9). Line 46 of the Zebu SIP specification indicates that the parsing of the URI should be lazy, so the function sip3261_Lazy_Addr_spec_-getParsed is used to force the parsing of this subfield (line 10). After a check that the host name is present (line 13), its value is extracted using the function sip3261_Option_Str_getVal in line 14.

Overall, due to the annotations in the Zebu specification, stub functions are available to access exactly the message fragments needed by the application. Similarly, memory usage is limited to the application's declared needs.

Experiments

A robust network application must accept valid messages, to provide continuous service, and reject invalid network messages, to avoid corrupting its internal state. As the parser is the front-line in the treatment of network messages, it has a key role to play in providing this robustness. In this section, we evaluate the robustness improvement offered by Zebu, by comparing the reaction of Zebu-based parsers and a variety of existing parsers to valid and invalid network messages. Our experiments are based on a mutation analysis technique.

For SIP, we compare with the oSIP and SER parsers previously described in Section 2. For RTSP, we use the parser in the widely used VLC media player and streaming server [START_REF]The videolan project[END_REF], and the parser provided by the LiveMedia library1 . Figure 5 shows the sizes of the ABNF and Zebu specifications of the message grammars for SIP and RTSP. The Zebu specification is longer, because it includes rules that are mentioned only by reference to another RFC in the original SIP and RTSP specifications. Figure 5 In the rest of this section, we first introduce mutation analysis, and then compare the robustness of existing SIP and RTSP parsers with that of the corresponding Zebu-based parsers. Finally, we evaluate the performance of Zebu, showing that Zebu-based parsers are often as efficient as hand-written ones.

Robustness evaluation

Mutation analysis is a fault-based testing technique for unit-level testing [START_REF] Demillo | Hints on test data selection: help for the practicing programmer[END_REF]. Traditional mutation testing involves introducing small changes, i.e., mutations, in program source code, to determine whether a given test suite is sufficient to distinguish between correct and incorrect programs. In our case, however, we are interested in assessing the robustness of the program, i.e., the parser, and thus we introduce mutations into the test data, i.e., the network messages, rather than into the program source code. We use mutation rules both to generate invalid messages and to generate valid messages that have properties that are known to be challenging for network protocol message parsers. A robust parser should reject the invalid messages and accept the valid ones.

To generate invalid messages, we have defined a set of mutation rules for messages based on ABNF structure:

Mutations on the characters set. Message literals are derived from a fixed set of possible characters. The first, middle, or last character of a message literal is replaced with any character outside the valid set.

Mutations on repetitions. As described in Section 2.1, ABNF offers a generic mechanism of repetition.

Mutants are chosen to describe an invalid number of repetitions.

Mutations based on constraints. Protocol specifications include additional constraints not specified in the message grammar about the values of header subfields. For example, the response code of a SIP response is not only an unsigned integer of three digits, but its value must also be less than 699 (see Figure 3). Mutants are chosen that violate these constraints.

To generate valid but problematic messages, we have extended our character set mutation rule to create messages of the form suggested by the SIP Torture Test Message RFC [START_REF] Sparks | Session initiation protocol (SIP) torture test messages[END_REF]. This RFC describes a set of valid SIP messages that test corner cases in SIP implementations.

To compare the robustness of Zebu-based applications to applications based on hand-crafted parsers, we consider the parsing of the principal fields of a network protocol message. For SIP, these fields are the command line and the six mandatory header fields, while for RTSP they are the command line and the header fields Transport, CSeq and UserAgent. We drive each of the parsers listed in Figure 5 using minimal applications that request access to these fields. The Zebu-based applications log-Zebu-SIP and log-Zebu-RTSP, for SIP and RTSP respectively, consist of a few lines of C code that log statistical information about incoming messages. These applications use the stubs generated by the Zebu compiler to access network messages, analogous to the code illustrated in Figure 4b. The SER application, log-SER is written using the SER configuration language to access the information in the various fields. The other applications, log-oSIP using oSIP, log-VLC using VLC, and log-LiveMedia using LiveMedia, are written in C using the appropriate API functions provided by the given parser.

Invalid messages In our first set of tests, we apply our mutation rules to SIP and RTSP messages, generating a stream of invalid messages, which we then send to each of the SIP and RTSP applications, respectively. As shown in Figure 6, while the Zebu-based applications detect every mutant as representing an invalid message, none of the hand-crafted parsers detects more than about 25% of the injected mutants. This situation may have a critical impact. In the case of SIP for example, we have crashed SER via a stream of 2416 incorrect messages, sent within of 17 seconds. Because SER is widely used for telephony, which is a critical service, the ability to crash the server is unacceptable. Valid messages While message parsers should detect erroneous messages as early as possible to preserve the robustness of the applications that use them, they also must correctly parse valid messages. The SIP Torture Test Message RFC [START_REF] Sparks | Session initiation protocol (SIP) torture test messages[END_REF] describes a set of valid SIP messages that test corner cases in SIP implementations.

Guided by this RFC, we have extended our character set mutation rule to generate mutants that are valid SIP messages but are designed to torture a SIP implementation. Figure 7 shows that up to about 4% of the valid messages are rejected by hand-crafted SIP parsers. By comparison, the Zebu-based SIP parser strictly follows the message grammar.

We have tried an analogous experiment with the RTSP applications, but the VLC and LiveMedia parsers are quite lax in their parsing of the message elements, such as the URI, that are covered by the SIP Torture Test RFC, and thus all three applications accept all of the mutated messages.

Performance Evaluation

We now compare the performance of Zebu-based parsers to that of hand-crafted ones. Our results are only for SIP, which is the most demanding in terms of performance. For our experiments, we have implemented four versions of the SIP message statistics reporting application described in Section 3.4. In each case, the application records the host information of the URI stored in the From header field of an INVITE message. The first version (inv-SER-module) is implemented as a dedicated SER module to obtain full access to the internal data structures of SER. The second version (inv-SER-exec) is written using the configuration language of SER and relies on the escape mechanism provided by SER to invoke sed to extract the host information, as described in Section 2.4. The third version (inv-oSIP) is implemented using a few lines of C code on top of the oSIP SIP stack. The last version (inv-Zebu) is the Zebu-based application depicted in Figure 4b.

Our application illustrates the case where an application such as a intrusion detection system needs to access a fragment of a header subfield. To explore the effect that various kinds of messages have on the parsing performance for such an application, we consider a collection of INVITE messages, which are relevant to our application, and an example of a non-INVITE message, which is not. Among the INVITE messages, in INVITE 1 the From header field contains only the URI subfield and an required tag subfield; all of the other subfields, which are optional, are omitted. This entails the minimal processing for a message that is relevant to the application. Our experiments were performed using a Pentium III (1GHz) as the server, which is stressed by a bi-processor Xeon 3.2Ghz client. Figure 8 compares the parsing time for each of the applications to that of SER-module, which has the fastest parser among the existing parsers that we tested.

SER uses the efficient two-level parsing strategy described in Section 3.1, to parse only the header fields that are relevant to the application. The parsing done by inv-SER-module is particularly efficient in the case of INVITE messages, as the information required by the application is already available in the SER internal data structures. The parsing done by inv-SER-exec is roughly as efficient as that done by inv-SER-module for the non-INVITE message. The parsing done by inv-SER-exec for the INVITE messages, on the other hand, is up to 648 times slower, because it forks a sed process. Despite the bad performance in this case, the use of the configuration language of SER remains relevant, because it provides ease of programming and safety, which are not provided by the use of a SER module.

The parsing done by inv-oSIP is over 13 times slower than the parsing done by inv-SER-module for INVITE messages and over 10 times slower for the non-INVITE message. In both cases, oSIP parses the six required SIP headers (plus two more required headers in the case of a REGISTER message) and stores pointers to the starting point of each sub-field. As the application requests information about the INVITE header field, oSIP additionally copies the subfields into a data structure that is provided to the application, roughly doubling the execution time. No results are presented for inv-oSIP for INVITE 3 , because oSIP crashes on this message.

Finally, while Zebu follows the same two-level parsing strategy as SER, the parsing done by inv-Zebu is significantly slower than the parsing done by inv-SER-module for the INVITE messages, because Zebu checks the URI more rigorously than SER. On the other hand, Zebu is significantly more efficient than SER for the non-INVITE messages. SER is directed towards routing applications, and thus it always parses the Via header, which is essential in the routing process, although irrelevant to our application. Thus, Zebu provides better performance in such cases by being more closely tailored to the needs of the application, and retains safety, which is lost in SER when using the module approach.

Related Work

Parser generators such as DATASCRIPT [START_REF] Back | DataScript -a specification and scripting language for binary data[END_REF], PacketTypes [START_REF] Mccann | Packet types: Abstract specifications of network protocol messages[END_REF], PADS [START_REF] Fisher | PADS: a domain-specific language for processing ad hoc data[END_REF], GAPA [START_REF] Borisov | A generic application-level protocol analyzer and its language[END_REF] and binpac [START_REF] Pang | binpac: a yacc for writing application protocol parsers[END_REF] have been recently developed to address the growing complexity of network protocol messages. However, as described in Section 2, these tools do not fulfill all the requirements of network application developers. APG [START_REF] Lowell | APG -an ABNF parser generator[END_REF] is a parser generator that accepts ABNF directly. Semantic actions are specified via callback functions rather than annotations on the grammar. We have found the use of such callback functions to be somewhat heavyweight, in our experience in using APG. Furthermore, APG is not specific to HTTP-like text-based protocols, and thus cannot implement the two-level parsing strategy outlined in Section 3.1, which we have found (Section 4) essential to obtaining good performance. Domain-specific languages have been used successfully in various application domains including operating systems [START_REF] Loo | Implementing declarative overlays[END_REF][START_REF] Mérillon | Devil: An IDL for Hardware Programming[END_REF] and networks [START_REF] Gay | The nesC language: A holistic approach to networked embedded systems[END_REF][START_REF] Hicks | PLAN: A packet language for active networks[END_REF]. Several of these languages have explicitly targeted improving system robustness. The Devil language, in the domain of device-driver development, provides high-level abstractions for specifying the code for interacting with the device, and performs a number of compile-time and (optional) runtime verifications to check that the specifications are consistent [START_REF] Réveillère | Improving driver robustness: an evaluation of the Devil approach[END_REF]. The language Promela++ for specifying network protocols, can be translated automatically both into the model checking language Promela [START_REF] Holzmann | Design and Validation of Computer Protocols[END_REF] and into efficient C code, thus easing the development of a protocol implementation that is both verified and efficient [START_REF] Basu | Promela++: A language for constructing correct and efficient protocols[END_REF].

Mutation analysis has been used to test the robustness of other software components, such as operating systems [START_REF] Duraes | Characterization of operating systems behavior in the presence of faulty drivers through software fault emulation[END_REF], network intrusion detection systems [START_REF] Vigna | Testing network-based intrusion detection signatures using mutant exploits[END_REF], and databases [START_REF] Tuya | Mutating database queries[END_REF]. Our work is most similar to the work on network intrusion detection systems, which also mutates network protocol messages.

Conclusion

In this paper, we have presented the Zebu declarative language for describing protocol message formats and related processing constraints. Zebu builds on the ABNF notations typically used in RFCs to describe protocol grammars. In evaluating Zebu, we have particularly focused on analyzing the improvement in robustness that it provides. For this, we have defined a test methodology based on a mutation analysis that injects errors into network messages. We have applied our test methodology to SIP and RTSP servers by comparing existing parsers with Zebu-generated ones.

The results of our experiments show that nearly 4 times more erroneous messages are detected by the Zebubased parser than by widely-used hand-written parsers. In the case of SIP, we were able to crash the widely used SER parser [START_REF] Pelinescu-Onciul | SIP express router (SER)[END_REF] via a stream of 2416 incorrect messages, sent within a space of 17 seconds. Because SER is used for telephony, which is a critical service, the ability to crash the server is unacceptable. We have also found valid messages that are not accepted by the SER and oSIP parsers, which can similarly have a critical impact. Finally, we have shown that the added safety and robustness provided by Zebu does not significantly impact performance. In the case of SIP, in micro-benchmarks, we have found that a Zebu-based parser is often as efficient as a hand-crafted one.

Figure 1 :

 1 Figure 1: Extract of the ABNF of the message syntax from the SIP RFC 3261

Figure 2 :

 2 Figure 2: PADS specification of the SIP RFC 3261

Figure 3 :

 3 Figure 3: Excerpt of the Zebu Specification for the SIP protocol

Figure 4 :

 4 Figure 4: Fragment of a Zebu-based SIP message statistics reporting application

Figure 5 :

 5 Figure 5: The sizes of the SIP and RTSP message grammars, and the sizes of existing parsers. Sizes in lines of code.

Figure 6 :

 6 Figure 6: Mutation coverage for invalidSIP and RTSP messages

Figure 8 :

 8 Figure 8: Performance of SIP applications (time in cycles, ratio as compared to inv-SER-module)

  also shows the number of lines of code in the oSIP, SER, VLC, and LiveMedia parser implementations.

	Protocol	ABNF size	Zebu spec size	Parser	Parser size
	SIP	700 (approx)	1081	oSIP	11982
				SER	13277
	RTSP	200 (approx)	330	VLC	1200 (approx)
				LiveMedia	1000 (approx)

  The remaining INVITE messages, INVITE 2 and INVITE 3 , show the effect of varying the position of the From header field. In INVITE 2 , the From header field is the first of 34 header fields, while in INVITE 2 it is the last of 34 header fields. The non-INVITE message is a BYE and has 7 headers.

			inv-SER-module	inv-SER-exec	inv-oSIP	inv-Zebu
		Message size	Cycles	Ratio	Cycles	Ratio	Cycles	Ratio	Cycles	Ratio
	INVITE1	697	13 788	1	7 593 550	551	182 703	13	51 054	4
	INVITE2	1 734	13 595	1	8 803 456	648	276 275	20	80 270	6
	INVITE3	1 734	32 045	1	10 015 827	313	-	-	133 164	4
	BYE	334	10 252	1	10 765	1	105 773	10	6 037	0.6

RR n 6167

LiveMedia: Streaming Media, http://www.livemediacast.net/ RR n 6167