Distributed Intrusion Detection Systems for Enhancing Security in Mobile Wireless Sensor Networks *

1. Introduction

A Wireless Sensor Network (WSN) usually consists of a number of different modalities sensors that, when combined with a microprocessor and a low-power radio transceiver, form smart network-enabled nodes. The sensed data can be related to different applications but in terms of capabilities all the nodes cooperating in the WSN can be assumed as homogeneous. A first level of cooperation may be viewed just to route collected data outside the sensed area to a fixed infrastructure (the sink nodes) where it is processed. Concerning the applications, medical services, battlefield operations, crisis response, disaster relief, environmental monitoring, premises surveillance, robotics are included. Due to the critical environment where such kind of networks may be used, as a second level of cooperation we are interested in investigating security issues. Such kind of networks are in fact frequently subject to attacks by malicious intruders. Intrusions take place through a sequence of actions that aim to subvert the network system. There are many vulnerabilities and threats to a mobile WSN. They include outages due to equipment breakdown and power failures, non-deliberate damage from environmental factors, physical tampering, and information gathering. In the following we summarize some of them (see [27] for an extended survey).

Passive Information Gathering: When communications are in clear or an intruder has got in some way the key for decryptions, it can easily pick off the data stream.

The category of attacks outlined in 1. and 2. are passive attacks, while the remaining ones are called active attacks. This is due to the fact that the former ones do not produce a modification of the traffic network. They are usually addressed by encryption mechanisms that obscure the traffic to unauthorized sensors. A lot of work has been done in this direction in order to reduce the complexity of the applied algorithms and hence the consumed energy (see for instance [5, 6]). In this paper we are interested in the second kind of attacks where the detection of malicious behaviors can be locally detected by observing the traffic over the network. We focalize our attention on Intrusion Detection Systems (IDSs) that analyze the observable behaviors of the systems (see for instance [28, 10, 26, 14, 19]) in order to detect attacks.

Intrusion detection techniques are successfully applied to wired networks; however, most of them are not suitable for the wireless context. The inadequacy of standard IDS in WSNs is a consequence of the open medium access, of the dynamic topology, of the cooperation needed among sensors (collaborative algorithms) and the lack of a fixed topology where all information flows. The detection of an attack may not be possible only considering the traffic locally sent/received by a sensor. Therefore, there must be some form of correlation among the data received by the sensors. This will permit to discover attacks that are scattered over several sensors.

Besides the problems mentioned above, in mobile WSNs the detection has to address the problems imposed by the limited battery, restricted computational power of the sensors, low bandwidth, and slower links. Moreover, sensors mobility can complicate the detection since the correct behavior of sensors is location dependent (i.e., the sensors correct behavior can change over time). In summary, an IDS for a mobile WSN should:

(i)

be decentralized;

(ii)

minimize the traffic overhead;

(iii)

address the mobility problem.

We use a specification-based approach to provide intrusion facilities into mobile wireless sensor networks. Specification-based IDSs [14, 19, 26] use some kind of formal specification to describe the correct behavior of the system. The detection of violations involves monitoring deviations from the formal specification, rather than matching specific well-known attacks. The advantage of this approach is the ability to detect previously unknown attacks at the expense of providing a formal specification of correct information flows.

In this work we automatically generate distributed-specification-based IDSs for mobile WSNs. In our system model each sensor s plays a role r that defines the possible messages sent and/or received by s. We use an automaton (in the following referred to as Global Automaton) as the basis in building a specification-based IDS. The Global Automaton defines an ordering among the roles messages and their correct format. We have developed an algorithm that given a Global Automaton produces a set of local automata each of them assigned to a role. For instance, in Fig. 1(a) we draw a Global Automaton decomposed into four local automata each of them assigned to a role. A local automaton (related to a role r) constitutes the basis in building a filter that can be used to monitor each sensor playing the role r. For example, in Fig. 1(b) we show nine sensors {S1, …, S9} each of them playing a different role among {1, …, 4} and monitored by the related filter {F1, …, F4}. Each filter locally monitors the messages sent/received by its sensor and locally detects violation of the policy expressed by the Global Automaton. ¹

OPEN IN VIEWER

Figure 1.

Specification and monitoring.

In order to validate and to explain this approach in more detail we apply it to a recently proposed routing protocol, CoP [23], for mobile WSNs. Note that, while the formal specification directly derives from the considered protocol, the method is completely independent of it. In fact, it can be used on any kind of protocol for mobile WSNs in order to add security aspects.

1.1. Related Work

In the field of intrusion detection systems on mobile WSNs few works appeared in the literature. The mobility issue is typically not addressed and moreover specific kind of attacks are considered separately. In [8], an anomaly approach based on self-organized criticality (SOC) and Hidden Markov models to detect data inconsistencies is proposed. This approach is developed based on the structure of naturally occurring events. With the acquired knowledge distilled from the self-organized criticality aspect of the deployment region, it applies a hidden Markov model. It lets sensor networks adapt to the dynamics norm in its natural surrounding so that any unusual activities can be singled out. Another paper formulates the attack-defense problem by means of the game theory and use the Markov Decision Process to predict the most vulnerable sensor nodes [1]. It formulates the attack-defense problem as a two-player, nonzero-sum, non-cooperative game between an attacker and a sensor network. It shows that this game achieves Nash equilibrium and thus leads to a defense strategy for the network. Then, it uses the Markov Decision Process to predict the most vulnerable sensor node. Finally, it uses an intuitive meter (nodes traffic) and protects the node with the highest value of this meter. Indeed, wireless sensor networks are susceptible to many forms of intrusion. In wired networks, traffic and computation are typically monitored and analyzed for anomalies at various concentration points. This is often expensive in terms of networks memory and energy-consumption, as well as its inherently limited bandwidth. Wireless sensor networks require a solution that is fully distributed and inexpensive in terms of communication, energy, and memory requirements. In order to look for anomalies, applications and typical threat models must be understood. It is particularly important to understand how cooperating adversaries might attack the system. The use of security groups may be a promising approach for decentralized intrusion detection [27]. Apart from those more general approaches, some papers provide intrusion detection techniques for particular operations, [11] describes a distributed algorithm, BoundHole, building routes around the routing holes, which are connected regions of the network with boundaries consisting of all the stuck nodes. It shows that hole-surrounding routes can be used in geographic routing, path migration, information storage mechanisms, and identification of regions of interest. [9] proposes a general scheme to detect localization anomalies that are caused by adversaries. It formulates the problem as an anomaly intrusion detection problem, and proposes a number of ways to detect localization anomalies. [24] describes an intrusion detection technique that uses information on both the network topology and the positioning of sensors to determine what can be considered malicious in a particular network place. The technique relies on an algorithm that automatically generates the appropriate sensor signatures. It applies that approach to an intra-domain distance-vector protocol and reports the results of its evaluation. Moreover, there are some papers applying fault-tolerant technologies in providing network security. In [4], secure multi-path routing to multiple destination base stations is designed to provide intrusion tolerance against isolation of a base station. Also, anti-traffic analysis strategies are proposed to help disguise the location of the base station from eavesdroppers. [7] targets the identification of faulty sensors, and detection of the events reachability in sensor networks with faulty sensors. It proposed two algorithms for faulty sensor identification and fault-tolerant event boundary detection. These algorithms are localized and scaleable for WSNs. In [29] the authors propose a statistical approach in order to detect attacks. Each cluster is equipped with a node that contains the rules in order to perform the detection. However, these statistical solutions have a high false alarm rate hence wasting energy in order to deliver the attacks. Moreover, a single sensor that performs all the detection activities will consume its energy before other sensors and the monitoring activities will soon be deactivated. Our approach aims to distribute the intrusion detection activities in order to prolong the monitoring. In [26] an intrusion detection scheme based on extended finite state machines is presented. They need to model one automaton for each link of the network in order to specify the correct behavior among all the connections of ad hoc networks. A backward checking algorithm detects run-time violations of this specification. With respect to it, our approach for WSNs, massively divide the workload of the monitoring activity among all the sensors participating in the given protocol. Moreover, as input, we do not need to model each link of the network but just a Global Automaton that specifies the behavior of the given protocol. Then, such an automaton is automatically divided and distributed among sensors according to their actual roles in the network.

