Distributed Information Flow Verification Framework for the Composition of Service Chain in Wireless Sensor Network

Abstract

Dynamic service composition provides us with a promising approach to cooperate different sensor nodes in WSN to build complex applications based on their basic functions. Usually multiple nodes located in different regions provide data with different security levels, and it is critical to ensure the security of the information flow in the composite services. However, the energy-limited nature of sensor nodes in WSN poses a significant challenge for the centralized information flow verification with which the verification node needs to consume lots of computation and network resources. In this paper, we specify the security constraints for each service participant to secure the information flow in a service chain based in the lattice model and then present a distributed verification framework that cooperates different service participants to verify their information flow policies distributively. The evaluation results show a significant decrease on the verification cost of the single verification node, which provides a better load balance in each sensor node.

1. Introduction

WSN is the key enablers for the development of the Internet of Things (IoT), which is responsible for collecting surrounding context and environment information. In a service-oriented WSN [1, 2], multiple sensor nodes with different basic services, for example, data aggregation, data processing, and decoding, can cooperate with each other to develop new applications rapidly. However, because of the variety and regional characteristics of WSN, the data provided by the sensor nodes have different security levels. When services are composed together, data are transmitted among these nodes, respectively, where an operation in a node assigning high-level data to a low-level object would cause the information leakage with a serious impact on the public safety or personal privacy.

For example, a personal-health helper service can be provided for the healthy advice according to the body status and environments data. Most of the former work, mainly focus on the access control of the individual services [3, 4]. But in a service chain, data may be computed from its prior services which can result in the undesired information leakage. When the collection service is completed, the data collected by the wearable sensors and environmental sensors are delivered to the data processing node, such as mobile phone. Healthy information may leak to untrusted third party through the illegal operations during data processing. So the information flow security is one of the major concerns about the service composition in sensor network environments.

One issue in information flow security of the composite service is the dynamic dependence among various objects in different service participants. Accorsi and Wonnemann [5] use Petri nets to represent the workflow and detect information leaks in workflow descriptions based on static information flow analysis. But this work can only validate the information flow in fixed workflow with static input and output dependences. In service-oriented WSN, there are several candidate services with same functions where the dependences between input and output are different from each other. It is necessary for user to select appropriate service for the secure composition of the service chain. She et al. [6, 7] define transformation factors to measure how likely the output depends on the input data in different candidate services. But it is hard to define the LR, MR, and HR transformation factors. Therefore, a suitable dependence model is required for the analysis of the information flow in different candidate services.

Another major issue for the information flow verification in WSN is the energy cost of the verification node. Zorgati and Abdellatif [8] and She et al. [9] propose the centralized verification approach against the information flow control policies to ensure an end-to-end security in wired network. However, in WSN, the sensor node is energy limited, and the centralized way consumes lots of energy of the verification node. Yildiz and Godart [10] propose an decentralized service composition approach considering the information flow policies in an inexpensive manner, but its policies are static. Based on the information flow type system, Hutter and Volkamer [11] specify the composition rules to control the security of dynamically computed data and their proliferation to other web services. But it costs extra energy of the sensor node to compile the service code again before the service execution.

In this paper, we present a distributed information flow verification approach applied on the composition of the service chain in wireless sensor network. Our contributions include the following. (1) For the dynamic dependences in service chain, we define the intra and inter dependences among different objects in composite service based on the PDG. (2) We specify the security constraints for each service participant based on the dependences and lattice model. (3) We propose a decentralized information flow verification approach to execute the verification process distributively to provide a better load balance of the sensor nodes in WSN.

The rest of the paper is structured as follows. Section 2 presents the basic definitions of the wireless sensor service system. Section 3 specifies the security constraints for each service participants based on the analysis of the information flow in the service chain. In Section 4, we propose the distributed information flow verification framework based on the secure information flow model. Section 5 evaluates the proposed verification approach. Section 6 concludes the paper.

2. Wireless Sensor Service System

A wireless sensor service system (WSS) is a large-scale distributed environment which consists of multiple wireless sensor nodes, public data resources and security authorities, which is shown in Figure 1. Sensor nodes in WSN can collect these resources, and provide different basic functions, such as data analyzing or processing, which are treated as various services in WSN. There is also a security authority for each data resources for the management of these data security levels which are used for the security verification. The service on each sensor node can be defined as follows.

Figure 1

A wireless sensor service system.

Definition 1.

Each service $s_i$ is a tuple $s_i=〈{id}_i,\hspace{0.17em}{In}_i,\hspace{0.17em}{Out}_i,\hspace{0.17em}{F}_i,\hspace{0.17em}C{e}_i〉$ , where $i{d}_i$ is the identifier of the service; ${In}_i$ is the set of input of service; ${Out}_i$ is the set of the output of service; $F_i$ is composed of a sequence of actions $〈a_1,a_2,\dots 〉$ ; $C{e}_i$ is the certificate of the service which specifies the security properties of service.

