Tony Bourdier
email: tony.bourdier@inria.fr

Tree automata based semantics of firewalls

Security constitutes a crucial concern in modern information systems. Several aspects are involved, such as user authentication (establishing and verifying users' identity), cryptology (changing secrets into unintelligible messages and back to the original secrets after transmission) and security policies (preventing illicit or forbidden accesses from users to information). Firewalls are a core element of network security policies, that is why their analysis has drawn many attention over the past decade. In this paper, we propose a new approach for analyzing firewalls, based on tree automata techniques: we show that the semantics of any process composing a firewall (including the network address translation functionality) can be expressed as a regular set or relation and thus can be denoted by a tree automaton. We also investigate abilities opened by tree automata based representations of the semantics of firewalls.

Introduction and motivations

Since the late 80s, firewalls are at the heart of network security. First designed to enable private networks to be opened up to the outside in a secure way, the growing complexity of organizations make them indispensable to control information flow within a company. The central role of firewalls in the security of the organization information make their management a critical task. Moreover, it is admitted for some years the importance of using formal methods to specify security policies. For example, to achieve high levels of certification (EAL1 5, 6, 7), it is necessary to provide a formal specification enabling to obtain mechanized formal proofs, to carry out techniques for test generation or to perform static analyses ensuring required properties.

Thus, for years, many methods and tools have been developed for analyzing and testing firewall policies. These methods can be broken down into two different categories: the active methods and the passive methods. The former consist in sending packets to the network and to make a diagnosis according to the received packets. The main advantage of these methods is that they can be directly performed without any computation. However, such methods have the major drawback of consuming bandwidth, interfering with the traffic and being no exhaustive. That is why many works focused on passive methods, that is methods which send no packet and make an offline analysis. Two main categories of passive analysis are investigated in the literature: structural analysis and query analysis. Structural analysis examine the relationships that rules have with other rules within a firewall configuration or across multiple firewalls. These works consider that a misconfiguration (or conflict) occurs when several rules match the same packet or when a rule can be removed without changing the behavior of the firewall. Query analysis provides a way to ask questions of the form "Which computers in the private network can receive packets from www.inria.fr?". It then consists in defining a language to describe a firewall query and a way to compute its solutions. Some interesting work [AsH04, CCBGA06, ABR08, ASH03, BB07, GL04, CCBGA05, Liu08, ASHBH05] looked into structural analysis and others [Haz00, EZ01, LG09, MK05] looked into query analysis. Indeed, [AsH04, CCBGA06, ABR08, ASH03, BB07, GL04, CCBGA05, Liu08, ASHBH05] focus on defining, detecting and discussing misconfigurations. All of them assume that packets are not modified during their network traversal and then do not support network translation address capabilities. [Haz00, EZ01, LG09, MK05] use structures based on decision diagrams which provide a way to represent both rule sets of firewalls and solutions of some queries over firewalls. All these works are dedicated to a specific analysis.

Comparing to these works, our aim is to study a representation of the semantics of each component of a firewall based on tree automata and to build a decidable first order theory associated to the firewall. We show that issues raised by previously mentioned analyses are definable in this theory and thus obtain a generic procedure for performing these analyses.

Indeed, one of the main motivations of tree automata is the study of computational problems that can be solved using these machines. The usual approach consists in associating a logical system to a class of automata, which provides decision procedures for problems expressed as specifications in this logical system. Although one knows that decidable theories are not necessarily trivial from a computational point of view, we use here some classes of automata that enable operations over tree automata to be performed with low-complexity algorithms. Moreover, a significant work has been done during the last years in order to obtain new efficient algorithms. In particular, some libraries implementing efficient algorithms with efficient data structures have been recently developed [START_REF] Lengál | An efficient tree automata library[END_REF]. A great advantage of our approach is the use of the well established algebraic frameworks of tree algebra and automata. Thus, our work takes full benefit from years of research on these domains. In particular, as we will sketch at the end of this paper, we can successfully apply from our work new techniques for model checking, called regular tree model checking, that have been developed to verify systems whose transition relation is described with a binary tree automaton [START_REF] Abdulla | Regular tree model checking[END_REF][START_REF] Bouajjani | Abstract regular tree model checking[END_REF]. Such techniques, following our approach, allow for example to find unwanted flows of packets from a given network security policy.

Roadmap. In Section 2, we recall basic definitions of terms, rewrite systems and tree automata. In Section 3, we show that the semantics of all firewall components are regular sets and relations. We investigate in Section 4 the possibilities opened by a tree automata based description of the semantics of firewalls. In particular, we define a first order theory in which all usual analyses are definable. We also discuss further abilities made possible by the use of tree automata. Finally, we give concluding remarks in Section 5.

Preliminaries

We assume that the reader is familiar with the standard notions of rewrite systems and tree automata. Comprehensive surveys can be found in [START_REF] Baader | Term rewriting and all that[END_REF] for first order terms and rewrite systems and in [CDG + 08] for tree language theory. This section fixes our notations.

Term algebra and rewrite systems

A signature Σ consists of a finite set S Σ whose elements are called sorts and an alphabet of symbols together with an application which associates to any symbol f a non empty sequence of sorts, which is denoted by f : s 1 × . . . × s n → s. ar(f ) = n is called the arity of f . Given a signature Σ, a sort κ ∈ S Σ and a countable set X s of variables for each sort s, we denote by T κ Σ,X the set whose elements are called terms sorted by κ inductively defined as follows: for any x ∈ X κ , x is in T κ Σ,X and for any f :

s 1 × . . . × s n → κ and t 1 , . . . , t n ∈ T s 1 Σ,X × . . . × T s n Σ,X , with s i ≤ s i for any i, the word f (t 1 , . . . , t n ) is in T κ Σ,X .
T Σ,X is the union of T s Σ,X for every sort s. The set of variables occurring in t ∈ T Σ,X is denoted by Var(t). If any variable of Var(t) occurs only once in t, t is said to be linear. If Var(t) is empty, t is called a ground term. T Σ denotes the set of all ground terms. A position of a term t is a finite sequence of positive integers describing the path from the root of t to the root of the sub-term at that position. The empty sequence representing the root position is denoted by ε. Pos(t) is called the set of positions of t. t |ω , resp. t(ω), denotes the subterm of t, resp. the symbol of t, at position ω. We denote by t [s] ω the term t with the subterm at position ω replaced by s. We call substitution any mapping from X to T Σ,X which is the identity except over a finite set of variables Dom(σ) called domain of σ extended to an endomorphism of T Σ,X . σ is often denoted by {x → σ(x) | x ∈ Dom(σ)}. If for any x ∈ Dom(σ), σ(x) ∈ T Σ , σ is said to be ground. For any ground substitution σ, σ(t) is called a ground instantiation of t. A rewrite rule (over Σ) is a pair (lhs, rhs) ∈ T Σ,X × T Σ,X such that Var(lhs) ⊆ Var(rhs) and a rewrite system is a set of rewrite rules R inducing a rewriting relation over T Σ , denoted by → R and such that t → R t iff there exist (l, r) ∈ R, ω ∈ Pos(t) and a ground substitution σ such that t |ω = σ(l) and t = t [σ(r)] ω . Finally, we denote by * -→ R the reflexive transitive closure of → R .

Tree automata

We call n-ary tree automaton any quadruple A = Σ, Q, F, ∆ such that Σ is an alphabet of function symbols, Q is a finite set of states, F is a subset of Q whose elements are called final states and ∆ is a relation over T Σ n [Q] × Q whose elements are called transitions where Λ is a new symbol and Σ n [Q] consisting of the unique sort conf and the alphabet

(Σ ∪ {Λ}) n \ { Λ, . . . , Λ } ∪ Q such that f 1 , . . . , f n ∈ (Σ ∪ {Λ}) n is of sort conf × . . . × conf → conf with ar(f 1 , . . . , f n ) = max i∈[1,n] (ar(f i ) | f i = Λ) and any q ∈ Q is a constant of sort conf . An ele- ment of T Σ n [Q] is called a configuration. A transition lhs → rhs of ∆ is normal- ized iff for any ω = ε, lhs(ω) ∈ Q.
An automaton whose transitions are normalized is said normalized. A tree automaton is said deterministic iff all its transitions have a different left-hand side. Without loss of generality, we can consider that all automata are normalized and deterministic. The rewriting relation induced by ∆ over T Σ n [Q] is denoted by → A and the language recognized by A is

L(A) = { t 1 , . . . , t n ∈ T Σ | ∃q f ∈ F, t 1 ⊗ . . . ⊗ t n * - → A q f } where t = t 1 ⊗ . . . ⊗ t n is the configuration such that: ∀ω ∈ n i=1 Pos(t i ), t(ω) = t 1 [ω), . . . , t n [ω) where u[ω) = u(ω) if ω ∈ Pos(t) and Λ otherwise.
A set E of n-tuples of terms (or equivalently n-ary relation) is said regular iff there exists an n-ary tree automaton A such that E = L(A). Moreover, we say that a set (or a relation) is effectively regular iff it is regular and we can compute the automaton which recognizes it.

The table depicted in Figure 1 recalls usual automata and operations over tree automata together with their semantics. We recall that the membership, the emptiness, the finiteness, the equivalence and the inclusion problems are decidable for tree automata.

Firewall semantics

In this section, we propose a definition of firewall semantics using tree automata. First, we informally explain the behavior of firewalls. Next, we describe the language from which we will describe firewall semantics. Finally, we show in the last part of this section that we can automatically compute, from usual specifications of firewalls, tree automata describing the behavior of each of their components and how to combine them to obtain an automaton corresponding to a firewall.

Notation

Language recognized by the automaton

A ⊕ A L(A) ⊕ L(A ) where ⊕ is ∩, ∪, or × A (T Σ ) n \ L(A) Ω κ T κ Σ Id n (A) n-tuples t, . . . , t for t ∈ L(A) rec(t)
ground instantiations of t (t linear)

i (A) (n+1)-tuples t 1 , . . . , t i-1 , t, t i , . . . , t n s.t. t 1 , . . . , t n ∈ L(A) i (A) (n-1)-tuples t 1 , . . . , t i-1 , t i+1 , . . . , t n s.t. ∃t ∈ T Σ : t 1 , . . . , t i-1 , t, t i+1 , . . . , t n ∈ L(A) i/t (A) (n-1)-tuples t 1 , . . . , t i-1 , t i+1 , . . . , t n s.t. t 1 , . . . , t i-1 , t, t i+1 , . . . , t n ∈ L(A) ∂ k f 1 ,...,fn (A) n-tuples t 1 , . . . , t n s.t. ∃ f 1 (. . . , x k-1 1 , t 1 , x k+1 1 , . . .), . . . , f n (. . . , x k-1 n , t n , x k+1 n , . . .) ∈ L(A)
Figure 1: Operations effectively preserving regularity

Processing model

In a network, when a host wants to transmit a message to another host, data message are encapsulated in a packet. A packet consists of the data that should be transmitted as well as some additional information, called header, used to route it to the appropriate destination. To control packet transmission between different subnetworks2 , it is common to deploy a network security policy based on a combination of firewalls. A firewall is an application that controls the forwarding of packets which cross it by using a combination of:

• packet filtering, which consists in inspecting each packet and either allowing it to continue its traversal or dropping it and

• network address translation, which consists in modifying network address information in packet headers.

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

Example 1. The following figure gives a simple example of firewall:

Filtering:    IP

Vocabulary for formal reasoning

In order to give a formal semantics to each of firewall components, we need to define the vocabulary from which we will describe the objects of our study (IP, packets, . . . ). As the introduction of this paper lets it suppose, we base our work on a description of each entities which composes a firewall as a term. In other words, we use terms to represent all these entities. In what follows, we will talk about symbolic representation of these entities.

For readability reasons, we consider in what follows that packets are only described by addresses and ports. Other information, such as protocols, tcp flags, states, could be considered without difficulty. The selected symbolic representation of entities is based on the following signature:

0, 1 : Binary → Binary # : → Binary ip : Binary → IP port : Binary → Port f rom : IP × Port → SrcAddress dest : IP × Port → DstAddress packet : SrcAddress × DstAddress → Packet
As we consider in this paper only one signature, we will denote by sort the set of ground terms of sort sort (abuse of notation).

Let us describe the meaning of the above symbols. IP addresses are represented as terms of sort Binary describing the inverted binary representation of the address. For example, the IP address 192.168.1.1 is symbolically denoted by the following term ip(1(0(0(0(0(0(0(0 (1(0(0(0(0(0(0(0 (0(0(0(1(0(1(0(1 (0(0(0(0(0(0(1(1(#) • • • ) (knowing that the integer 192 has 11000000 for binary representation and 168 has 10101000). We proceed in the same way for ports (with the symbol port instead of ip). Finally, packets are terms of sort Packet. For convenience, we will use in this paper the dot-decimal notation for addresses and the decimal notation for ports. For example: packet(f rom(ip(192.168.1.1), port(80)), dest(ip(172.20.3.1), port(80))) has to be understood as the term packet(f rom(ip(t s ), port(t p )), dest(ip(t d ), port(t p ))) where    t s = 1(0(0(0(0(0(0(0 (1(0(0(0(0(0(0(0 (0(0(0(1(0(1(0(1 (0(0(0(0(0(0(1(1(#) • • • ) t d = 1(0(0(0(0(0(0(0 (1(1(0(0(0(0(0(0 (0(0(1(0(1(0(0(0 (0(0(1(1(0(1(0(1(#) • • • ) and t p = 0(0(0(0(1(0(1(0(0(0(0(0(0(0(0(0(#) • • • ) Now, let us recall that a subnetwork is a logically visible subdivision of an IP network. Subnetworks are characterized by the partition of IP addresses into two parts: a "network prefix" and a "host number". More precisely, defining a subnetwork consists in giving a number n < max of bits (where max is 32 for IPv4 and 128 for IPv6) together with a sequence of n bits (characterizing the network prefix). The remaining max -n bits identify the host within the subnetwork. For example, the subnetwork (CIDR notation [START_REF] Fuller | Classless Inter-Domain Routing (CIDR): The Internet Address Assignment and Aggregation Plan[END_REF]) 192.168.5.64/26 corresponds to the range of IP addresses whose binary representation begins with the 26 first bits of the binary representation of 192.168.5.64. Note that for convenience, we suppose that any term of sort IP represents an IP address. A term of sort IP corresponds to an IPv4 address (resp. IPv6) iff it contains exactly 32 (resp. 128) symbols 0 or 1. Proposition 2. The set of symbolic representations of IP addresses which belong to a given subnetwork is a regular set.

Proof. Let be a subnetwork characterized by a prefix b 1 , . . . , b n . The minimal deterministic automaton recognizing the set of IP addresses which belong to this subnetwork is given by:

   ip(q n ) → q F 0(q n ) → q n 1(q n ) → q n    ∪ {b i (q i-1 ) → q i | i = 1, . . . , n} ∪ {# → q 0 } Note that if we denote by E[n] the subset of terms of E of length n, for any boolean operation ⊕, E[n] ⊕ F [n] = (E ⊕ F )[n]
. Thus, there is no problem to consider automata which recognize IP addresses of an arbitrary length.

Tree automata based semantics

In what follows, we consider that a firewall f is given by three sets filter(f ), dnat(f ) and snat(f ) respectively containing filtering rules, prerouting (or DNAT) rules and postrouting (or SNAT) rules as well as an order relation < f over these rules.

Filtering rules

Let us start by giving a semantics of filtering rules. If we denote by Packet the set of all packets, then any filtering rule r ∈ filter(f ) is associated to a subset of Packet which corresponds to the packets validating all conditions specified by r. For any packet p ∈ Packet and filtering rule r, we write r filter p to indicate that the packet p matches the rule r. Proposition 3. For any filtering rule r, the set filter (r) = {p ∈ Packet | r filter p} is effectively regular.

In addition, since filtering rules of firewalls are evaluated depending on the order < f (only the first matched rule is applied), then the set of packets that effectively match a rule depends on the set of prior rules. For any firewall f and filtering rule r occurring in f , we define the relation f filter as follows: r f filter p iff r filter p and there is no prior rule r < f r in filter(f ) such that r filter p.

Proposition 4. For any firewall f and filtering rule r ∈ filter(f ), the set

f filter (r) = {p ∈ Packet | r f filter p} is effectively regular.
We saw that the goal of a filtering rule is to associate some set of packets with a decision (accept or drop). Thus, we can see any filtering rule r as a partial function r -→ filter which associates to any packet p such that r filter p either accept or drop. Moreover, as previously, we define a partial function r -→ f filter which maps any packet p such that r f filter p to the decision (accept or drop) associated to r.

Proposition 5. For any firewall f and filtering rule r ∈ filter(f ), the partial functions r -→ filter and r -→ f filter are effectively regular (as relations).

Finally we can associate any firewall f with a function which maps any packet p ∈ Packet to a decision. This function is, by definition:

-→ f filter = r∈filter(f ) r -→ f filter
(where the functions r -→ f filter are seen as relations with disjoint domains). We obtain the following proposition: Proposition 6. For any firewall f , -→ f filter is effectively regular.

Translation rules

The objective of the network address translation rules is to transform any packet into another packet (possibly identical). So, every rule r of dnat(f ) can be considered as a partial function r -→ dnat from Packet to Packet. A similar reasoning leads us to define for every rule r ∈ dnat(f ) the relations r dnat p and r f dnat p respectively meaning that p matches the rule r and that p matches r but does not match any prior rule r < f r.

Proposition 7. For any DNAT rule r, r -→ dnat is effectively regular.

Proof. Let r be a DNAT rule. r is characterized by a source subnetwork net together with a target IP address add as well as possibly a source port sport together with a target port tport. If no port is specified, then the translation does not alter the destination port of the packet. Let us build the automaton recognizing the functional relation r -→ dnat . We denote by:

• A[net] the tree automaton which recognizes the set of IP addresses which belong to net;

• A[add] the automaton recognizing the IP address add;

• A[sport] and A[tport] the automata recognizing, if specified, sport and tport.

We build the automaton A dnat [r] as the automaton containing the following rules:

• packet, packet (q f r , q dst ) → q F (q F is the unique final state);

• rules of the automaton Id 2 (Ω SrcAddress ) whose final state is renamed into q f r ;

• dest, dest (q ip , q port ) → q dst ;

• rules of the automaton Id 2 (Ω Port ) whose final state is renamed into q port if sport and tport are not specified or rules of A[sport] × A[tport] whose final state is renamed into q port otherwise;

• rules of the automaton A[net] × A[add] whose final state is renamed into q ip ; Like filtering rules, any DNAT rule r has a different semantics in the context of the set of DNAT rules of a firewall f . We denote by r -→ f dnat the corresponding semantics which also is a function from Packet to Packet. Proposition 8. For any firewall f and filtering rule r ∈ dnat(f ), the partial function r -→ f dnat is effectively regular (as a relation).

When a packet matches no DNAT rule, then it is not translated by DNAT. In other terms, the semantics of the set of rules dnat(f ) is a total function r -→ dnat from Packet to Packet which is the identity except over the union of domains of r -→ dnat for r ∈ dnat(f ). Formally, we have:

-→ f dnat =   r∈dnat(f ) r -→ f dnat   ∪ id |Packet\( r∈dnat(f ) dnat(r))
Proposition 9. For any firewall f , -→ f dnat is effectively regular.

All the notations and results presented in this part are naturally extended to SNAT.

Firewall semantics

We saw in Section 3.1 that when a packet p goes through a firewall f , the following steps occur:

• p is rewritten into p by the DNAT rules,

• p is either accepted or dropped,

• if p is accepted, then p is rewritten into p by the SNAT rules.

In other words, any firewall f describes a function which associates to a packet p ∈ Packet either another packet or drop. We denote by f -→ this function.

Proposition 10. For any firewall f ,

f -→ is effectively regular. Proof. f -→ = L 2 3 (A dnat ) ∩ 1,3 (A accept filter ) ∩ 1 (A snat ) ∪ 2 (A dnat ∩ 1 (A drop filter )) × rec(drop)
where:

• L(A dnat ) = -→ f dnat , L(A snat ) = -→ f snat , • L(A accept filter ) = ( -→ f filter ) -1 (accept) and L(A drop filter ) = ( -→ f filter ) -1 (drop).

Applications

Our goal is to show that all usual analyses can be expressed as operations (which preserve regularity) over sets and relations that have previously been shown regular and that our approach allows us to extend the possibilities of analyses. In this section, we first study simple properties over a firewall (completeness and comparison). We next show that our approach allows us to deal with usual analyses (structural and query analyses). Finally, we discuss one further ability enabled by our approach.

Properties

If one sees a firewall as a decision process which associates to an incoming packet a decision which can be drop or another packet, the following properties are relevant to analyze: consistency, which indicates that at most one decision is taken for a given incoming packet, termination, which assures that a firewall computes a decision in a finite time and completeness, which means that for any incoming packet, the firewall returns a decision. Another important issue is to compare different firewalls. By construction, every firewall denotes a terminating and consistent decision process. Then, we deal with completeness and comparison. We first give the formal definition of completeness and next define an order to compare firewalls.

Definition 11 (Completeness). We say that a firewall f is complete iff f -→ is a total function. Proposition 12. Completeness is decidable.

It is sufficient to check that the projection over the first component of the automaton recognizing f -→ equals to Ω Packet (decidable). In the case of complete firewalls, it can be important to determine if a firewall is less or more permissive than another one. More permissive means allowing at least the same traffic. Such an order is obviously not total.

Definition 13 (Order). We define a partial order over complete firewalls as follows: for any f and f , f f (f is more permissive than f ) iff for any

p, p ∈ Packet, if p f -→ p then p f ' -→ p . We write f ≈ f iff f f and f f . Note that f ≈ f iff f -→ = f ' -→.
Proposition 14. The order relation is decidable.

Proof. It is sufficient to compute the automata recognizing the restriction of f -→ and f ' -→ to packets which are not associated to drop and to test the inclusion between them.

Structural analysis

Structural analysis refers to the detection of misconfigurations (or anomalies) in firewalls rules. A complete survey of misconfigurations can be found in [START_REF] Cuppens | Detection of network security component misconfiguration by rewriting and correlation[END_REF][START_REF] Hamed | Taxonomy of conflicts in network security policies[END_REF]. Examples of anomalies are shadowing, redundancy, correlation, exception,. . . We have shown that the sets and relations of Figure 2 are regular and that we can compute tree automata which recognize them. It is well known that the set of solutions of any first order formula containing only variables and ground terms (or equivalently the computation of algorithms containing only operations depicted in Figure 1) over regular sets and relations are effectively regular, i.e. we can compute a tree automaton which recognizes the set of solutions.

(i) filter (ii) snat (iii) dnat (iv) f filter (v) f snat (vi) f dnat (vii) • -→ filter (viii) • -→ snat (ix) • -→ dnat (x) • -→ f filter (xi) • -→ f snat (xii) • -→ f dnat (xiii) -→ f filter (xiv) -→ f snat (xv) -→ f dnat (xvi) f -→
Definition 15. For any firewall f , we define Th f as the first order theory based on the following syntax:

• Constants: rules of f , packets of Packet, decisions (accept and drop)

• Predicate symbols: those of the Figure 2 and< f • Quantifiers: ∃ and ∀ • Variables: any countable set • Connectives: ∧, ∨, ⇒, ¬ Proposition 16. For any firewall f , the theory Th f is decidable. Moreover, for any formula of Th f , we can compute a tree automaton recognizing the set of solutions.

A possible algorithm to compute the tree automaton corresponding to a formula of Th f can be established following the approach described in [START_REF] Dauchet | The theory of ground rewrite systems is decidable[END_REF]. In addition, we can easily show that any misconfiguration can be expressed as a formula of Th f . It would be tedious to consider all anomalies, that is why we only discuss about an example of misconfigurations (shadowing). Let us first recall the definition of the shadowing anomaly.

Definition 17 (Shadowing). We say that a firewall has shadowing iff it contains at least one filtering rule such that all packets it accepts (resp. drops) are dropped (resp. accepted) by a prior rule. In such a case, the concerned rule is said to be shadowed.

Proposition 18. The shadowing property can be expressed as a formula of Th f . Indeed, we can define the formula Shadowed f (r) as follows :

∀p: p r -→ f filter accept ⇒ (∃r : r < f r ∧ p r -→ f filter drop) ∨ ∀p: p r -→ f
filter drop ⇒ (∃r : r < f r ∧ p r -→ f filter accept) Thereby, the real question which arises from structural analysis in our case is to know if the selected symbolic representation of packets provides efficient algorithms to perform these operations. Indeed, it is well-known that operations over tree automata have high complexity in general. We can remark that in our case the complexity of operations strongly relies on the representation of addresses. Therefore, let us focus our discussion over addresses and their representation. We made the choice of describing addresses as words over {0, 1} (or equivalently as terms built from monadic symbols 0 and 1 and a constant #). To simplify explanations, we consider word automata (the correspondence with tree automata is straightforward). A good property of manipulated ranges of addresses is that corresponding minimal and deterministic automata has no loop except at their unique final state which loops over itself for any word. Let us call n-prefix (or simply prefix) language any regular language of the form α 1 .{0, 1} * ∪ . . . ∪ α n .{0, 1} * . The main advantages of such languages are the following:

• boolean operations preserve the prefix property,

• boolean operations can be performed in O(n) (where n is the number of states of the bigger operand) over the minimal deterministic automata and

• the corresponding algorithms directly produce deterministic and minimal automata (which avoid to perform any determinization).

Consequently, misconfigurations can be efficiently detected.

Query analysis

Another main issue addressed about firewalls is query analysis.

Further abilities

Let us mention a promising example (that we can not develop due to the lack of place): regular tree model checking. Regular tree model checking is a method for formal verification of infinite-state systems whose states are encoded as trees and whose transition relation is denoted by a tree transducer (transducers are binary tree automata recognizing relations over terms having the same set of positions). Given a transducer T , regular tree model checking consists in computing the transitive Tree automata based semantics of firewalls closure of →= L(T ) and then the set of reachable states (from a regular initial set of configurations) as tree automata ([ALdR05, BHRV06]).

Regular tree model checking can be successfully applied to network security policies analysis. Indeed, given a network composed by firewalls separating several subnetworks, we can define a transition system whose states are terms of sort Packet in which the head symbol has been replaced by a symbol which indicates the subnet in which the packet is located. To any firewall f in the network is associated a part of the transition relation corresponding to the semantics of f such that net 1 (t) → f net 2 (t ) if f separates the networks net 1 and net 2 and packet(t) f -→ packet(t ). A host h which belongs to the subnet net can receive the packet packet(t) from another host h located in net if net(t) is a reachable state (and t contains the subterm dest(ip, port) where ip is the IP address of h) from the automaton recognizing net (t ) (and t contains the subterm dest(ip , port ) where ip is the IP address of h ). Given such a transition system and knowing that the transition relation is recognized by a transducer if we fix the size of IP addresses (the proof is obvious), our framework allows us to detect violations of the security policy. Indeed, contrary to query analysis which only allow to compute valid instantiations of a given path (since any query describes a path in the network), regular tree model checking provides a way to prove the existence of paths denoting unwanted (and no necessarily direct) flows of packets.

Conclusion

We have proposed in this paper an original way to describe firewall semantics using tree automata. We have shown that this approach allows us to perform usual analysis over firewall policies. Some advantages of our approach are the following: First, unlike most of existing works, tree automata allow us to consider the network address translation functionality. Second, the proposed approach allows us to perform structural and query analysis. Misconfigurations are automatically computed from their formal definitions. Moreover, we have shown that our approach opens new perspectives of analyses. For all these reasons, describing firewall semantics with tree automata seems to be relevant and promising. We currently work on several follows-up of the results presented in this paper. The first one concerns composition of firewalls: we try to extend the specification of firewalls to take into account the routing functionality. It would allow us to define the semantics of complex compositions of firewalls. We also want to address the problem of minimalizing the set of rules of a given firewall, i.e. building from a tree automata based firewall semantics an equivalent firewall having a minimum of filtering and NAT rules. Finally, we currently work on the implementation of the work presented in this paper.

Figure 2 :

 2 Figure 2: Sets and relations of the theory of a firewall f

  We use the CIDR notation[START_REF] Fuller | Classless Inter-Domain Routing (CIDR): The Internet Address Assignment and Aggregation Plan[END_REF] to denote subnetworks 3 . Any packet of protocol tcp whose source is 192.168.20.1:80 and destination 192.168.5.130:80 (notation address:port) is forwarded by the firewall as a packet whose source is 121.130.1.1:80 and whose destination is 121.130.1.15:80 whereas any packet whose destination is 121.130.1.30:80 is dropped by the firewall.

			address src IP address dest Protocol Port src Port dst Decision
			192.168.20.1/24 121.130.1.1/28	tcp	80	any	accept
			any	any		any	any	any	drop
	NAT:	 	Src/Dest Dest	Address range 192.168.5.128/25	Port range New address [ : port ] any 121.130.1.15:80
			Src	192.168.20.1/24		any	121.130.1.1

  Query analysis provides a way to assist firewall administrators in understanding the behavior of a firewall by computing the result of user-defined queries such as "Which hosts in the subnetwork 192.168.1.1/22 can receive packets from a host in the subnetwork 172.20.1.1/24 ?". Such analysis only recently emerged with[START_REF] Marmorstein | An open source solution for testing NAT'd and nested iptables firewalls[END_REF][START_REF] Liu | Firewall policy queries[END_REF]. To handle the class of queries presented for example in[START_REF] Liu | Firewall policy queries[END_REF], it is sufficient to slightly extend the formulae of Th f . The main feature handled in usual queries which cannot be computed by a formula of Th f is reasoning about the different fields of packets (source or destination IP, . . . ). Thus, we add to Th where 138.96.146.2 is the IP address of www.inria.fr. From this formula we can compute a tree automaton recognizing the set of pairs of IP addresses and ports ip 1 , p 1 satisfying the query.

f : • linear terms of sort Packet whose variable are of sort IP or Port • subnetworks (as constants) • a binary predicate ∈ over terms of sort Packet and subnetworks This extension of Th f preserves the Proposition 16.

Example 19. Let us consider a firewall f between a private network and the internet together with the following query "Who can access to www.inria.fr from the private network 192.168.1.1/22" ? This query can be expressed as the following formula:

ip 1 ∈ 192.168.1.1/22 ∧ ∃ip 2 , ip 3 , ip 4 , p 2 , p 3 : packet(f rom(ip 1 , p 1 ), dest(ip 2 , 80)) f -→ packet(f rom(ip 3 , p 2 ),

dest(138.96.146.2, 80)) ∧ packet(f rom(138.96.146.2, 80), dest(ip 3 , p 2 )) f -→ packet(f rom(ip 4 , p 3 ), dest(ip 1 , p 1 ))

Evaluation Assurance Level

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

Acknowledgment

The author would like to thank Jean-Christophe Bach for discussion about firewalls and Horatiu Cirstea for its improvement suggestions. This work was supported by anr ssurf and région Lorraine.


Lamia Benamara

Clémence Magnien

Pierre Borgnat

Patrice Abry

Matthieu Latapy

Marcelo Dias

Removing bias due to finite measurement of dynamic systems: case study on P2P systems

Mesurer avec précision la dynamique des graphes de terrain est une tâche difficile, car les propriétés observées peuvent être biaisées pour différentes raisons, en particulier le fait que la période de mesure soit finie. Dans ce papier, nous introduisons une méthodologie générale qui nous permet de savoir si la fenêtre d'observation est suffisamment longue pour caractériser une propriété donnée dans n'importe quel système dynamique.

Introduction

Many systems are naturally dynamic. For instance in the internet, routers, AS and/or links between them are created or deleted [START_REF] Magnien | Fast dynamics in internet topology: Observations and first explanations[END_REF]; in peer-to-peer (P2P) networks users join or leave the system [SR06, [START_REF] Saroiu | Measuring and analyzing the characteristics of napster and gnutella hosts[END_REF][START_REF] Stevens Le-Blond | Finding good partners in availability-aware P2P networks[END_REF] and exchange different files at different times. In all these cases, understanding the dynamics of the system is a key issue. However, accurately measuring these dynamics is a difficult task. In particular, the fact that the observation window is necessarily finite induces a bias for property characterization [START_REF] Stutzbach | Understanding churn in peer-to-peer networks[END_REF][START_REF] Saroiu | Measuring and analyzing the characteristics of napster and gnutella hosts[END_REF]. Though this bias tends to decrease when the observation window length increases, it is difficult to quantify it in practice, or know whether it is negligible or not.

In this paper, we introduce a new methodology that allows to rigorously determine the minimum observation time required to characterize a stationary property in real-world dynamic systems. This methodology is different and complementary to other methodologies existing in the literature [SR06, SGG03, GT99], and has two main advantages. First, it allows to determine if the observation window was long enough for a rigorous characterization. Second, it can be applied to any property characterizing the dynamics of a system. To illustrate its relevance, we apply it to the study of session lengths and files' life duration in two different P2P systems.

Methodology

Suppose we start observing a dynamic graph at a time t, for a duration l. We denote by W t,l this observation window. We are faced with two problems if we want to characterize the graph's dynamics from the observation of W t,l . First, l must be long enough for W t,l to be representative. Second, even if it is representative, the fact that l is finite still induces a bias for property characterization. Indeed, events occurring before t or after t + l are not observed, which prevents from characterizing accurately some quantities. An important point to observe is that the longer the measurement period, the smaller the bias induced.

Our methodology addresses these two issues at the same time. Intuitively, it aims at deciding if the measurement period W t,l is long enough to characterize a given property P, i.e. if the bias induced by its finiteness on the observed property is negligible. If the window W t,l is long enough, then if we use a longer window W t,l+x , the observed property does not change: P(W t,l ) = P(W t,l+x ). In order to know if a given window is long enough, we use windows of increasing length W 0,l 1 ,W 0,l 2 , ... W 0,l n , with l 1 < l 2 < ... < l n . By studying how the observed property P(W 0,l 1 ),P(W 0,l 2 ), ...P(W 0,l n ) evolves as a function of l, we determine if it is correctly evaluated or not.

Finally, an important point is that characterizing a property P only makes sense if it is stationary, i.e. if P does not evolve while the measurement is under progress. Notice however that if it is not stationary, our methodology will not be able to provide a characterization: the observed property P will not become stable when the observation window length l increases. If it does become stable, this means both that W t,l is long enough, and that P is stationary. Notice that, depending on the property studied, other types of bias can occur, see for instance [START_REF] Stutzbach | Understanding churn in peer-to-peer networks[END_REF], including biases coming from the identification of users and their sessions. We will also rigorously take this into account, see Section 4.1.

Here, most of the properties we study are complementary cumulative distributions, i.e. for each value k, P k is the fraction of all observations values which are larger than or equal to k.

To study how an observed distribution P evolves with the length of the observation window, we will first plot the observed distributions P(W t,l ) for different values of l. In order to confirm more formally the visual observations, we will also study a statistical indicator which quantifies how close two distributions P and Q are to each other: the Monge-Kantorovich distance, or M-K distance [START_REF] Tryphon | Metrics for power spectra: An axiomatic approach[END_REF] compares two normalized cumulative (complementary or not) distributions P and Q. It is equal to the mean of the distance between the two distributions:

MK(P, Q) = (∑ k |P k -Q k |)/k max .
We use this indicator to study how the observed distribution P(W t,l ) evolves: we compute the M-K distance between P(W 0,l ) (with different values of l) and P(W 0,l max ), where l max is the length of the longest observation window for this dataset, and plot this as a function of l. Following [START_REF] Willinger | A pragmatic approach to dealing with highvariability in network measurements[END_REF], we also study the mean and the standard deviation of P(W 0,l ) as a function of l.

Data

In order to show the relevance of our methodology, we use two datasets: the queries dataset which is a capture of the UDP traffic of a large eDonkey server [START_REF] Aidouni | Ten weeks in the life of an edonkey server[END_REF]. It consists of the queries made by users (for lists of files matching certain keywords, or for providers for a given file), and of the server's answers to these queries. The measurement lasted for 10 weeks which represents 1 billion messages, with 89 million peers and 275 million files involved. The logins dataset consists in a trace of the login and logout of peers on the eDonkey network [START_REF] Stevens Le-Blond | Finding good partners in availability-aware P2P networks[END_REF]. It contains more than 200 millions of connections by more than 14 millions of peers, over a period of 27 days. The two datasets are therefore complementary.

Users' session lengths

Definition of a session

We do not formally know when user sessions begin or end in the queries dataset, because there is no notion of session in the UDP eDonkey protocol. Instead, users make stand-alone queries and receive answers from the server. We therefore have to infer sessions from these queries.

It is natural to consider that two consecutive queries made by a same user belong to the same session (whether they are for a same file or not) if the time elapsed between them is short, and belong to two different sessions if it is long. The question is then to find an appropriate threshold for distinguishing between these two cases. Based on the study of the inter-query time distribution (not presented here), we have chosen to use a threshold of 10 800 seconds, i.e. 3 hours.

Removing bias due to finite measurement of dynamic systems: case study on P2P systems

Characterization of session lengths

We now apply our methodology to the study of the session length distributions S, by studying S(W 0,l ) for different values of l. Figure 1 shows the complementary cumulative distribution S(W 0,l ) for different values of l, up to l = 10 weeks, for the queries dataset. The shapes of these distributions are similar, with a small fraction of sessions with length smaller than 2 000 s, and an approximately linear shape between 2 000 s and 100 000 s. However, when l ≤ 1 day, the distributions exhibit a clear cut-off. This is not the case anymore for l ≥ 4 days: the tail of the distribution flattens after a bend occurring close to 100 000 s (∼ 28 hours), and we observe a small fraction of extreme values after this bend. For observation windows larger than four days, the shape of the distribution does not seem to evolve anymore: the distributions corresponding to l = 1 week and l = 10 weeks (presented in the inset) are very similar to each other and to the one obtained for l = 4 days. One must be however careful when driving conclusions from a visual examination. Indeed, if we observe the same plot as the inset of Figure 1 but with a linear scale on the x-axis and a logarithmic scale on the y-axis (see Figure 2), the distributions seem visually strongly different from each other. However, the distributions are different only for less than 1% of the values, which are values after the bend in Figure 1 and are extreme values. The fact that the extreme values change when l increase shows that they cannot be characterized with our methodology, and we leave their study for further work.

To confirm these observations, we study MK(S(W 0,l ), S(W 0,l max )) as a function of l, presented in Figure 3. The values observed tend to decrease (with fluctuations) until the observation window reaches approximately 150 hours (6 days and 6 hours). After this, the value of the M-K distance becomes very small: this shows that the corresponding distributions are very close to each other.

We also studied the standard deviation and the mean of S(W 0,l ) as a function of l (not presented here). We observe that the mean becomes stable once l reaches approximately 1 week, at the same time as the M-K distance. This confirms that an observation window of one week is long enough to accurately estimate the distribution. The standard deviation, however, does not seem to converge as the observation window length increases, confirming that the distribution cannot be fully characterized. This is consistent with the distinction between the normal part of the distribution and extreme values.

Figure 4 shows the complementary cumulative distribution S(W 0,l ) for different values of l, up to l = 3 weeks, for the logins dataset. We can see that the shape of these distributions are similar, and get closer to each other as l increases. However, when we compare these distributions with the M-K distance (see Figure 5), the values obtained tend to decrease linearly which means that the distributions change at a constant rate. The values obtained for the mean and the standard deviation also do not stabilize. Therefore, we can not fully characterize this distribution. We however have confidence that the true shape of the distribution is not far from the one we observed. We considered two different definitions for a files' lifetime F. The first one is the same as for users' sessions lengths: we use a threshold and consider that a file is not present in the system if there is no consecutive queries for this file separated by less than this threshold. The second definition consists in considering the time interval between the first and the last query for a given file. In both cases, the shape of distributions F(W 0,l ) (not presented here) evolves strongly with l. We therefore conclude that this property cannot be characterized. The question which arises is whether this is because this property is intrinsically not stationary or because our measurement period is too short to be able to characterize it.

Conclusion

In this paper we introduced an empirical methodology for deciding when the bias induced by the finiteness of observation windows in dynamic systems becomes negligible. To illustrate the relevance of this approach, we applied it to the study of sessions lengths and files' life duration in two different datasets.

We have shown that we can characterize some properties, but not all. When a property can't be characterized, our methodology doesn't allow to determine if the observation window shall be increased or not since we don't know the stationarity of the property itself. It is interesting to note that, for a same dataset, some properties can be accurately characterized, and others not.

Figure 1 :

 1 Figure 1: Complementary cumulative distributions of S(W 0,l ) for different observation windows lengths in loglin scale, for the queries dataset.

Figure 2 :

 2 Figure 2: Complementary cumulative distributions of S(W 0,l ) for observation windows lengths l = 1 week and l = 10 weeks in lin-log scale, for the queries dataset.

Figure 3 :

 3 Figure 3: MK(S(W 0,l ), S(W 0,l max )) as a function of l, for the queries dataset.

Figure 4 :

 4 Figure 4: Complementary cumulative distributions of S(W 0,l ) for different observation windows lengths, for the logins dataset.

Figure 5 :

 5 Figure 5: MK(S(W 0,l ), S(W 0,l max )) as a function of l, for the logins dataset

de Amorim and Nadjet Belblida for valuable ideas and comments about this manuscript. This work was supported in part by the French ANR MAPE project, and by a grant from the Agence Nationale de la Recherche, with reference ANR-10-JCJC-0202. This research work is conducted and funded by the European Commission through the EULER project (Grant No 258307) part of the Future Internet Research and Experimentation (FIRE) objective of the Seventh Framework Programme (FP7).


Pim David Connolly

Van Leeuwen

Dr John Bailie
email: john.bailie@doctors.org

Amanda Black
email: amanda.black@qub.ac.uk

Liam Joseph Murray
email: l.murray@qub.ac.uk

Patrick Francis Keane
email: patrick.keane@belfasttrust.hscni.net

Anna Gavin
email: a.gavin@qub.ac.uk

Dr Pim J Van Leeuwen
email: p.vanleeuwen@erasmusmc.nl

Mr David Connolly

M B Bch

Prof J Liam

MD Murray

Mr Patrick

F Keane

Dr Anna Gavin Ffphm

Daily, monthly and seasonal variation in prostate

Keywords: Age, PSA, Season, Variation, Weather Age, PSA, Season, Variation, Weather

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Prostate specific antigen (PSA) remains the best available biomarker for the early detection of prostate cancer. [START_REF] Catalona | The PSA era is not over for prostate cancer[END_REF] One of the main limitations to the accuracy of PSA is its inherent variability, [START_REF] Soletormos | Biological variation of total prostate-specific antigen: a survey of published estimates and consequences for clinical practice[END_REF] with many factors known to cause transient elevations in PSA that are unrelated to prostate cancer. [START_REF] Tchetgen | The effect of prostatitis, urinary retention, ejaculation, and ambulation on the serum prostate-specific antigen concentration[END_REF][START_REF] Herschman | Effect of ejaculation on serum total and free prostate-specific antigen concentrations[END_REF][START_REF] Chybowski | The effect of digital rectal examination on the serum prostate specific antigen concentration: results of a randomized study[END_REF][START_REF] Pansadoro | Prostate-specific antigen and prostatitis in men under fifty[END_REF] As part of this variability, PSA has been shown to vary by season, with two studies from the French and Spanish sections of the European Randomized Study of Screening for Prostate Cancer (ERSPC) having contrasting results. [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF][START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] Specifically, Luján Galán et al. [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF] found a non-significant trend towards higher PSA levels during the autumn and winter, whilst Salama et al. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] found that PSA levels were higher during the summer, with a positive correlation between PSA level and insolation (hours of bright sunshine). The current study aimed to assess if the seasonality of PSA continued in a large non-screening population, and to examine the correlation of total PSA with meteorological data on a daily, weekly, monthly and seasonal basis.

Subjects and Methods

Study Participants

All men, aged 45-74 years, with an initial PSA <10.0 ng/ml, measured during a weekday in Northern Ireland (NI) between 1 st January, 2002 and 31 st December, 2006 were identified from a regional database of PSA tests. [START_REF] Connolly | Long term follow-up of men with elevated prostate specific antigen levels: a population based study[END_REF][START_REF] Connolly | Repeating an Abnormal Prostate-Specific Antigen (PSA) Level: How Relevant is a Decrease in PSA?[END_REF][START_REF] Connolly | Baseline prostate-specific antigen level and risk of prostate cancer and prostate-specific mortality: diagnosis is dependent on the intensity of investigation[END_REF] Initial PSA data only were included, whilst men with a prior diagnosis of prostate cancer were excluded.

Weather data for NI were obtained from the UK Met Office To assess if the weather parameters influenced the number of men who theoretically would be referred for biopsy if screening were performed, the number of men with a serum PSA ≥3.0ng/ml was calculated for each month.

Statistical Analysis

Variables are expressed as median and mean with 95% confidence intervals (CI). For statistical comparison, PSA values were logarithmically transformed to obtain a normal distribution. Weather parameters were normally distributed and so were not similarly transformed. Relationships were tested by the Pearson's product correlation coefficient.

Multivariate linear and logistic regression was used to test the relation of meteorological data with PSA and a PSA cut-off of 3.0ng/ml. A p-value <0.05 was considered significant. All analyses were performed with the Statistical Package for the Social Sciences software, version 16.0.

All patient identifiable information was removed before the research team accessed the data used in this study, and no patient contact was made during the study. Therefore, ethical approval was not sought.

Results

53 224 men were included. Overall, total PSA correlated with age (r=0.34, p<0.001), with mean and median PSA levels increasing with age category (Table 1). The number and percentage of men with PSA levels above 3.0ng/ml also increased with increasing age (p<0.001). There was seasonal variation in PSA levels, with median PSA levels being higher in spring compared to other seasons (1.18 vs. 1.10ng/ml, p=0.001). Mean age at initial PSA testing was slightly higher in springtime compared to other seasons (59.7 vs. 59.4 years respectively, p=0.075). Consequently, seasonal variation in PSA was not apparent when PSA levels were age-adjusted (p=0.112). The monthly mean and median PSA levels, as well as the proportion of men with PSA levels above 3.0ng/ml are graphically illustrated in Figure 1. In contrast, age-adjusted PSA levels did vary by weekday, with PSA levels on Thursday and Friday being higher than on Monday, Tuesday and Wednesday (median 1.16 vs. 1.10ng/ml respectively, p=0.004).

As demonstrated in Figure 2, meteorological data showed monthly variation in hours of bright sunshine, mean temperatures and rainfall (95% CI: sunshine 93.3-117.5 hours, temperature 8.5°C-10.5°C, rainfall 84.4-103.8 mm). Actual hours sunshine and mean temperatures were correlated (r=0.60, p<0.001), with a negative correlation between sunshine and rainfall (r=-0.362, p<0.001).

Overall, for the years 2002-2006, the age-adjusted total PSA was not correlated with monthly hours of sunshine (r=-0.004, p=0.429), mean temperature (r=-0.005, p=0.282) nor rainfall (r=-0.001, p=0.935). For 2006, the correlation between the age-adjusted PSA level and daily and weekly meteorological data was tested. No correlation was found for sunshine (r=-0.005, p=0.570), mean temperature (r=-0.002, p=0.844), rainfall (r=0.001, p=0.931), nor wind speed (r=0.007, p=0.382). When analyses were confined to men with PSA levels <4.0ng/ml, again no correlation was found between ageadjusted PSA levels and sunshine (r=-0.003, p=0.603), temperature (r=0.004, p=0.445) nor rainfall (r=-0.001, p=0.829).

Since PSA ≥3.0ng/ml is a widely used cut-off for prostate biopsy, multivariate logistic regression analysis was used to establish if men were at higher risk of having PSA ≥3.0ng/ml in relation to age and meteorological variation. Significant association was found for age [odds ratio (OR): 1.091, 95%CI 1.087-1.095, p<0.001], but not for sunshine (OR 1.00, 95%CI 0.99-1.01, p=0.789), mean temperature (OR 0.993, 95%CI 0.983-1.002, p=0.123), nor rainfall (OR 1.00, 95%CI 0.99-1.01, p=0.827).

Discussion

This study has confirmed that there is seasonal variation in total PSA levels, with men in the current study having higher PSA levels in spring compared to other seasons. Seasonal variation was however not apparent when PSA levels were age-adjusted.

Further, there was no direct correlation between PSA and any single meteorological parameter. In contrast, there was variation in age-adjusted PSA level by weekday, with total PSA being higher on a Thursday or Friday than other days, suggesting that there may be other social factors responsible for this variation as opposed to it simply being weather related. Finally, although the variations in PSA level noted in the current study, namely a median difference of 0.08ng/ml by season and 0.06ng/ml by weekday respectively, are statistically significant, they are not clinically significant. Therefore, contrary to the recommendations by Salama et al. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] there is no benefit in repeating an abnormal PSA level, and the decision to proceed to prostate biopsy should be independent of season or climatic conditions.

Strengths of the current study are the large number of participants and its populationbased design. The PSA data included represents all initial PSA tests <10.0ng/ml, performed in NI between 2002 and 2006 -this is therefore a heterogeneous group containing all men undergoing PSA testing, irrespective of their symptoms. Previous studies have demonstrated that the majority of men in NI had PSA testing performed for urinary symptoms (64.9%), 16.9% had testing for symptoms suggestive of advanced cancer such as bone pain, whilst only 18.0% were asymptomatic -this therefore more likely represents a standard clinical population than a pure screening study. [START_REF] Connolly | Long term follow-up of men with elevated prostate specific antigen levels: a population based study[END_REF] Further, meteorological data was available at a daily level as opposed to simply a seasonal or monthly level, allowing more in depth analysis.

There are a number of notable limitations. Firstly, the data are retrospective. Ideally, the effect of weather parameters on PSA levels should be assessed by a prospective longitudinal study. Given the small variations in PSA levels noted in the current study, this would require a large number of participants, with data also being collected on other factors which may affect PSA levels such as sexual activity. As this would require significant time and resources, and the impact on clinical practice is likely to be minor, the current study design may be an appropriate alternative. Secondly, clinical information was not available for men, which prevents inferences being made about how factors such as the reason for PSA testing, family history, medications, rectal examination findings, or prostate volume may have influenced PSA levels. Thirdly, different PSA assays were used during the study period, which, given their inherent variability, might not provide results that are directly comparable. Analyses were repeated assessing each individual year when assays may have changed and no significant correlation was identified between weather parameters and PSA. Further, previous analyses of the NI PSA database have not shown any systematic bias in PSA results from any laboratory. [START_REF] Connolly | Long term follow-up of men with elevated prostate specific antigen levels: a population based study[END_REF][START_REF] Connolly | Repeating an Abnormal Prostate-Specific Antigen (PSA) Level: How Relevant is a Decrease in PSA?[END_REF][START_REF] Connolly | Baseline prostate-specific antigen level and risk of prostate cancer and prostate-specific mortality: diagnosis is dependent on the intensity of investigation[END_REF] Other limitations of the data in the NI PSA database have previously been discussed. 9-11 Additionally, regional weather data only are presented. NI is a small region with similar weather patterns throughout the province, therefore local differences in weather parameters are unlikely to be significant. Furthermore, NI is a temperate region with lower temperatures and levels of sunshine than many countries; the PSA changes demonstrated may only be applicable to areas with similar climatic conditions. Finally, due to the possibility of there being a lag time between periods of bright sunshine to changes in PSA, the analyses were repeated assessing a lag time of one week and one month. Similar results i.e. no correlation was identified between any weather parameter and PSA levels.

The results of the current study differ from recent studies that demonstrated higher PSA levels in autumn or winter and in summer. [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF][START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF][START_REF] Vieth | Rise in prostatespecific antigen in men with untreated low-grade prostate cancer is slower during spring-summer[END_REF] Luján Galán et al. [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF] assessed PSA levels in 2147 men participating in the Spanish section of the ERSPC, and correlated these with meteorological data. They found a non-significant trend towards higher PSA levels in the autumn and winter, with age and temperature being independent predictors of having a PSA level ≥3.0ng/ml on multivariate analysis. As the magnitude of the PSA changes was small, Luján Galán et al. [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF] did not recommend any changes to biopsy indication based on climatic parameters. In contrast, using a similar study design in 8644 men from the French section of the ERSPC, Salama et al. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] found higher PSA levels during the summer, with a positive correlation between PSA and insolation. This resulted in a 23% higher risk of being referred for prostate biopsy during the summer, based on the ERSPC cut-off of 3.0ng/ml. Salama et al. therefore recommended 'confirming any isolated test result before biopsy, even more so if this was obtained in summer'. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] Veith et al. [START_REF] Vieth | Rise in prostatespecific antigen in men with untreated low-grade prostate cancer is slower during spring-summer[END_REF] assessed changes in PSA in men on active surveillance for prostate cancer, and found a lower increase or even a decrease in PSA levels in spring compared to other seasons. This was attributed, as it was in the study by Salama et al. 8 to be due to the potentially positive effects of vitamin D on prostate biology. The current study, in a much larger and heterogeneous population, showed higher PSA levels in spring with no correlation between PSA and meteorological parameters. One possible explanation for the differing results may be the different populations; certainly the population in NI is different from that in the ERSPC, with less than 20% of men being asymptomatic at the time of PSA testing. [START_REF] Connolly | Long term follow-up of men with elevated prostate specific antigen levels: a population based study[END_REF] However, the populations in the French and Spanish studies should have been similar, with both meeting the inclusion criteria for the ERSPC, and so, comparable results would have been expected. Another possible reason could be the temperate climate in NI compared to France or Spain. If PSA levels were related to insolation, then there may be a minimum level of sunshine exposure that is required to cause an elevation of PSA, which is not met in NI. As demonstrated in Figure 2, even at peak levels of sunshine, the duration was much lower in NI (150 to 200 hours per month) compared to the French study (300 to 350 hours per month). [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] Again, if this effect were true, then an even greater difference would have been expected in the Spanish study, [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF] and in fact, the converse was true, PSA levels were higher in cold weather conditions.

A more likely explanation to the differing results between the studies may be that other unmeasured factors were involved which may cause higher PSA levels and are related to season. Firstly, as the seasonal variation was not apparent when PSA levels were age-adjusted, this may simply be an age-related phenomenon i.e. slightly older men were more likely to attend for PSA testing during springtime. Further, the variation in age-adjusted PSA levels in NI by weekday suggests that there may be social reasons involved as opposed to a true biological basis. One possible factor is sexual behaviour and ejaculation. Ejaculation has been shown to cause transient rises of PSA. [START_REF] Tchetgen | The effect of prostatitis, urinary retention, ejaculation, and ambulation on the serum prostate-specific antigen concentration[END_REF][START_REF] Herschman | Effect of ejaculation on serum total and free prostate-specific antigen concentrations[END_REF] Tchetgen et al. [START_REF] Tchetgen | The effect of prostatitis, urinary retention, ejaculation, and ambulation on the serum prostate-specific antigen concentration[END_REF] demonstrated in 64 men aged 49-79 years, that PSA had increased by 0.8ng/ml at 1 hour, 0.3ng/ml at 6 hours and 0.2ng/ml at 24 hours post-ejaculation. They also found that higher baseline PSA values tended to increase by more following ejaculation and that there was a significant positive correlation between the patients' age and the PSA increase following ejaculation. [START_REF] Tchetgen | The effect of prostatitis, urinary retention, ejaculation, and ambulation on the serum prostate-specific antigen concentration[END_REF] Similarly, Herschman et al. [START_REF] Herschman | Effect of ejaculation on serum total and free prostate-specific antigen concentrations[END_REF] found in 20 men with mean age 59 years, a mean increase in PSA of 0.3ng/ml at 1 hour, 0.1ng/ml at 6 hours and 0.1ng/ml at 24 hours post-ejaculation. Sexual behaviour in humans does show seasonal variation. [START_REF] Roenneberg | Annual rhythm of human reproduction: I. Biology, sociology, or both?[END_REF][START_REF] Roenneberg | Annual rhythm of human reproduction: II. Environmental correlations[END_REF][START_REF] Cummings | Additional confirmation for the effect of environmental light intensity on the seasonality of human conceptions[END_REF][START_REF] Foster | Human responses to the geophysical daily, annual and lunar cycles[END_REF][START_REF] Carlsen | Effects of ejaculatory frequency and season on variations in semen quality[END_REF] This is apparent in many European countries, [START_REF] Roenneberg | Annual rhythm of human reproduction: I. Biology, sociology, or both?[END_REF] with peak conception rates occurring in April / May. Conception rates also correlate with increasing exposure to sunlight and with temperature. [START_REF] Roenneberg | Annual rhythm of human reproduction: II. Environmental correlations[END_REF][START_REF] Cummings | Additional confirmation for the effect of environmental light intensity on the seasonality of human conceptions[END_REF] Further, the frequency of sexual activity, rate of sexually transmitted diseases and the sale of contraceptives are all seasonal, [START_REF] Foster | Human responses to the geophysical daily, annual and lunar cycles[END_REF] with Carlsen et al. [START_REF] Carlsen | Effects of ejaculatory frequency and season on variations in semen quality[END_REF] demonstrating higher rates of ejaculation during springtime in Danish men. Therefore, seasonal variation in PSA levels may be a reflection of the variation in ejaculation frequency in the studied populations. Interestingly, Roenneberg and Aschoff found that conception rates are decreased at extremes of temperature, [START_REF] Roenneberg | Annual rhythm of human reproduction: II. Environmental correlations[END_REF] which, if there was an associated decrease in frequency of ejaculation, may explain the lower levels of PSA in Spain during the summer and the subsequent higher levels in autumn and winter. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] seasonal variation in PSA. Physical activity, particularly bicycle riding, can be associated with a transient rise in PSA, [START_REF] Oremek | Physical activity releases prostate-specific antigen (PSA) from the prostate gland into blood and increases serum PSA concentrations[END_REF][START_REF] Crawford | The effect of bicycle riding on serum prostate specific antigen levels[END_REF] particularly in older men and those with elevated baseline PSA levels. Further, physical exercise has been shown to have seasonal variability, with decreased levels of exercise during the winter or in extremes of weather. [START_REF] Tucker | The effect of season and weather on physical activity: A systematic review[END_REF] This has been shown specifically in older people, with exercise levels being independently correlated with day length, sunshine and mean temperature. [START_REF] Sumukadas | Day length and weather conditions profoundly affect physical activity levels in older functionally impaired people[END_REF] Irrespective of the cause of seasonal variation of PSA, the clinical application of this is more straightforward. As demonstrated in the previous studies and illustrated in Figure 1, [START_REF] Galán | Impact of the weather on the serum levels of prostatic specific antigen [PSA[END_REF][START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF][START_REF] Vieth | Rise in prostatespecific antigen in men with untreated low-grade prostate cancer is slower during spring-summer[END_REF] the actual variation in mean and median PSA by season is of a small magnitude, and although statistically significant, is not clinically significant. If the decision to proceed to prostate biopsy is based on the underlying risk of prostate cancer as opposed to a PSA value being above or below an arbitrary cut-off, then these variations in PSA by season or weekday are irrelevant. Contrary to the recommendations by Salama et al. [START_REF] Salama | Seasonality of serum prostate-specific antigen levels: a population-based study[END_REF] , there is therefore no benefit in repeating an abnormal PSA level, and the decision to proceed to prostate biopsy should be independent of season or climatic conditions.

In conclusion, this study has confirmed that there is seasonal variation in total PSA levels, with men in the current study having higher PSA levels in spring compared to other seasons. As the seasonal variation was not apparent when PSA levels were age-

(

  http://www.metoffice.gov.uk/climate/uk/datasets/index.html). Weather information including monthly minimum, maximum and mean temperatures ( o C), duration of bright sunshine (hours), actual rainfall (mm) and mean wind speed (knots) were obtained from January 2002 until December 2006. Daily meteorological data were available for 2006 only.

Figure 1

 1 Figure 1Variation in total prostate specific antigen (PSA) levels and percentage of men with PSA ≥3.0 ng/ml by month.

Figure 1a Total PSAFigure 1b Figure 2

 1b2 Figure 1a Total PSA Figure 1b Percentage with PSA>3.0ng/ml

Figure 2a Figure 2b Figure 2c

 2a2b2c Figure 2a Actual sunshine (hours) Figure 2b Temperature ( o C) Figure 2c Rainfall (mm)

Table 1

 1 Patient characteristics; age, total prostate specific antigen (PSA) and number with PSA>3.0ng/ml by age category

	Tables
	Age	Number of	Total PSA (ng/ml)	PSA >3.0ng/ml
	(years)	men (%)	Mean (95% CI)	Median (IQR)	(%)
	45-50	8971 (16.9)	1.02 (0.99-1.04)	0.70 (0.50-1.11)	371 (4.1)
	51-55 10167 (19.1)	1.26 (1.24-1.29)	0.90 (0.50-1.50)	787 (7.7)
	56-60 11108 (20.6)	1.56 (1.53-1.59)	1.00 (0.60-1.90)	1422 (12.8)
	61-65	9604 (18.2)	1.82 (1.78-1.85)	1.20 (0.70-2.30)	1698 (17.7)
	66-70	7541 (14.2)	2.20 (2.15-2.24)	1.50 (0.80-2.91)	1877 (24.9)
	71-75	5833 (11.0)	2.48 (2.43-2.54)	1.80 (0.90-3.50)	1791 (30.7)

Acknowledgement

The authors wish to thank James Vincent Smith from the UK Met Office for providing the meteorological data. This research was funded by the Northern Ireland Research and Development Office and by the Men Against Cancer charity. The Northern Ireland Cancer Registry is funded by the Public Health Agency, Northern Ireland. The funding bodies had no role in study design, data collection, data analysis, manuscript preparation or the decision to proceed to publication.

This research was funded by the Northern Ireland Research and Development Office and by the Men Against Cancer charity. The Northern Ireland Cancer Registry is funded by the Public Health Agency, Northern Ireland. The funding bodies had no role in study design, data collection, data analysis, manuscript preparation or the decision to proceed to publication.

Conflict of interest

There is no conflict of interest for any author.