1.2. Outline

The paper is organized as follows. In the next section we introduce some notation coming directly from the wired environment where IDSs usually are successfully applied. We point out the basic difference with the wireless and mobile environment that must be considered for managing WSNs. In Section 3, the CoP protocol is introduced. We make use of it in order to better explain our approach at work. CoP is in fact a protocol designed for routing on mobile WSNs. Our aim, while describing our method, is to enrich the protocol by means of security issues. Section 4 gives details about the formalization needed to describe the system interactions defined by the CoP protocol while Section 5 makes explicit the state machine needed as input by our tool in order to describe the desired behavior of the sensor network. We show how our tool can be tuned in order to output different levels of security. Section 6 describes the heavy solution where all the sensors of specific areas monitor each other. In section 7, instead, we show how the same kind of monitoring can be performed with the minimum overhead by means of a subdivision of the monitoring according to the sensor roles. Section 8 is devoted to experimental results. It shows the overhead obtained on the CoP protocol. Finally, Section 9 provides conclusive remarks.

2. From the Wired to the Wireless Environment

In this section we introduce some basic definitions and the notation that comes directly from the wired and static environment. As described in the introduction, this is due to the fact that intrusion detection systems are usually more suitable for those kinds of networks. Next, we point out the main properties that must be considered when moving to a mobile and wireless environment.

A wired system S is composed by a set of entities {C₁,…, C _n }, communicating by means of the send(sender, receiver, msg) and receive(senderꞋ, receiverދ, msgދ) primitives. sender, receiver, senderꞋ and receiverދ are formal parameters that take as value a component in S. msg and msgދ are formal parameters that take values in the domain of all possible entities messages values. The send(C, CꞋ, m) (receive(C, CꞋ, mދ)) primitive invocation is used by an entity C(Cދ) in order to send (receive) the message m (mދ) to (from) the entity Cދ (C). A communication is then achieved whenever a send invocation is eventually followed by the related receive invocation. In the following we assume that a global system clock exists. However, this assumption is needed only for modeling purposes and it will be relaxed in Section 7.

Given a system S, the send and receive primitives invocations define an architectural system trace, i.e., a string containing all send/receive invocations performed by the entities of the system.

Definition 1. Let S = {C ₁ , …, C _n ) be a system. Let T be a string p ₁ p ₂ p _i +1… . T is an architectural system trace of S if the following properties hold:

(i)

∀k  0, p _k is either a send or a receive invocation performed by an entity C of S;

(ii)

if i < k then t(p _i )  t(p _k ), where t(p) denotes the global system time at which the invocation occurs.

The primitives invocations performed by an entity produce an entity local trace, i.e., all invocations locally observed on a single entity:

Definition 2. Let S = {C ₁ , …, C _n ) be a system. Let C be an entity of S . T _ C = p 1 c p 2 c ⋯ p k c p k c + 1 ⋯ is an entity local trace of C if ∀ k ≥ 0 , p k c is either a send or receive invocation performed by C.

In the following we define the merge operation among entity local traces.

Definition 3. Let S = {C₁, C ₂ … C _n ) be a system. Let C₁ and C ₂ be two entities of S . L e t T C 1 = p 1 c 1 p 2 c 1 p 3 c 1 ⋯ p k c 1 p k + 1 c 1 ⋯ and T C 2 = p 1 c 2 p 2 c 2 p 3 c 2 ⋯ p j c 2 p j + 1 c 2 …be the local entity traces of C₁ and C₂, respectively. A merge trace T _{C 1} ⊕ T _{C 2} is a new trace defined by p₁p₂p₃ … p _t p_t+1… where: (i)

p _t appears inT _{C 1} ⊕ T _{C 2} if and only if p _t appears either inT _{C 1} orT _{C 2} :

(ii)

for each p _i and p _j appearing either inT _{C 1} orT _{C 2} if t(p _i ) < t(p _j ) then p _i appears before p _j inT _{C 1} ⊕ T _{C 2} .

In our system model each running entity C _i defines an entity local trace T _{C 1} and the merging of all entity local traces define an architectural system trace T.

For the ease of notation we denote the invocation send(C₁, C₂, m₁) (receive(C₃, C₄, m₂)) with !m₁_C₁_C₂ (?m₂_C₃_C₄), i.e., we substitute send (receive) with the symbol!(?) followed by the message m₁ (m₂) and the sender (receiver). Moreover, we denote with p ^C an invocation performed by C that can be either of the form !m₁_C_C₁ or ?m₂_C₂_C.

This system model, characterized by send and receive invocations, has been shown to be flexible enough to model different distributed systems interactions and communication patterns. Messages can be structured as needed for security and modeling purposes (e.g. a message can be a service invocation, hardware signals, control signals).

Generally speaking, we assume that each entity C implements an interface. The C interface contains each C required and provided service (if any) described using the notation !serviceName (listOf Parameters).returnType and ?serviceName1 (listOf Parameters1).returnType1, respectively. The former means that C is a client of the serviceName service having the listOf Parameters formal parameters and the returnType returned value type. The latter means that C is a server of the serviceName1 service. The listOf Parameters is a sequence of the type T₁D₁X₁, …, T _n D _n X _n , i.e., a sequence of parameter declarations. A parameter declaration T _i D _i X _i can be described as follows. T _i is a label that can take one of the following values: in and out. in specifies that the parameter X _i is an input service parameter (i.e., it must be provided to the service). out specifies that X _i is an output service parameter (i.e., it contains an output after the service execution). D _i is the domain of X _i and defines the set of values that it can take. Finally, a service returnType is the set of values that the service can return to the environment.

The entities then communicate by means of services invocation. There are three main types of entities communication models [3]: (i)

synchronous;

(ii)

asynchronous;

(iii)

deferred synchronous.