In WSS system, various services are provided by different sensor nodes. These individual services can also be combined together to generate a more powerful service. During the execution of composite service, each service node collects data from its local storage or the public resources, processes the input data, and finally provides results to the sink nodes. On the other hand, these nodes may also update the local storage or store to the public data resources in WSS. A composite service can be denoted as a directed graph, where the vertex is the service component and the edge represents an composition relationship from one service to another. In this paper, we investigate a simplified composite service, the service chain, which is defined as follows.

Definition 2.

A service chain $s_c$ can be represented as a tuple $s_c=〈CH,In,Out〉$ where $CH$ is a sequence of services $〈s_1,s_2,\dots 〉$ ; $In$ is the set of input of $s_c$ , $s_c$ ; $Out$ is set of output of $s_c$ .

In a service chain $s_c$ , the predecessor of a service $s_i$ can be denoted as $s_{i-1}$ , and the successor of a service $s_i$ is denoted as $s_{i+1}$ . $s_0$ denotes the node who sends the initial request to $s_1$ , and $s_{n+1}$ denotes the sink node who receives the service result from $s_n$ . Figure 2 shows a simple service chain model.

Figure 2

A service chain model.

Due to the dynamic and heterogeneous sensor network environment, it is necessary to select appropriate service to satisfy the different requirements including QoS and security. In this paper, we focus on the verification of the information flow security in composite service chain and providing support for the security enforced selection of services in WSN.

3. Secure Information Flow Model

3.1. Security Label Model

For the information with different sensitivities, we use multilevel security labels to describe the security properties of objects o.

Definition 3.

Security label model is defined as a lattice $(SL,\le )$ , where $SL$ is a finite set of security levels that is totally ordered by ≤.

The lattice model is widely used in government or military systems in which the security classes are determined solely from the four security levels: unclassified, confidential, secret, and top secret [12].

For a clear discussion, in this paper, we define that each object o has a provided and required security level, $\text{Pr}(o)$ and $\mathrm{Re}(o)$ , which specifies the read and write permissions possessed by o. The provided security labels of the objects can be given by the data owners, which are specified in certificates. And the required security labels of data objects will be computed according to the dependence of the input and output data.

3.2. Information Flow in Service Component

In a service chain, the information flow through $s_i$ is shown in Figure 3. We consider a data flow model in which each service may read from a set of input data objects and write to a set of output data objects. The set of input objects of a service $s_i$ includes all the objects that $s_i$ receives from its predecessor $s_{i-1}$ and all data objects obtained from the public data resources or stored in the local storage in sensor nodes. The set of output objects of $s_i$ includes all the objects that $s_i$ sends to its successor $s_{i+1}$ and all the data objects that $s_i$ updates to the public data resources and the local storage.

Figure 3

Information flow in service component.

For the input information for $s_i$ , there is ${In}_i=\{{In}_i^M,{In}_i^D,{In}_i^L\}$ , where

• (i)

${In}_i^M=\{{In}_{i,1}^M,{In}_{i,2}^M,\dots ,{In}_{i,n}^M\}$ is the set of all input objects that $s_i$ receives from its predecessor $s_{\text{i}-1}$ ;

(ii)

${In}_i^D=\{{In}_{i,1}^D,{In}_{i,2}^D,\dots ,{In}_{i,n}^D\}$ is the set of all input objects from the public data resources;

(iii)

${In}_i^L=\{{In}_{i,1}^L,{In}_{i,2}^L,\dots ,{In}_{i,n}^L\}$ is the set of all input objects located in local storage in sensor nodes.

For the output information for $s_i$ , there is ${Out}_i=\{{Out}_i^M,{Out}_i^D,{Out}_i^L\}$ , where

• (i)

${Out}_i^M=\{{Out}_{i,1}^M,{Out}_{i,2}^M,\dots ,{Out}_{i,n}^M\}$ is the set of all output objects that $s_i$ sends to its successor $s_{i+1}$ ;

(ii)

${Out}_i^D=\{{Out}_{i,1}^D,{Out}_{i,2}^D,\dots ,{Out}_{i,n}^D\}$ is the set of all output objects that $s_i$ updates to the public data resources;

(iii)

${Out}_i^L=\{{Out}_{i,1}^L,{Out}_{i,2}^L,\dots ,{Out}_{i,n}^L\}$ is the set of all output objects that $s_i$ writes to the local storage in sensor nodes.

In order to validate the information flow in $s_i$ , we need to analyze the relationships between the input and output objects. The output ${Out}_i$ is computed from $I{n}_i$ during the execution of the service function $F_i$ . The syntax of $F_i$ is defined as follows:

$$\begin{array}{l}f::=a;f,\\ a::=\text{skip}\mid \text{input}\left(in,e\right)\mid \text{var}≔e\mid a;a\\ \hspace{1em}\hspace{0.5em}\mid \text{if}\left(e\right)\hspace{0.17em}\hspace{0.17em}\text{then}\hspace{0.17em}\hspace{0.17em}a\hspace{0.17em}\hspace{0.17em}\text{else}\mathrm{\hspace{0.17em}\hspace{0.17em}}a\\ \hspace{1em}\hspace{0.5em}\mid \text{while}\left(e\right)\mathrm{\hspace{0.17em}\hspace{0.17em}}a\mid \text{output}\left(out,e\right),\\ \hspace{0.17em}e::=\text{var}\mid e\mathrm{Re}\\ R::=+\mid -\mid \hspace{0.17em}=\hspace{0.17em}\mid <.\end{array}$$

(1)

A service function consists of a collection of activities, some of which are the control and computation operations, while some of which are responsible for receiving the inputs from different sources $in$ and producing outputs data to the required objects $out$ . We can establish the program dependence graph (PDG) [13] of $F_i$ according to its syntax to analyze the relationships among different objects used in $F_i$ . The PDG is defined as follows.

Definition 4.

Program dependence graphs (PDG) is a directed graph $〈V,\overrightarrow{E}〉$ , where the expressions and the activities in $F_i$ constitute the nodes of the graph and the edges express data and control dependences. A data dependence represented by an edge $a{\to }_d$ $a^{\prime }$ means that the activity a assigns variable x which is used in activity $a^{\prime }$ . A control dependence represented by an edge $e{\to }_c$ a means that the execution of a depends on the value of the expression e, which is typically a branch and loop condition.

Once a program dependence graph $\text{PDG}=〈V,\overrightarrow{E}〉$ has been constructed, program backward slice [14] is used to analyze the dependences among the different objects that are used in activities and expressions in $\text{PDG}$ . Here we use $\text{Dep}(o)$ to represent the obtained dependency set of an object o.

Based on the dependency set $\text{Dep}(o)$ , we can compute output object required security level according to the following equations: for $\forall u\in {Out}_i$ ,

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)=\bigsqcup _{\max }\mathrm{Re}\left(v\right),\hspace{1em}v\in {In}_i\wedge v\in \text{Dep}\left(u\right).\end{array}$$

(2)

Based on the previous equation, we can obtain the following.

Theorem 5.

For $\forall u\in {Out}_i^M$ , there is

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(v\right),\hspace{1em}\forall v\in {In}_i\wedge v\in \text{Dep}\left(u\right).\end{array}$$

(3)

Each service $s_i$ has different levels of inputs and outputs. The value of the input objects with high-level security label may flow to the low-level output objects during the execution of the service and cause the information leak. Therefore, the definition of the secure information flow in service component is given as follows.

Definition 6.

The information flow in service component $s_i$ is considered secure if it satisfies that for $\forall u\in {Out}_{i,j}^D\cup {Out}_{i,j}^L$ , there are

$$\begin{array}{cc}& \text{Pr}\left(u\right)\ge \mathrm{Re}\left(u\right)=\bigsqcup _{\max }\mathrm{Re}\left(v\right),\hspace{1em}v\in {In}_i\wedge v\in \text{Dep}\left(u\right).\end{array}$$

(4)

The previous condition provides that there are no lower level objects in public resources and local storage storing the data with higher security level during the execution of each service.

3.3. Secure Information Flow in Service Chain

Consider the service chain $〈s_1,s_2,\dots ,s_n〉$ . The output data sent from $s_i$ to $s_{i+1}$ , ${Out}_i^M$ , may be dynamically computed from some data stored by sensor node and public data resources, ${In}_i^L$ and ${In}_i^D$ , and some data received from $s_{i-1}$ , ${Out}_{i-1}^M$ . ${Out}_i^M$ may be further processed by $s_{i+1},\dots ,s_{j-1}$ and computed into ${Out}_{j-1}^M$ which is delivered to service $s_j$ , $j>i$ . And the dependence between objects belonging to different service components is considered as the interservice dependence. The interservice dependence set of object u, $\text{De}{\text{p}}_{\text{inter}}(u)$ , is defined as follows.

Definition 7.

For objects $v\in s_i$ and $u\in s_j$ where $j>i$ , v is in $\text{De}{\text{p}}_{\text{inter}}(u)$ which satisfies one of the following two conditions:

• (1)

   $i=j-1:$

 

$\exists w_1\in Ou{t}_i^M,\hspace{0.17em}{w}_2\in I{n}_j^M,\hspace{0.17em}{w}_1=w_2$

 