As it is implemented in the CORBA interface definition language the type of service invocation is specified by means of a label that is prefixed to the service declaration. However, for the sake of brevity we do not show such detail in all entities interfaces described in this paper.

In the following we show how this architectural model can be mapped to our system one. Let C (C′) be an entity that requires (exports) the service ! (?) serviceName (T₁D₁X₁, …, T _n D _n X _n ).returnType. Synchronous and deferred synchronous service invocations from the client C to the server C′ are modeled with the following sequence of send and receive invocations:

!m_C_C′ where m = serviceName(x₁, …, x _n ), and x _i ∊ D _i , (i.e., the client invocation);

?m_C_C′ (i.e., the server incoming request);

!m′_C′_C where m′ = serviceName. and serviceName. encodes the C′ outgoing response (i.e., the server answer);

?m′_C′_C (i.e., the client incoming result).

A asynchronous service invocation is modeled as above without steps 3 and 4.

In this case the structure of messages sent by means of our primitives is strictly related to the entity interfaces. If C requires the service !serviceName (T₁D₁X₁, …, T _n D _n X _n ).returnType then C can send a message serviceName(X₁, …. X _n ), where X₁, … X _n are suitably instantiated and can receive the incoming message serviceName. (i.e., the service invocation result) belonging to the set returnType. Symmetrically, If C′ provides the service ?serviceName1 (T₁D₁X₁, …, T _n D _n X _n ).returnType1 then C′ can receive a message serviceName1(X₁, …, X _n ), where X₁, … X _n are suitably instantiated and can send the outgoing message serviceName1. (i.e., the service invocation result) belonging to the set returnType1. Therefore from now on messages can have the above structure and are suitably instantiated when they are sent.

Note that the above system model implicitly assumes that: (i)

both the sender and the receiver of a message are known;

(ii)

an entity cannot change its location;

(iii)

an entity cannot change its interface and behavior.

In the process of adapting the previous model to mobile WSNs we match entities with sensors and entity interfaces with roles. Clearly the previous assumptions cannot be now guaranteed. The more evident is (ii) since we are in a mobile environment. For (i), due to the random and mobile environment, a sensor can not know its neighbors at each time unless it wastes energy in control messages. Concerning (iii), in general, in WSNs sensors change their behavior according to their actual role in the network, i.e., a sensor can change the messages it can send/receive. The idea is usually to guarantee a balanced energy-consumption of all the sensors participating in the protocol. As we are going to see in the next section, in the CoP protocol [23] the roles change depending on the actual positions of the sensors. We therefore remove assumptions (i), (ii) and (iii), hence obtaining a framework able to work with all those protocols for WSNs in which sensors have different behaviors according to a predetermined set of roles. The security aspects that we want to guarantee by this method concern the monitoring of the normal behavior of the sensors participating in a given protocol. In order to better describe and validate our new approach, we apply it on a protocol designed for mobile WSNs, CoP [23]. Before giving the details of our approach according to the CoP protocol, in the next section we first present how it routes messages on random instances of uniform sensors distribution.

3. Connectionless Probabilistic (CoP) Routing

The CoP protocol [23] for routing on mobile WSNs assumes a random uniform distribution of sensors inside a given area. The only thing that each sensor needs to know in order to participate in the CoP protocol is its own location, the location of the sink (the fixed infrastructure outside the sensed area (see Fig. 2)) and a further parameter called grid unit.

OPEN IN VIEWER

Figure 2.

Multihop routing from the area of interest (shaded area) to the sink in a sensors field.

In such a model, a communication session begins when a sensor needs to inform the sink about some collected information of interest. Since computing operations are cheaper than transmissions (see for instance [12, 22]), aggregating information is desired. As in the great majority of the protocols that are proposed, the aim is to efficiently route the message towards the destination, using the least possible energy in order to extend the lifetime of the whole network. To this end, the standard multihop approach was adopted here as well. Location-awareness routing protocols for adhoc networks typically assume some kind of awareness of a greater topology among the distributed sensors. Quite usually this means that in order to make local decisions, the nodes are required to know their neighbors' positions as well as their own. This is achieved by exchanging control messages that consume considerable amounts of energy in large, densely deployed, mobile networks. The key idea of the CoP protocol is that the saving of energy is achieved not only by choosing an appropriate path between source and destination pairs but also by eliminating all the transmissions usually needed by other protocols to choose the next hop node or just to communicate the positions of the nodes (see for instance [2, 18, 20]). Furthermore, since we assume mobility in our model, the determination of static paths or the knowledge of the neighbors' locations could be useless in many cases where real-time connectionless communication is required.

In CoP, clustering methods are used to reduce the number of needed hops to establish the required communication session and hence reduce the average routing time. To this end, a two-level communication model was proposed where each node is itself candidate to be either a normal sensor or a clusterhead.

The protocol assumes a virtual infrastructure represented by a grid covering the sensed area. Messages are then routed on the grid nodes emulated by the sensors. The knowledge of the grid is determined by considering the sink as a grid node at the border of the area of interest and according to the fixed grid unit. Since the sensors are randomly spread on the area of interest, a distortion parameter called ds is fixed to be the maximum distance from a virtual grid node (VGN) where the real sensor has to reside in order to candidate itself and become a clusterhead (see Fig. 3). Roughly speaking, this means that all the sensors in the fixed range of a VGN “believe” they are grid nodes. All the other remaining sensors are themselves associated to some VGN just through the minimum distance, hence determining an area (A _VGN ) associated to each VGN. Note that if more than one sensor resides inside a described circular area, a standard local “leader election” is performed [21] in order to elect the clusterhead. In [23] it is formally described how to estimate the right value for ds in order to fix with high probability that at least one sensor resides inside each A _VGN . The configuration can easily change with time, according to the degree of the sensors' mobility but each one can decide which is the closest clusterhead-area or if it is a clusterhead itself. If a sensor is a clusterhead, it can transmit the collected information to the next clusterhead-area in order to reach the sink. Since the transmission needed power of a non-clusterhead node is less than the one needed by a clusterhead, in order to prolong the lifetime of the entire network, a sort of rotation in the roles could be convenient. If the network is characterized by high mobility, then every node frequently changes its status from clusterhead to non-clusterhead and vice-versa. This depends on the actual location of the sensor and therefore mobility works in favor of a fair and uniform energy consumption in the CoP protocol.

OPEN IN VIEWER

Figure 3.

Multihop routing from the area of interest (shaded area) to the sink in a sensors field using the virtual grid. The empty circles represent the area associated to each virtual grid node. Every node inside such an area participate in a local leader election in order to become clusterhead.

In the field of location-awareness and clustering protocols like CoP, we model a mobile WSN by a set of sensors AH = {s₁, s₂, …, s _k }. Let L ? AH be a subset {l₁, l₂, …, l _m } of sensors identifying the clusterhead of a given protocol P. In other words, the sensors in L characterize a set of areas Ar = {Ar₁, Ar₂, …, Ar _m } (clusters) where each area Ar _i represents the portion of the sensed area where the corresponding l _i plays the clusterhead role. There can be different roles according to P, let R = {C₁, C₂,…,C _m } be the set of roles. Each C _i has associated an interface that characterizes all messages sent/received by sensors playing that role.