$(v\in \text{Dep}(w_1)\vee w_1=v)\wedge (w_2\in \text{Dep}(u)\vee w_2=u)$ ,

(2)

$i\ne j-1:$

 

$\exists w\in s_k,i<k<j$

 

$v\in \text{De}{\text{p}}_{\text{inter}}(w)\wedge w\in \text{De}{\text{p}}_{\text{inter}}(u)$ .

For two adjacent services $s_i$ and $s_j$ where $i=j-1$ , there are four cases that need to be considered. (1) For $v\in {Out}_i^M$ = $u\in {In}_j^M$ , there is an interservice dependence between u and v. (2) For $v\in {Out}_i^M$ and $u\notin {In}_j^M$ , there is an interservice dependence between them if there are objects $w\in {In}_j^M$ and $v=w$ that u depends on. (3) For $v\notin {Out}_i^M$ and $u\in {In}_j^M$ , u externally depends on v if there are objects $w\in {Out}_i^M$ and $u=w$ that depends on v. (4) For $v\notin {Out}_i^M$ = $u\notin {In}_j^M$ , if there are two objects $w_1\in {Out}_i^M$ , $w_2\in {In}_j^M$ that $w_1=w_2$ , while data object u in $s_j$ depends on $w_2$ , and $w_1$ depends on v in $s_i$ , we call uthat externally depends on v.

For two services $s_i$ and $s_j$ where $j>i+1$ , if there is an object w in $s_k$ , $i<k<j$ which w externally depends on v, while u externally depends on w, the dependence between u and v is the interservice dependence.

For a service chain $s_c$ where $I{n}_{sc}={\bigcup }_{}‍\{{In}_i^L\cup {In}_i^D\}$ and $Ou{t}_{sc}={\bigcup }_{}‍\{{Out}_i^L\cup {Out}_i^D\}$ , $0\le i\le n+1$ , we use $s_0$ that denotes the start node which sends the initial request to $s_1$ , and $s_{n+1}$ denotes the sink node which receives the service results from $s_n$ . And we assume that ${In}_0^M=\varphi$ , ${Out}_0^D\cup {Out}_0^L=\varphi$ , ${In}_{n+1}^L\cup {In}_{n+1}^D=\varphi$ , and ${Out}_{n+1}^M=\varphi$ .

Definition 8.

The information flow in service chain $s_c$ is considered secure if and only if it satisfies that for $\forall u\in {Out}_c$ , there are

$$\begin{array}{cc}& \text{Pr}\left(u\right)\ge \bigsqcup _{\max }\mathrm{Re}\left(v\right)\\ v\in {In}_c\wedge \left(v\in \text{Dep}\left(u\right)\vee v\in \text{De}{\text{p}}_{\text{inter}}\left(u\right)\right)\\ 1\le j<i.\end{array}$$

(5)

According to the definition of the secure information flow in $s_i$ and $s_c$ , we can obtain the following lemmas and theorems.

Lemma 9.

In a service chain $s_c〈s_1,s_2,\dots ,s_m〉$ , $\forall u\in {Out}_i^M$ , $0\le i\le m$ satisfies

$$\begin{array}{cc}& \text{Re}\left(u\right)\ge \text{Re}\left(v\right)\\ v\in {In}_j\wedge \left(v\in \text{Dep}\left(u\right)\vee {\text{Dep}}_{\text{inter}}\text{}\left(u\right)\right),\\ 0\le j\le i.\end{array}$$

(6)

Proof.

First, let $m=1$ , then there are two service components $s_0$ and $s_1$ .

For $\forall u\in {Out}_0^M$ , Theorem 5 provides that $\forall v\in {In}_0\wedge v\in \text{Dep}(u)$ , and there is $\mathrm{Re}(u)\ge \mathrm{Re}(v)$ .

And there is no interservice dependence in $s_0$ , so the lemma is proved.

For $\forall u\in {Out}_1^M$ , there are two cases to consider.

Case 1. $j=1,\forall v\in {In}_1\wedge v\in \text{Dep}(u)$ . Theorem 5 provides $\mathrm{Re}(u)\ge \mathrm{Re}(v)$ .

Case 2. $j=0,\forall v\in I{n}_0\wedge v\in \text{De}{\text{p}}_{\text{inter}}(u)$ . In this case, the definition of the interservice dependence provides $\exists w_1\mathrm{\hspace{0.17em}\hspace{0.17em}}\text{and}\mathrm{\hspace{0.17em}\hspace{0.17em}}{w}_2$ where

$$\begin{array}{cc}& w_1\in {Out}_0^M=w_2\in {In}_1^M,\\ v\in \text{Dep}\left(w_1\right)\wedge w_2\in \text{Dep}\left(u\right).\end{array}$$

(7)

Theorem 5 provides that

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(w_2\right),\end{array}$$

(8)

$$\begin{array}{cc}& \mathrm{Re}\left(w_1\right)\ge \mathrm{Re}\left(v\right).\end{array}$$

(9)

And there is

$$\begin{array}{cc}& \mathrm{Re}\left(w_2\right)=\mathrm{Re}\left(w_1\right).\end{array}$$

(10)

Based on (8), (9), and (10), we can get

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(v\right).\end{array}$$

(11)

In a conclusion, when $m=1$ , the lemma is proved.

Then we suppose that the lemma is true when $m=n-1$ ; that is, for $\forall u\in {Out}_i^M$ , $0\le i\le n-1$ , there are

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(v\right),\\ v\in {In}_j\wedge \left(v\in \text{Dep}\left(u\right)\vee v\in \text{De}{\text{p}}_{\text{inter}}\left(u\right)\right),\\ 0\le j\le i.\end{array}$$

(12)

And the case that $m=n$ is proved as follows: for $\forall u\in Ou{t}_n^M$ , there are also two cases to consider.

Case 1. $j=i,\forall v\in I{n}_n\wedge v\in \text{Dep}(u)$ . In this case, Theorem 5 provides $\mathrm{Re}(u)\ge \mathrm{Re}(v)$ .

Case 2. $0\le j<i,\forall v\in {In}_j\wedge v\in \text{De}{\text{p}}_{\text{inter}}(u)$ . In this case, the definition of the interservice dependence provides $\exists w_1,w_2$ where

$$\begin{array}{cc}& w_1\in {Out}_{n-1}^M=w_2\in {In}_n^M,\\ \left(v\in \text{Dep}\left(w_1\right)\vee v\in \text{De}{\text{p}}_{\text{inter}}\left(w_1\right)\right)\wedge w_2\in \text{Dep}\left(u\right).\end{array}$$

(13)

Theorem 5 provides that

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(w_2\right).\end{array}$$

(14)

The previous assumption provides that for $0\le i\le n-1$ , there is

$$\begin{array}{cc}& \mathrm{Re}\left(w_1\right)\ge \mathrm{Re}\left(v\right),\end{array}$$

(15)

and there is

$$\begin{array}{cc}& \mathrm{Re}\left(w_2\right)=\mathrm{Re}\left(w_1\right)\end{array}$$

(16)

Based on (14), (15), and (16), we can get

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(v\right).\end{array}$$

(17)

In a conclusion, when $m=n$ , the lemma is proved.

Lemma 10.

If the information flow of each service in first m step of $s_c$ is secure, $\forall u\in {Out}_i^D\cup {Out}_i^L$ , $0\le i\le m$ satisfies

$$\begin{array}{cc}& \text{Pr}\left(u\right)\ge \mathrm{Re}\left(v\right),\\ v\in {In}_j\wedge \left(v\in \text{Dep}\left(u\right)\vee {\text{Dep}}_{\text{inter}}\text{}\left(u\right)\right),\\ 0\le j\le i\end{array}$$

(18)

Proof.

For $\forall u\in {Out}_i^D\cup {Out}_i^L$ , there are also two cases to consider.

Case 1. $j=i,\forall v\in {In}_i\wedge v\in \text{Dep}(u)$ . In this case, the secure information flow Definition 6 provides $\text{Pr}(u)\ge \mathrm{Re}(v)$ .

Case 2. $0\le j<i,\forall v\in {In}_j\wedge v\in \text{De}{\text{p}}_{\text{inter}}(u)$ . In this case, the definition of the interservice dependence provides $\exists w_1,w_2$ where

$$\begin{array}{cc}& w_1\in {Out}_{n-1}^M=w_2\in {In}_n^M,\\ \left(v\in \text{Dep}\left(w_1\right)\vee v\in \text{De}{\text{p}}_{\text{inter}}\left(w_1\right)\right)\wedge w_2\in \text{Dep}\left(u\right).\end{array}$$

(19)

The secure information flow Definition 6 provides

$$\begin{array}{cc}& \text{Pr}\left(u\right)\ge \mathrm{Re}\left(u\right).\end{array}$$

(20)

Theorem 5 provides that

$$\begin{array}{cc}& \mathrm{Re}\left(u\right)\ge \mathrm{Re}\left(w_2\right).\end{array}$$

(21)

And the Lemma 9 provides that

$$\begin{array}{cc}& \mathrm{Re}\left(w_1\right)\ge \mathrm{Re}\left(v\right).\end{array}$$

(22)

And there is

$$\begin{array}{cc}& \mathrm{Re}\left(w_2\right)=\mathrm{Re}\left(w_1\right).\end{array}$$