In wireless sensor networks we refine the semantic of invocation. An invocation of the form !m_C_C₁ means that a sensor playing the role C inside some area Ar _i ∊ Ar sends the message m to all sensors residing in the same area Ar _i playing the role C₁. An invocation of the form ?m₁_C_C₃ means that all sensors playing the role C₃ inside some area Ar _i ∊ Ar receive the message m₁ sent by a sensor playing the role C inside Ar _i . Due to the open medium access, in the system model for WSNs each sensor residing in a given area belonging to Ar can sniff all the traffic occurring inside such an area. In this model each sent invocation is then immediately followed by the related receive. Therefore, in our policies, it is redundant to model the reception of a message that is assumed to follow the related send.

In some invocation we can use the symbol ‘*’ instead of a role C whenever the invocation is performed by an unknown role. We can associate to each role a set of variables that are used in the policies definition. Moreover, we specify when a role is played by exactly one sensor or by different sensors. ²

In general a sensor s can change its role from C to C′ as a consequence of:

(i)

changing the location;

(ii)

the messages locally sent/received by s.

According to the previous definitions, we can recognize one architectural system trace (see Definition 1) for each defined area A _{r i} . Each running sensor s _i of the area A _{r i} has a role R _j and defines an entity local trace T _{C i} . The merge of such local traces generates the architectural system trace of A _{r i} .

In Fig. 4 we show the four types of roles that each sensor can play and the corresponding interfaces according to the described CoP protocol. Considering each A _VGN we define the Out-range, the In-range, and the Clusterhead roles that are played by sensors residing in it, and the Extern role representing the sensor playing the cluster-head role inside an adjacent A _VGN .

OPEN IN VIEWER

Figure 4.

The CoP roles.

The role Out-range models a sensor s located in a position that is inside the A _VGN but at a distance greater than ds from the corresponding VGN. This role defines an interface composed by the ?pos(double x, double y).void and !send(double x, double y, unt dest, char [] msg).void asynchronous services. ?pos(double x, double y).void specifies that the sensor s can receive the incoming message pos(double x, double y) used to set up its initial position. The parameters double x and double y are suitably instantiated with the coordinates of s inside the virtual grid. !send(double x, double y, unt dest, char [] msg).void specifies that s can send the message msg towards the sink dest. The parameters x and y are instantiated with the current position of s and dest is an integer that denotes a sink.

The role In-range models a sensor s located in a position inside an A _VGN and at a distance at most ds from the corresponding VGN. This role adds to the Out-range role the following services: !leader(double x, double y).void, ?no - leader().void and ?leader (double x, double y).void. The service !leader(double x, double y).void specifies that the sensor s can send the message leader(double x, double y) in order to become clusterhead. The parameters double x and double y are suitably instantiated with the coordinates of s inside the virtual grid. ?no - leader().void is implemented by s in order to accept the notification sent by the clusterhead when it leaves its role. ?leader(double x, double y).void is used by s to receive the notification of a sensor s′ that requires to be clusterhead. The parameters double x and double y are suitably instantiated with the coordinates of s′.

The role Clusterhead is played by a sensor s providing the forward of messages towards the right sink. This role defines the following services: !no - leader().void, ?forward(double x, double y, int dest, char [] msg).void, !forward(double x, double y, int dest, char [] msg).void and ?send(double x, double y, int dest, char [] msg).void. The !no - leader().void service specifies that the sensor s can send the asynchronous message no - leader() to the environment. This message is sent by s in order to leave its cluster-head role due to its movement or to its draining battery. ?forward(double x, double y, int dest, char [] msg).void implements the service used by s in order to receive the message msg. This message is forwarded by a clusterhead s′ that resides in an area surrounding the one of s. The parameters x and y denotes the position of the clusterhead s′ and dest encodes the sink. The service !forward(double x, double y, int dest, char [] msg).void is used by s in order to forward the message msg towards the sink dest. The parameters x and y denotes the position of s. The service ?send(double x, doubley, int dest, char [] msg).void is used by s in order to receive a message msg sent by a sensor s′ residing inside the A _VGN . The parameters x and y denote the position of s′ and dest is an integer that denotes a sink.

The role Extern models one of the clusterheads surrounding the current A _VGN .

All roles have associated the real numbers x and y used to store the current position of the sensor and the string role that encodes the current role played by the sensor.

5. The Formal Specification: Global Automaton

We use a Global Automaton to define the correct interactions among sensors (i.e., the correct architectural system traces).

Definition 4. A Global Automaton is 5-tuple A = (Q, q₀, I, δ, P) where:

(i)

Q is a finite set of automaton states;

(ii)

q₀ ∊ Q is the initial state;

(iii)

I is a finite set of input symbols; (iii) δ : Q × I → Q is a transition function; (iv) P = {P₁. P₂, …, P _n } is a finite set of predicates.

We use integers to denote state names, in particular 0 will be always used to denote the initial state q₀. I is a finite set of invocations. δ represents the policy that defines the correct sequence of invocations (i.e., the correct exchange of messages among sensors). Each transition rule q′ = δ(q, p), with q, q′ ∊ Q, and p ∊ I, has associated exactly one predicate in P denoted with P(q, q′)(p). ³ P(q, q′)(p) (e.g. p = !m_C_C′) is a boolean expression evaluated on the basis of the states q and q′ and the message m. P(q, q′)(!m_C_C′) acts like a transition precondition, i.e., when it is true the related transition is allowed, otherwise the transition is not permitted.

In the following we introduce definitions related to our Global Automaton, i.e., the invocations acceptance criterion and the language it recognizes.

Definition 5. A Global Automaton A = (Q, q ₀ , I, δ, P) parses an architectural system trace T = p₁, …, p_i, … one symbol at a time from left to right. Let q_i- 1 ∊ Q be the current state of A and let p _i ∊ I be the next symbol to read. A accepts p _i if there exists a transition rule q _i = δ(q _i - 1, p _i ) defined in A and P(q_i- 1, q _i )(p _i ) is true. In this case we say that the symbol p _i can be accepted by means of the A-rule q _i = δ(q _i - 1, p _i ).

Definition 6. Let A = (Q, q₀, I, δ, P) be a Global Automaton and T = p₁, …, p_i, … be an architectural system trace. Let q₀be the starting state of A and p₁be the first symbol to read. A accepts the sequence T if for each current state q_i − 1 and next symbol p _i , A accepts p _i , q _i = δ(q_i- 1, p _i ) is the new state of A and p_{i +}1the next symbol to read.

Definition 7. The language ℓ(A) recognized by A = (Q, q₀, I, δ, P) is composed of all traces accepted by A.

We point out that this acceptance criterion permits to recognize finite and infinite sequences of symbols.