(23)

Based on (20), (21), (22), and (23), we can get

$$\begin{array}{cc}& \text{Pr}\left(u\right)\ge \mathrm{Re}\left(v\right).\end{array}$$

(24)

In a conclusion, the lemma is proved.

Theorem 11.

For a service chain $s_c$ , if the information flow in each service component $s_i$ is considered secure, the flow in the service chain is secure.

Proof.

Let $m=n+1$ , and the theorem is proved based on Lemma 10.

4. Distributed Information Flow Verification Framework for Wireless Service Composition

4.1. Information Flow Verification Framework

For a service chain $s_c=〈s_0,s_1,\dots ,s_n,s_{n+1}〉$ , there are several candidate services but different implementations by developers for each service step $s_i$ . In the distributed information flow verification framework, each sensor node is only responsible for validating its next-step candidate service node $s_{i,j}$ , which can balance the energy cost on a single verification node. The distributed information flow verification framework is shown in Figure 4.

Figure 4

Decentralized information flow verification framework.

In our framework, Service Authorization Centre (SAC) is a trusted third party for service certificate generation before the deployment of the sensor node. There are two phases for the verification of the information flow: service certificate setup and service verification phase. The service certificate that specifies the security properties of the service, that is, the dependence between the service input and output, is first generated and signed by a SAC. During the service composition procedure, the service composer obtains the required service certificates, and verifies the information flow in candidate nodes. These two phases are detailed in the following sections.

4.2. Service Certificate Setup

Service certificate setup is the preparation phase of the verification process, which is shown in Figure 5. In this phase, service developer submits authorization request containing service function code in service node to SAC. And then the generated service certificate $Ce$ is installed on the sensor node with the service. Considering the complexity and security of the service code transmission, the authorization process is executed by the offline mode between the service developer and SAC, which does not need to consume extra energy of the sensor node.

Figure 5

Service certificate setup phase.

Definition 12.

A service certificate $Ce$ is a tuple $〈CA,s,De〉$ , where $CA$ is the issuer, that is, SAC; s is the service identifier; $De$ is the set of statements that describe the output data dependence.

The service certificate $Ce$ specifies the attributes of the service including the service identifier, the dependence between input and output objects in the service function. Regarding the PDG construction of service function, SAC uses the algorithms presented in [13] to generate the PDG. Once a program dependence graph PDG = $〈V,\overrightarrow{E}〉$ has been computed, a dependence set can be established for each node $x\in V$ by using intraprocedural backward slice [14], written $De(x)$ containing the set of all nodes in PDG from which x can be reached as follows: $De(x)=\{y\mid y{\to }_{*}x\}$ . In this paper we mainly consider the dependences between the input and output objects in the PDG nodes; that is, $D{e}_{in}({Out}_{i,k})=\{v\mid v\in De({Out}_{i,k})\wedge v\in {In}_i\},0\le i\le n+1$ , $0\le k\le |{Out}_i|$ . For each ${Out}_{i,k}\in {Out}_i$ , its input dependence is written into the certificate. Finally, the certificate is signed by SAC and sent to the service node. Then the service certificate setup phase is complete. The Algorithm 1 is shown as follows.

Algorithm 1: Service_Certificate_Set_Up().

Input:  Service $s_i〈i{d}_i,do{m}_i,I{n}_i,Ou{t}_i,F_i,C{e}_i〉$ .

Output:  Service certificate of $C{e}_i〈CA,s,De〉$ .

$(1)$ ∖∖ Var $(x)$ represents the variables objects in x statement

$(2)$   $C{e}_i·s=i{d}_i$

$(3)$   PDG  $G〈V,\overrightarrow{E}〉$

$(4)$ generatePDG $(F_i,G)$

$(5)$   for  each output node $x\in G\wedge \mathit{V}\mathit{a}\mathit{r}(x)\in Ou{t}_i$  do

$(6)$   BS(x)=backwardSlice(x)

$(7)$   for  each $y\in \mathit{B}\mathit{S}(x)$  do

$(8)$     if  $\mathit{V}\mathit{a}\mathit{r}(y)\in I{n}_i$  then

$(9)$       pushInto( $C{e}_i·De(\mathit{V}\mathit{a}\mathit{r}(x),\mathit{V}\mathit{a}\mathit{r}(y)))$

$(\mathrm{10})$     end if

$(\mathrm{11})$   end for

$(\mathrm{12})$   end for

$(\mathrm{13})$ signature( $C{e}_i·CA,SAC$ )

$(\mathrm{14})$   return  $C{e}_i$

When there is a request for the service, the node needs to send its certificate to the composer for its information flow verification. The provided security levels of the public and local input data and output objects are also required to be sent to the verification node. If the realization of the service is changed, for example, a new version service is published, the service needs to be authorized by SAC again and reinstalled on the sensor node.