We can annotate a rule (e.g. q _i = δ(q_i-1, !m_C_C′)) with a piece of code composed of a sequence of instructions. ⁴ We use instruction in order to set the role variables. ⁵ Variables store the current sensor position and the role played by it.

They can be updated on the basis of: (i)

the m message;

(ii)

the role C;

(iii)

the current state q.

A Global Automaton models the correct exchange of messages among sensors playing different roles and residing in (i)

the same area; or

(ii)

an adjacent area.

Predicates can be used to define the correct messages format so that some kind of attacks are avoided (e.g. sql injection, buffer overflow).

5.1. The Global Automaton Definition for the CoP Protocol

Starting from the description of the CoP protocol we now point out some basic properties that should be guaranteed in order to obtain a fair behavior of the protocol.

For each grid node there must be at most one sensor playing as clusterhead.

We formalize these properties by defining a state machine that will be given in input to our tool in order to produce the distributed “patch” for the sensors participating in the CoP protocol.

Figure 5 shows the Global Automaton related to the sensors based system of Fig. 4. This automaton defines the correct sequences of messages inside each A _VGN . At the beginning (state q0) all the sensors are informed about their positions. As described in Section 3, according to their position, each sensor sets its local variable role. The In-Range sensors candidate themselves to become leader. Once the ClusterHead has been elected, the system moves to state q1 and the real interaction can start. This transition, in practice, realizes property 1. Property 2 is realized by the path q1, q2, q3. In this example we fixed the “finite amount of data” by means of a maximum of three collected messages which the clusterhead necessarily forwarded. Property 3 is realized by means of transition q1, q5, in fact, if the system state is q1 there are no messages stored in the clusterhead. When data is forwarded, it is received by the Extern role, i.e., some clusterhead of another A _VGN on the way to the specified sink. ⁶ And this realizes property 4. Finally, property 5 is valid by means of transition q1, q5. From q5, in fact, a new ClusterHead must be elected before any other communication can occur. ⁷ Note that, when a ClusterHead receives a forward (transition q1, q6), it necessarily has to forward it (transition q5, q1).

OPEN IN VIEWER

Figure 5.

Global Automaton.

Concerning the predicates, check1(msg) is used to verify the correct format of the message msg forwarded by the ClusterHead. This predicate permits to check that msg is not a buffer overflow attack. The check2(msg) is similar to the above one, however it adds a test verifying that msg is equivalent to the compression of the two messages previously received by the ClusterHead. The predicate check(x, y) verifies that the leader is at a distance at most ds from its VGN.

We use the Global Automaton as the basis to build our specification-based intrusion detection system. We produce a set of filters (one for each specified role) that will be assigned to each sensor according to their actual role. Each filter locally monitors the sensor it resides on in order to validate the policy expressed by the Global Automaton. We provide different solutions in order to implement the filters:

a “heavy” solution in which each filter contains the whole global automaton;

These solutions allow a tradeoff among the security level and the overhead generated by the filter addition.

In Fig. 6 we describe the heavy solution for a filter that resides on a sensor s playing the role C.

OPEN IN VIEWER

Figure 6.

The heavy filter behavior: a sensor s playing the role C.

At step 1 the filter observes an invocation !m_C₁_C₂. At step 2 the filter takes into account the interface of the role C₁ and checks whether m can be derived from such an interface. When the derivation of m fails an attack reaction policy is undertaken.

At step 3 the filter verifies whether the current automaton state (e.g., q) contains a rule q′ = δ(q, !m_C₁_C₂) such that the predicate evaluated on !m_C₁_C₂ is true. In this case the filter applies one of the following steps 3a, 3b, 3c, or 3d.

Step 3a is applied when the invocation !m_C₁_C₂ is performed by s that is playing the role C, with C ≡ C₁. In this case the filter performs the invocation (i.e., it forwards the message m to the environment), changes the automaton state (that becomes q′) and executes the code related to the rule q′ = δ(q, !m_C₁_C₂). Step 3b is applied when the filter sniffs !m_C₁_C₂ from the environment. The filter changes the current automaton state to q′ and in the case that s is playing the role C, with C ≡ C₂, the message m is forwarded to s. Note that, a receive invocation from the filter point of view immediately follows the related send invocation. Step 3c is applied when the filter detects that s has performed a send invocation !m_C₁_C₂ and s is not playing the role C₁. In this case the message is discarded and a reaction policy is undertaken. Symmetrically, step 3d is applied when !m_C₁_C₂ is sniffed from the network and it was not performed by a filter s′ playing the role C₁. At step 4 the filter cannot accept the invocation in the current state, thus the invocation is discarded and an attack reaction policy is undertaken. Note that the interfaces are used in order to: (i)

verify the correct format of a message;

The reaction policy could require the sending of an alert message. This kind of message contains the information of the violation. The following reaction rules are applied: (i)

if the attack derives from a sensor invocation (i.e., it is locally detected by the related filter) then the filter locally discards the message and no alert is sent;

Concerning the mobility of the sensors we can have a sensor s that moves from an A _VGN to another one. Therefore, the filter of s has to discover the new correct local automaton state. In this case we provide two solutions. The first solution adds to all message m a short integer. This integer uniquely identifies a transition of the Global Automaton. By looking at this short integer the filter discovers which transition of A has been applied (i.e., it discovers the new state of its local automaton). In the second solution the filter sniffs the traffic and, by looking at the sequence of invocations, it finds the unique chain of rules that matches the sequence. The first solution requires to add overhead to the normal message, but it provides fast synchronization. The second solution does not add overhead, but it can require to sniff different invocations in order to guess the local automaton state.

Synchronization is also required when sensors can activate the sleep mode. In this modality sensors go idle to improve energy efficiency and wake up when required. The period of sleep mode is highly dependent on the considered protocol, therefore we cannot assume how long it will last. In our approach we require that when a sensor is turned on from the sleep mode there is a correct filter set up and the discovery of its new automaton state. In Fig. 7 we show a sensor s playing the role C and the basic operations needed when s turns on from the sleep mode. The first operation updates the variable roles to set up the new sensor role (e.g., C1) and the related filter (e.g, F_C1). The second operation is the discovery of the new local automaton state. This can be done by using the solutions proposed for managing mobility, i.e., (i)

read an integer added to the message in order to find out which transition of the global automaton has been applied:

In the following we describe how an IDS (i.e., the filter) based on the Global Automaton can be used in order to detect the attacks summarized in Section 1.

OPEN IN VIEWER

Figure 7.

Sleep mode and sensor wake up.

Concerning the Compromised Node attack, each filter controls all messages exchanged by the sensor where it resides on. Therefore, any sensor anomalous behavior is locally detected.

The False Node attacks is prevented since all filters residing in a given area sniff and validate all traffic. Even though new sensors (without filter) are added they must validate the property expressed by the Global Automaton since they are controlled by the “good” ones. In particular, it is sufficient to have a good sensor, in a given area, in order to detect the compromised ones.

The Node Outage attack is prevented since when a sensor has to transmit something and it does not (as can happen for a ClusterHead that is not forwarding collected data), the filter of the other sensors sends an alert.

Concerning the Message Corruption attack, step 2 verifies the integrity of a message with respect to the defined component interface. In other words, given an invocation !serviceName1 (T₁D₁X₁, …, T _n D _n X _n )_C₁_C₂, the role C₁ must define the service serviceName1 (T₁D₁X₁, …, T _n D _n X _n ). returnType1. Moreover, step 3c controls that the role C₂ allows the reception of the message by defining the service ?serviceName1 (T₁D₁X₁, …, T _n D _n X _n ). returnType1.

Denial of Service is prevented by specifying a suitable property. Assume that from a state q to a state q′ a finite number of messages must be received. Any sensor that performs an unbounded number of invocations is detected.

In this section we describe the light solution in which filters do not contain the whole Global Automaton. We use an algorithm to decompose the Global Automaton in a set of local automata that are assigned one for each role. The local automaton (denoted as A _C ) of the role C constitutes the basis in realizing a filter (denoted by C). The filter C has the same behavior of the one described in Section 6, but it contains a smaller automaton. This solution preserves the correctness with respect to the heavy one and brings the advantage of predicate workload distribution. As we describe in Section 6 another method for saving energy is setting the nodes to go idle (into sleep mode) if they are not needed and to wake up when required. In this case the synchronization problem (see Section 6) still arises once a sensor turns on its transceiver. In Subsection 7.3 we show how to address this problem.

In the following we describe the two main phases of the algorithm, i.e., local automata generation and dependencies generation.

7.1. Local Automata Generation

In this phase the transitions of the Global Automaton are projected on local automata according to the described roles. The phase considers the Global Automaton A = (Q, q₀, I, δ, P) and a role C. The output is a preliminary version A _C = (Q _C , q_C0, I _C , δ _C , P _C ) of the local automaton related to the role C. A _C is obtained by considering each rule q₁ = δ(q, !m_C₁_C₂), with C₁ ? C, defined in A (i.e., the send invocation performed by a filter playing the role C). This rule is reflected in the A _C -rule q₁ = δ_C(q, !m_C₁_C₂), the states q and q₁ are added to Q _C , !m_C₁_C₂ is added to I _C and the predicate P(q, q₁)(!m_C₁_C₂) is added to P _C . Moreover, rules of the form q₁ = δ _C (q, !m_*_C₂), with C₂ ? C are added to A _C , i.e., when the sender of a message is not modeled, the receiver must check the invocation. For both the above projections we say that the invocations are ‘associated’ to the role C. In other words, looking at the Global Automaton A, interactions that happen locally on a sensor playing the role C are projected on A _C .

Figures 8, 9, and 10 show the local automata generation projection performed on the In-Range, Out-Range, and ClusterHead roles, respectively. ⁸ For instance, part of the Global Automaton related to the invocations: !pos(double x, double y)_ * _Out – range [posx = x:posy = y], and !send(double x, double y, int dest, char [] msg) _Out _ Range_ClusterHead{chek(msg)} constitute the local automaton of the role Out-Range, since such invocations are locally performed by a sensor playing that role.

OPEN IN VIEWER

Figure 8.

Projection of the Global Automaton to the Out-Range role.

OPEN IN VIEWER

Figure 9.

Projection of the Global Automaton to the In-Range role.

OPEN IN VIEWER

Figure 10.

Projection of the Global Automaton to the ClusterHead role.

The preliminary version of a local automaton is not sufficient to realize the correct monitoring. A local automaton A _C can be constituted by disconnected sub-automata (see Fig. 8). The filter _C cannot be able to choose the right sub-automaton. Moreover, given a sub-automaton it cannot establish the next one.

Our solution is to enrich the local automaton with context information and to link the sub-automata with ε-moves. We call the context information dependency information.

Definition 8 Dependency information is of the form ? f (m, C′) where C′ range on the name of the sensor roles. ? f (m, C′) means that the message m is sent by a filter playing the role C′.

Given a local automaton A _C = (Q _C , q_0C, I _C , δ _C , P _C ) dependencies are added to the set I _C and their correct ordering is defined by means of the function δ _C . They establish the minimal information that _C must sniff in order to locally validate the property expressed by the Global Automaton. Dependencies are added by the dependencies generation phase.

7.2. Dependencies Generation

Dependencies affect synchronization and enabling states of the Global Automaton A = (Q, q₀, I, δ, P).

A synchronization state q of A is a state exited by at least two transitions labeled with invocations associated to different roles. We consider the case in which from q exactly two transitions exit: q₁ = δ(q, !m₁_C₁_C₂) and q₂ = δ(q, !m₂_C₃_C₄) with C₁ ≠ C₃, and q ¹q₁ ¹q₂.

The local automata generation ensures that these transitions are projected onto the related local automata (i.e., q₁ = δ _{C 1} (q, !m₁_C₁_C₂) and q₂ = δ _{C 3} (q, !m₂_C₃_C₄) are added to A _{C 1} and A _{C 3} , respectively). The dependencies generation phase considers the synchronization state q and adds the rules q₂ = δ _{C 1} (q, ?f(m₂, C₃)) and q₁ = δ _{C 3} (q, ?f(m₁, C₁)) to A _{C 1} and A _{C 3} , respectively.

From the point of view of A, if it is in the state q then either the transition q₁ = δ(q, !m₁_C₁_C₂) or q₂ = δ(q, !m₂_C₃_C₄) can be applied. From the filters point of view such possibility is lost since these rules are independently applied by the two different filters residing on the two different sensors. The rules q₂ = δ _{C 1} (q, ?f(m₂,C₃)) and q₁ = δ _{C 3} (q, ?f(m₁, C₁)) are a means used by the filters to overcome this problem. Suppose that both the local automata of filters ℑ _{C 1} and ℑ _{C 3} are in the state q, if a sensor playing the role C₁ is scheduled before other ones then

(i)

the filter ℑ _{C 1} changes the local automaton by applying the rule q₁ = δ(q, !m₁_C₁_C₂);

(ii)

filters ℑ _{C 3} sniff the invocation !m₁_C₁_C₂ and move by applying the rule q₁ = δ _{C 3} (q, ?f(m₁, C₁)).

Symmetrically, if a sensor playing the role C₃ is scheduled before other sensors then (i)

the filter ℑ _{C 3} change the local automaton by applying the rule q₂ = δ(q, !m₂_C₃_C₄);

(ii)

filters ℑ _{C 1} sniff the invocation !m₂_C₃_C₄ and move by applying the rule q₂ = δ _{C 1} (q, ?f(m₂, C₃)).

The following definition generalizes the above considerations.

Definition 9 Let A = (Q, q₀, I, δ, P) be a Global Automaton and let q be a state of A, we denote by ^q a set of filters. _C belongs to ^q if there exists p ∊ I _C such that the rule q′ = δ(q, p) is defined in A.

We can observe that each local automaton A _C of the filter ℑC, with ℑC ∊ ^q , must contain a projection of a q-exiting transition.