4.3. Service Verification

Service verification is a vital phase in which the verification node requires the service certificates and validates the candidate nodes against the information flow control policies. The verification procedure is shown in Figure 6. During the verification process, service composer $s_{i-1}$ , required for the service certificate and the provided security levels of the public and local data and objects first. Then the composer computes the required security levels of the output objects and then validates whether they satisfy the security constrains.

Figure 6

Service Verification Phase.

4.3.1. Required Security Level Computation

According to the secure information flow definition in service chain, the required security levels of the data objects need to be computed first. The required security levels of the objects in each service $s_{i,j}$ are computed according to the following three computation rules (CR):

$\text{CR}\mathrm{\hspace{0.17em}\hspace{0.17em}}1$ For $\forall u\in {In}_i^D\cup {In}_i^L$ , $\mathrm{Re}(u)=\text{Pr}(u)$ ;

$\text{CR}\mathrm{\hspace{0.17em}\hspace{0.17em}}2$ For $\forall u\in {In}_i^M$ , $\mathrm{Re}(u)=\text{Pr}(v)$ where $v\in {Out}_{i-1}^M\wedge v=u$ ;

$\text{CR}\mathrm{\hspace{0.17em}\hspace{0.17em}}3$ For $\forall u\in {Out}_i$ , $\mathrm{Re}(u)={\bigsqcup }_{\max }\mathrm{Re}(v)\mathrm{\hspace{0.17em}\hspace{0.17em}}\mathrm{\hspace{0.17em}\hspace{0.17em}}v\in I{n}_i\wedge v\in \text{Dep}(u)$ .

$\text{CR}\hspace{0.17em}1$ specifies that the required security levels of the input objects from public and local storage are equal to their provided security levels. $\text{CR}\hspace{0.17em}2$ specifies that the required security levels of the input objects from predecessor are determined by that of the output objects in $s_{i-1}$ . $\text{CR}\hspace{0.17em}3$ specifies that the required security levels of the output objects are computed from that of the input objects that the output depends on.

4.3.2. Service Verification

During the service verification, the information flow control policy (IFCP) specifies how to validate a candidate service $s_{i,j}$ . Based on the security label model and the definition of the secure information flow in each service, we define the information flow control policies in each service $s_i$ as follows:

$\text{IFCP}\mathrm{\hspace{0.17em}\hspace{0.17em}}1$ For $\forall u\in {Out}_i^D$ , $\text{Pr}(u)\ge \mathrm{Re}(u)\Rightarrow \text{true}$ , $\text{Pr}(u)<\mathrm{Re}(u)\Rightarrow \text{false}$ ;

$\text{IFCP}\mathrm{\hspace{0.17em}\hspace{0.17em}}2$ For $\forall u\in {Out}_i^L$ , $\text{Pr}(\text{u})\ge \mathrm{Re}(\text{u})\Rightarrow \text{true}$ , $\text{Pr}(\text{u})<\mathrm{Re}(\text{u})\Rightarrow \text{false}$ .

Based on the required security level computation rules and information flow control policies, verification node can validate the candidate sensor node $s_{i,j}$ in a service chain. The Algorithm 2 is shown as follows.

Algorithm 2: Service_Verification().

Input:  $\mathrm{Re}(Ou{t}_{i-1}^M)$ , Candidate Service Set $S_i$ , $\text{Pr}(I{n}_{i-1}^D)$ , $\text{Pr}(I{n}_{i-1}^L)$ , $\text{Pr}(Ou{t}_{i-1}^D)$ , $\text{Pr}(Ou{t}_{i-1}^L)$

Output:  Passed Service Set $S_{p,i}$ .

$(1)$ $\setminus \setminus$ exOutput $(I{n}_{i,j}^M)$ represents $I{n}_{i,j}^M$ 's corresponding output in its predecessor

$(2)$ $\setminus \setminus$ filterService $(S_p,S_{i,j})$ represents filtering the unsatisfied candidate service $s_{i,j}$ from $S_p$

$(3)$   $S_{p,i}=S_i$

$(4)$   for  each $s_{i,j}\in S_i$  do

$(5)$   requestCert $(s_{i,j},Ce)$

$(6)$   for  each $u\in I{n}_{i,j}^D,v\in I{n}_{i,j}^L,w\in I{n}_{i,j}^M$  do

$(7)$      $\mathrm{Re}(u)=\text{Pr}(u)$

$(8)$      $\mathrm{Re}(v)=\text{Pr}(v)$

$(9)$      $\mathrm{Re}(w)=\mathrm{Re}(\mathit{e}\mathit{x}\mathit{O}\mathit{u}\mathit{t}\mathit{p}\mathit{u}\mathit{t}(w))$