If ℑ ^q = {ℑ _{C 1} , ℑ _{C 2} , …, ℑ _{C n} } and a filter ℑ _{C i} , with ℑ _{C i} ∊ ℑ ^q , and 1  i  n will apply the rule q′ = δ _{C i} (q, !m₁_C _i _C′), then all filters ℑ _{C j} , with ℑ _{C j} ∊ ℑ ^q and j ≠ i, move by applying the rule q′ = δ _{C j} (q, ?f(m₁, C _i )). This means that all the local automaton of the filters in ^‵ are synchronized to the state q. We call such dependencies synchronization dependencies since they are used to synchronize the filters in order to accept one invocation exactly.

A state of A is an enabling state if it is entered and exited by transitions projected on two different local automata. For instance, consider the state q in which A defines the chain of rules q = δ(q⁻, !m₁_C₁_C₂) and q⁺ = δ(q, !m₂_C₃_C₄), with C₁ ≠ C₃, and q ≠ q⁻. The local automata generation ensures that the rules q = δ(q⁻, !m₁_C₁_C₂) and q⁺ = δ(q, !m₂_C₃_C₄) are projected on the automata of the filters ℑ _{C 1} and ℑ _{C 3} , respectively. From the A point of view, this chain of rules defines a constraint among the invocations !m₁_C₁_C₂ and !m₂_C₃_C₄. That is, !m₁_C₁_C₂ must be accepted before !m₂_C₃_C₄. However, from the local filters point of view, this constraint is lost, since the chain of rules is divided not the filters ℑ _{C 1} and ℑ _{C 3} . Therefore, the filter ℑ _{C 3} can autonomously perform the invocation !m₂_C₃_C₄ before that the invocation !m₁_C₁_C₂ is performed by ℑ _{C 1} . The problem is solved by adding dependencies.

The dependencies generation adds to A _{C 3} the rule q = δ _{C 3} (q⁻, ?f(m₁, C₁)). Therefore, ℑ _{C 3} can move to the state q by means of the rule q = δ _{C 3} (q⁻, ?f (m₁, C₁)). However, this rule can be applied only when the filter ℑ_C1 performs the invocation !m₁_C₁_C₂, i.e., the filter ℑ _{C 3} sniffs the message m₁ sent by ℑ_C1. This is a mean for filter ℑ _{C 1} to impose the right ordering among the messages !m₁_C₁_C₂ and !m₂_C₃_C₄. We call such dependencies enabling dependencies, since they are used to enable the local-filter parsing when there is the right context condition.

Note that, after the addition of these dependencies, a local automaton A _C can still be disconnected, i.e., constituted by the disconnected automata A¹, A², …, A ^nC . The last step of the dependencies generation phase links together these local disconnected automata by means of ε moves. Given the state q and q _n of A _C , this step can add to A _C rules of the type q _n = δ _C (q, ε). This epsilon move models that the state q and q _n of A _C are separated by a chain of rules labeled with invocation that are not associated to the role C. The filter _C can ignore these interactions moving from q to q _n where it will be informed by means of a dependency when this chain of rules has been performed.

By applying usual techniques, ε-moves can be removed [13] in any local automaton A _C = (Q _C , q_0C, I _C , δ _C ). Indeed, let Q ̄ = q ∪ { q 1 , q 2 , … , q n } be the state obtained by removing ε-moves from q as explained in [13], where {q₁, q₂, …, q _n } are all the states reachable from the given state q ∊ Q _C by means of ε-moves. The set of transitions exiting from Q ̄ can only be labeled with dependency. ⁹ However, the process of removing ε-moves can create a state Q ̄ where two different states q i , q j ∈ Q ̄ can be exited by transition labeled with the same dependencies ? f (m, C): q′ = δ _C (q _i , ? f (m, C′)) and q? = δ _C (q _j , ? f (m, C′)). This non-determinism can be solved either by translating the local automaton ^C to the deterministic one or by letting the filter ^′CꞋ adding an integer k to the message m. The integer k uniquely identifies a transition of the Global Automaton. Therefore, although a filter can contain ε-moves only one of them can be deterministically applied.

The filter behavior _C is similar to the one proposed by the heavy solution: (i)

it can only accept invocations associated to the role C (i.e., the ones projected to its local automaton A _C );

(ii)

it verifies the correct format and the predicates related to invocations performed by sensor playing the same role;

(iii)

it sniffs the network and moves when the message matches a dependency that labels an A _C transition.

Therefore, filters based on the light solution distribute the workload of predicates evaluation. There are less rules to apply. Moreover, when the Global Automaton is big in size and a sensor never changes its role we can reduce the memory allocation.

In Fig. 11 we show the local automaton of the Out-Range role. We can observe as the local automaton allows the send invocation only when the leader message has been sniffed from the environment. Note that only the transitions of the Out-range role require the predicates evaluation.

OPEN IN VIEWER

Figure 11.

Local automaton of the Out-Range role.

7.3. Mobility Aspects and Sleep Mode

The position of a sensor can change as a consequence of its mobility. This may also change the role of the sensor in the network. The associated filter then, should refer to a different automaton. It can happen that a state in the original automaton is not present in the new one. In order to solve this problem we propose two solutions. One is to define a mapping function that takes in input a state q _x of a role C′ and a role C?, and outputs a state q _w of the role C? that corresponds to q _x in C′. Such a function should be evaluated by the filters each time the corresponding sensor changes its behavior (role). The overhead is then given by the needed computations to evaluate such a function.

Another solution is to enrich the messages by making explicit the corresponding move on the local automaton, in such a way, that the receiver can understand which dependency on the local automaton is satisfied hence discovering its current state. The overhead in this case is given by the extra information we need inside each message.

The right choice among those solutions strongly depends on the given protocol. From the energy-consumption point of view the first solution seems more suitable. In the case where a sensor changes A _VGN , the same arguments of the heavy solution can be applied.

As already pointed out at the beginning of the section, synchronization problems can arise when the desired protocol makes use of the sleep modality for the sensors in order to save energy. In the light solution after the sensor turns on from the sleep mode its filter has to perform the same operations described in Section 6 (see Fig. 7). In particular, the discovery of the new local automaton state can be done by applying the following techniques:

(i)

discover the new state by observing the integer added to the message in order to find out the new local state ¹⁰ ;

(ii)

sniff the sequence of invocations to eventually find out a unique chain of rules that matches the sequence.

7.4. Attacks Detection

Concerning the attacks detection, filters behave like in the heavy solution but restricted to their own roles. The Node Outage attack, for instance, is prevented since when a sensor has to transmit something and it does not, the filters of the other sensors playing the same role send an alert. Conversely, special attention must be given to Compromised Node attacks since we have to ensure that the Global Automaton is now perfectly emulated by the local ones. The following theorem ensures that this attack is prevented.

Theorem 1. Given a protocol P for mobile WSNs, let A = (Q, q ₀ , I, δ, P) be a Global Automaton expressing the correct behaviors of p sensors {s₁, s₂, s₃ … s _p } according to a set R of defined roles with respect to a cluster A _{r i} with 1  i  m. Let ℑ _{C j} be the filter related to the sensor s _j . The automaton A accepts an architectural trace T = T _{s i} ⊕ … ⊕ T _{s ^p} if and only if all the sensor traces T _{s j} are accepted by each corresponding ℑ _{C j} with 1  j  p.

Proof. ⇐) Dependencies permit to prove that the merge of local traces is accepted by the Global Automaton ¹¹ . For this aim we summarize the state of all filters in a given area A _{r i} (i.e., the state of the whole IDS system) as the state of each local automaton (i.e., a p-tuple of states) and we show that the IDS state has to go through states where the following predicate is true.

Definition 10. Let A = (Q, q₀, _I , δ, P) be a Global Automaton and let q ∊ Q be a state of A. We say that the IDS is in a state where the predicate ψ(q) is true if the following conditions hold:

(i)

every local automaton A _C of a filter ^C in ^q is in the state q;

(ii)

every local automaton of a filter in ℑ ^q is in a state where all exiting transitions are labeled with incoming dependencies.

When ψ(q) is true all local automata of the filteres in ^q are in the state q, therefore exactly one filter _C ∊ ^q accepts its local invocation (e.g., !m_C_C₁) by means of the rule q′ = δ _C (q, !m_C_C₁). Once _C has applied the rule, all other filters in ^q move to q′ by applying the rule q / c = d C ( q , ? f ( m , C ) ) (i.e., the rule labeled with a synchronization dependency). A filter _C′ in ^q′\ ^q defines a transition exiting from q′ (e.g., q″ = δ_C′(q′, !m_C′_C′₁)). The state q′ is an enabling state of A since there is the q′ entering transition q / c = δ C ( q , ! m _ C _ C 1 ) and the q / c exiting transition q” = δ _C′ (q′, !m_C′_C′₁), with C ≢ C′, and q ≠ q′. Therefore, if we prove that all filters in ′ q ′ ∖ ′ q are in the state q they move to the state q′ by applying the rule labeled with the enabling dependency ?f(m, C), ¹² i.e., the IDS reaches a state where ψ(q′) holds. In this case we say that the IDS performs one step from a state were ψ(q) is true to a state were ψ(q′) is true.

Starting from the initial state (i.e., all local automata are in the state q₀) the IDS performs step 1, ?, i where the predicates ψ(q₀), ?, ψ(q _i ) are true and at each step j, with 1  j  i, the rule q_j+1 = δ _{C j} (q _j , !m _j _C _j _C′ _j ) is applied by ℑ _{C j} ∊ ℑ ^{q _j} . The sequence of rules q_j+1 = δ _{C j} (q _j , !m _j _C _j _C′ _j ) are projections of A rules, therefore, the Global Automaton A can accept the sequence !m₁_C₁_C′_{1 ?} !m _i _C _i _C′ _i by applying the same sequence of rules.

By induction on step i, we prove that if the filter ℑ _{C i} applies the rule q _i = δ _{C i-1} (q_i-1, !m_i-1_C_i-1_C′_i-1) then all filters in ℑ ^{q _i} are in state q_i-1. This is sufficient in order to prove that at step i + 1 the predicate ψ(q _i ) holds.

The predicate ψ(q₀) is true when the sensors start to work since all local automata are in state q₀. Moreover at step 1 if filter ℑ _{C 1} applies the rule q₁ = δ _{C 0} (q₀, !m₀_C₀_C′₀) all filters in ℑ q 1 ∖ ℑ q 0 are in state q₀.

At step i the filter ℑ _{C i} applies the rule q_i=1 = δ _{C i} (q _i , !m _i _C _i _C′ _i ′). By contradiction, we assume there exists a filter ^ꞌC^′ in ℑ q i + 1 ∖ ℑ q i that is not in the state q _i .

The filter _Cʼ contains a q_i+1 exiting transition q_i+2 = δ_C′ (q_i+1, !m_i+1_C′_C′_i+1), _{C i} the rule q i + 1 = d C i ( q i , ? f ( m i , C i ) ) . Therefore, q_i+1 is an enabling state of A and _C′ contains the rule q i + 1 = d C c / ( q i , ? f ( m i , C i ) ) .

_C′ , at step i − 1, cannot belong to the set ℑ ^q_i-1 otherwise by induction it would be in the state q _i at step i. Let the step j be the last state where ‵ _C′ is in state q _j , i.e., for all steps k, with k > j, ^ꞌCꞋ does not belong to the set ‵q ^k . Thus, the chain of rules q k + 1 = δ C c / ( q k , ? f ( m k , − C k ) ) is not labeled with invocations associated to C^‵. With this last assumption the rule q i − 1 = d C c / ( q k , ε ) (q _k , ε) is defined in A _C′ . Since all rules exiting from q _i − 1 are labeled with dependency related to q _i - 1 then ^‵C between step k and i − 1 cannot move, i.e., at step i − 1 it is in q_i- 1, and this contradicts the hypothesis.

⇒)

Let T = T _{s 1} ⊕ … ⊕ T _{s p} be a trace accepted by A. We can always find a schedule such that each sensor s _i produces the trace T _{s i} .

8. Performance Evaluation

In this section we show how our method affects the performance of the CoP protocol in terms of energy-consumption and computed operations. The experiments are performed running the powered protocol over hundreds of random instances of mobile WSNs. We applied both the heavy and the light solutions. We show the overhead in terms of consumed energy and in terms of performed instructions by the filtered sensors. The experiments also show the estimated percentage reduction of the network lifetime with respect to the original CoP protocol.

In Fig. 12 we show the lifetime of the system inside an A _VGN . Considering each kind of message of the sensors as a different set of instructions, we show the overhead in terms of percentage of computational power loss. The cost of ensuring the normal behavior of the protocol in terms of number of instructions by means of the light solution is increased, on average, around 24%. The heavy solution costs, on average, around 39%. Note that transmission/reception operations are much more expensive than local computations. According to the consumption values expressed in [12, 23], transmitter and receiver electronics consume an equal amount of energy per bit, namely 5nJ/bit. While the energy to support the signal above some acceptable threshold against power attenuation caused by the distance is just 100pJ/bit/m².

OPEN IN VIEWER

Figure 12.

Average of the residual computational power depending on messages exchanged inside an A _VGN .

In Fig. 13 we show, on average, the percentage of the draining of the sensors batteries inside an A _VGN . For the heavy solution it is increased by around 37% while for the light solution we obtained around 19%. Note that such comparisons are performed without simulating attacks. This means that the original CoP protocol was able to perform the desired (random) communications. In the case of attacks, the original protocol can waste indeed much more energy with respect to the “safe” solutions. Consider for instance a sensor that generates traffic without following the right syntax of the messages or the right scheduling. While in the original CoP protocol those messages are forwarded till the sink, now they are just blocked by the local filters.

OPEN IN VIEWER

Figure 13.

Average of the residual energy depending on messages exchanged inside an A _VGN .