$(\mathrm{10})$   end for

$(\mathrm{11})$   for  each $u\in Ou{t}_i^D$ , $v\in Ou{t}_i^L$  do

$(\mathrm{12})$     for  each $w\in De(u)$  do

$(\mathrm{13})$        $\mathrm{Re}(u)={\bigsqcup }_{\max }\mathrm{Re}(w)$

$(\mathrm{14})$     end for

$(\mathrm{15})$     if  $\text{Pr}(u)<\mathrm{Re}(u)$  then

$(\mathrm{16})$        filterService $(S_{p,i},S_{i,j})$

(17)       break;

(18)     end if

(19)     for  each $w\in De(v)$  do

(20)        $\mathrm{Re}(v)={\bigsqcup }_{\max }\mathrm{Re}(w)$

(21)     end for

(22)      if  $\text{Pr}(v)<\mathrm{Re}(v)$  then

(23)        filterService $(S_{p,i},S_{i,j})$

(24)       break;

(25)     end if

(26)   end for

(27)  end for

(28)  return  $S_{p,i}$

4.4. Decentralized Information Flow Verification Algorithm for the Service Chain

For each step verification, verification node obtains the passed candidate service set $S_{p,i}$ , then the verification node will notice these passed sensor nodes to verify the following candidate services. And there are three types of messages for the synchronization of the verification procedure, that is, $start\_message$ , $success\_message$ , and $fail\_message$ . $start\_message$ is used to allow the candidate service $s_{i,j}$ to execute the $Verify\_ServiceChain()$ procedure. When the nodes in service chain all pass the service verification process, $success\_message$ with the executable path is sent to inform its requestor $s_0$ . During each step verification $fail\_message$ will be sent to the predecessor of the verification node when there are no candidate services passed the verification in next step. The Algorithm 3 is presented as above.

Algorithm 3: Verify_ServiceChain().

Input:  $\mathrm{Re}(Ou{t}_{i-1}^M)$ , Candidate Service Set $S_{i+1}$ .

Output:  Secure Execution Path P

$(1)$   if  $i\ne 1$  then

$(2)$    wait  start_message

$(3)$   end if

$(4)$   if  $i=n$  then

$(5)$    send success_message with secure execution path P to the requestor

$(6)$   else

$(7)$   push $S_{i,j}$ into the Execution Path P

$(8)$    $S_{p,i+1}=Service\_Verification(Re(Ou{t}_{i-1}^M),S_{i+1})$

$(9)$   if  $S_{p,i+1}=\varphi$  then

$(\mathrm{10})$     send  fail_message to its predecessor

$(\mathrm{11})$   else

$(\mathrm{12})$     for  each $s_{i+1,k}\in S_{p,i+1}$  do

$(\mathrm{13})$        send start_message to $s_{i+1,k}$

$(\mathrm{14})$     end for

$(\mathrm{15})$   end if

$(\mathrm{16})$ end if

5. Experiments and Evaluations

This paper studies distributed information verification framework for the service composition in WSN. Through the security analysis in Section 3, the information flow security can be ensured by the Theorem 11. In this section, we investigate the impact of distributed service verification on the sensor node's cost including verification time and communication effort. A centralized approach implements the service verification work by a single sensor node. We test both approaches with NS-3 [15] in multiple scenarios. Table 1 shows further details about the simulation configuration.

Table 1

Simulation Configuration.

General
Simulator	NS-3
Field ( ${\text{m}}^2$ )	$100\times 100$
Radio type	Zigbee
Service step	4
Simulation duration (s)	1000
Random
Node placement
Node movement
Security level	Unclassified, confidential, secret, and top secret
Controlled
Candidate number	5–10
Verification mode	Centralized, decentralized

Figure 7 shows the computation time on the verification node. In the centralized way, time rises vastly with the increase of the candidate service number. That is because the execution paths that need to be verified are increased at an exponential rate. However, time increases slowly in the distributed way because there is no significant variations on the candidate nodes that each sensor node needs to verify.

Figure 7

Computation time on the verification node(s).

Figure 8 shows the communication effort on the verification node. In Figure 8, the communication effort in the centralized way is evidently higher than that used the distributed way. That is because the single verification node needs to communicate with all other service nodes in centralized way, while it just needs to communicate with the next-step service nodes which can decrease the communication effort and save the energy of the sensor nodes.

Figure 8

Communication effort on the verification node(s).

6. Conclusion

In this paper, we specify the security constraints for each service participant based on the partial order model and propose a decentralized information flow verification approach that cooperates each sensor node to verify the information flow security distributively and builds up secure service chains in wireless sensor environments. Through the simulation on NS-3, the result shows that this approach can decrease the cost of the sensor nodes effectively.