Security Testing of Internet of Things for Smart City Applications: A Formal Approach

Abstract

This is a work in progress in which we are interested in testing security aspects of Internet of Things for smart cities. For this purpose we follow a model-based approach which consists in: modeling the system under investigation with an appropriate formalism; deriving test suites from the obtained model; applying some coverage criteria to select suitable tests; executing the obtained tests; and finally collecting verdicts and analyzing them in order to detect errors and repair them. The adopted formalism is based on the model of extended timed automata with inputs and outputs. We propose a conformance testing relation, the so-called extended timed input–output conformance relation—etioco. For test execution, we introduce a cloud-based architecture.

1 Introduction

Internet of Things (IoT) is a promising technology that permits to connect everyday things or objects to the Internet by giving them the capabilities to sense the environment and interact with other objects and/or human beings through the Internet. This evolving technology has promoted a new generation of innovative and valuable services. Today cities are getting smarter by deploying intelligent systems for traffic control, water management, energy management, public transport, street lighting, etc., thanks to these services. Nevertheless, these services can easily be compromised and attacked by malicious parties in the absence of proper mechanism for providing adequate security.

Recent studies have shown that the attackers are using smart home appliances to launch serious attacks such as infiltrating to the network or sending malicious email or launching malicious actions such as distributed denial of service (DDoS) attack. Therefore, security solutions need to be proposed, set up, and tested to mitigate these identified attacks.

In this work, we aim to adopt a model-based security testing (MBST) approach to check the security of IoT applications in the context of smart cities. The MBST approach consists in specifying the desired IoT application in an abstract manner using an adequate formal specification language and then deriving test suites from this specification to find security vulnerabilities in the application under test in a systematic manner.

The work introduced here is an extension of a previous work [19] and it is a piece of a broader approach dealing with the security of IoT applications for smart cities and consisting of the following steps:

• Identify and assess the threats and the attacks in smart cities IoT applications.

• Design and develop security mechanisms for standard protocols at the application and the network layer.

• Evaluate the performance and the correctness of the proposed security protocols using simulation and implementation on real devices.

The rest of this paper is organized as follows. Section 26.2 introduces some preliminaries about IoT and smart cities. Section 26.3 defines the model of extended timed automata. Section 26.4 presents our conformance testing framework. Section 26.5 presents an overview about our proposed approach. Section 26.6 reports on related research efforts dealing with IoT security testing. Finally Sect. 26.7 concludes the paper.

2 Preliminaries

2.1 Internet of Objects

Recent advances in communication and sensing devices make our everyday objects smarter. This smartness is resulted from the capability of objects to sense the environment, to process the captured (sensed) data, and to communicate it to users either directly or through the Internet. Taking an example of the object “lamp,” a classical lamp needs to be wired, linked to the electricity in order to produce light and it does not handle more than the on and off states. This lamp becomes smarter if it is equipped with sensors that can detect environment luminosity and adjust its brightness automatically based on the sensed value. Moreover, this lamp can be equipped with a communication system and therefore can be remotely controlled and supervised (e.g., energy consumption). This example can be generalized to any other thing (object) and therefore leading to the Internet of Things (IoT) concept. The IoT refers to the ability of everyday objects to connect to the Internet and to send and receive data. The integration of these smart objects to the Internet infrastructure is promoting a new generation of innovative and valuable services for people. These services include home automation, traffic control, public transportation, smart water metering, waste and energy management, etc. When integrated in a city context, they make citizens live better and so form the modern smart city.

2.2 Smart Cities

In the recent years, several research works are shaping the smart cities concept [4, 34]. In October 2015, ITU-T’s Focus Group on Smart Sustainable Cities (FG-SSC)¹ agreed on the following definition of a smart sustainable city: A smart sustainable city (SSC) is an innovative city that uses information and communication technologies (ICTs) and other means to improve quality of life, efficiency of urban operation and services, and competitiveness, while ensuring that it meets the needs of present and future generations with respect to economic, social, and environmental aspects. Based on this definition, the main goal for SSC is to enhance the quality of life of its citizens across multiple, interrelated dimensions, including (but not limited to) the provision and access to water resources, energy, transportation and mobility, education, environment, waste management, housing, and livelihoods (e.g., jobs), utilizing ICTs as the key medium. Therefore, the IoT as a promising ICT technology will play a major role in the development of these new smart cities. With IoT, objects like phones, cars, household appliances, or clothes become wirelessly connected and can sense and share data.

2.3 Threats

Indeed, connecting our everyday things to the public Internet opens these objects to several kinds of attacks. Take the example of a traffic control system. If the hackers could insert fake messages to these traffic control system devices, they can make traffic perturbations and bottlenecks. Another example related to home automation, if attackers gain access to smart devices such as lamps and doors, it could manipulate doors and steal the house properties. The main security threats in the IoT are summarized in [8] as follows:

• Cloning of smart things by untrusted manufacturers;

• Malicious substitution of smart things during installation;

• Firmware replacement attack;

• Extraction of security parameters since smart things may be physically unprotected;

• Eavesdropping attack if the communication channel is not adequately protected;

• Man-in-the-middle attack during key exchange;

• Routing attacks;

• Denial-of-service attacks; and

• Privacy threats.

Therefore, a key challenge for IoT towards smart city applications is ensuring its reliability, security, and privacy, which represent the main scope of this work. Without guarantees that smart city IoT objects are: (1) sensing correctly the environment, (2) exchanging the information securely, (3) safeguarding private information, and (4) providing correct and not manipulated information, users are reluctant to adopt this new technology that will be a part of their everyday lives.

2.4 Challenges

Due to its specific characteristic, new issues are raised in the area of IoT. Trust management, which plays an important role in the IoT for reliable data fusion, qualified services, and enhanced user privacy and information security, is one of these main issues. Indeed, data collection trust is a crucial issue in the IoT. If the huge collected data is not trusted (e.g., due to the damage or malicious input of some sensors), the IoT service quality will be greatly influenced and hard to be accepted by users even though the network layer trust and the application layer trust can be fully provided [36]. On the other hand, in order to have intelligent context-aware services, users should disclose or have to share their personal data or privacy such as location, preferences, and contacts. Providing intelligent context-aware and personalized services and at the same time preserving user privacy are two conflicting objectives that induce a big challenges in the IoT. Another challenge faced when designing security solutions to the IoT is the limited resources of the IoT devices. Indeed, most of IoT devices are limited in terms of CPU, memory capacity, and battery supply. They often operate on lossy and low bandwidth communication channels. This renders the application of the conventional Internet security solutions not appropriate. As an example, the use of small packets (i.e., IEEE 802.15.4 supports only 127-bytes packets) may result in fragmentation of larger packets when using the standard protocols. This will quickly exhaust the lifetime of IoT devices and open new possibilities for DoS attacks [25]. Moreover, the limited resources of IoT devices render the use of complex cryptographic protocols inadequate. Finally, the inherent complexity of the IoT, where multiple heterogeneous entities located in different contexts can exchange information with each other, further complicates the design and the deployment of efficient, interoperable, and scalable security mechanisms [28]. The proposed security solutions should fulfill the following security requirements [26].

• Data confidentiality: make information inaccessible to unauthorized users. For example, a 6LoWPAN node should not leak some of its collected data to neighboring networks.

• Data authentication: since an adversary can easily inject messages, the receiver needs to ensure that data are originated from trusted sources.

• Data integrity: ensures that an adversary does not alter the received data in transit.

• Availability: ensures the survivability of network services to (only) authorized parties when needed, despite a DoS attack(s).

• Energy efficiency: a security scheme must be energy efficient so as to maximize the network lifetime.

3 Extended Timed Automata

We extend the framework presented in [18].

3.1 Timed Labeled Transition Systems

Let R be the set of non-negative reals, Q the set of non-negative rationals, and N the set of non-negative integers. Given a finite set of actions A c, the set (A c ∪R)^∗ of all finite-length real-time sequences over A c will be denoted R T(A c). 𝜖 ∈R T(A c) is the empty sequence. Given A c ^′⊆A c and ρ ∈R T(A c), $\mathsf {P}_{\mathsf {Ac}^{\prime }}({{\rho }})$ denotes the projection of ρ to A c ^′∪R, obtained by “erasing” from ρ all actions not in A c ^′∪R. Similarly, $\mathsf {DP}_{\mathsf {Ac}^{\prime }}({{\rho }})$ denotes the (discrete) projection of ρ to A c ^′. For example, if A c = {a, b}, A c ^′ = {a} and ρ = a 1 b 2 a 3, then $\mathsf {P}_{\mathsf {Ac}^{\prime }}({{\rho }}) = a \, 3 \, a \, 3$ and $\mathsf {DP}_{\mathsf {Ac}^{\prime }}({{\rho }}) = a \, a$. The time spent in a sequence ρ, denoted d u r a t i o n(ρ), is the sum of all delays in ρ, for example, d u r a t i o n(𝜖) = 0 and d u r a t i o n(a 1 b 0.5) = 1.5. In the rest of the document, we assume given a set of actions A c, partitioned in two disjoint sets: a set of input actions A c _in and a set of output actions A c _out. Actions in A c _in ∪A c _out are called observable actions. We also assume there is an unobservable action τ∉A c. Let A c _τ = A c ∪{τ}. A timed labeled transition system (TLTS) over A c is a tuple (S, s ₀, A c, T _d, T _t), where:

• S is a set of states;

• s ₀ is the initial state; T _d is a set of discrete transitions of the form (s, a, s ^′) where s, s ^′∈ S and a ∈A c;

• T _t is a set of timed transitions of the form (s, t, s ^′) where s, s ^′∈ S and t ∈R.

Timed transitions must be deterministic, that is, (s, t, s ^′) ∈ T _t and (s, t, s ^′′) ∈ T _t implies s ^′ = s ^′′. T _t must also satisfy the following conditions: (s, t, s ^′) ∈ T _t and (s ^′, t ^′, s ^′′) ∈ T _t implies (s, t + t ^′, s ^′′) ∈ T _t; (s, t, s ^′) ∈ T _t implies that for all t ^′ < t, there is some (s, t ^′, s ^′′) ∈ T _t.

We use standard notation concerning TLTS. For s, s ^′, s _i ∈ S, μ, μ _i ∈A c _τ ∪R, a, a _i ∈A c ∪R, ρ ∈R T(A c _τ) and σ ∈R T(A c), we have

• General transitions:

  • ; ;

  • ;

  • ;

  • ;

  • .

• Observable transitions:

  • or ;

  • ;

  • ; ;

  • ;

  • .

A sequence of the form is called a run and a sequence of the form an observable run.

3.2 Extended Timed Automata

We use timed automata [2] with deadlines to model urgency [18]. An extended timed automaton over A c is a tuple A = (Q, q ₀, X, I, A c, E), where:

• Q is a finite set of locations;

• q ₀ ∈ Q is the initial location;

• X is a finite set of clocks;

• I is a finite set of integer variables;

• E is a finite set of edges.

Each edge is a tuple (q, q ^′, ψ, r, inc, dec, d, a), where:

• q, q ^′∈ Q are the source and destination locations;

• ψ is the guard, a conjunction of constraints of the form x#c, where x ∈ X ∪I, c is an integer constant and # ∈{<, ≤, =, ≥, >};

• r ⊆ X ∪I is a set of clocks and integer variables to reset to zero;

• inc ⊆I is a set of integer variables (disjoint from r) to increment by one;

• dec ⊆I is a set of integer variables (disjoint from r and inc) to decrement by one;

• d ∈{l a z y, d e l a y a b l e, e a g e r} is the deadline;

• a ∈A c is the action.

An example of an extended timed automaton A = (Q, q ₀, X, I, A c, E) over the set of actions A c = {a, b, c, d} is given in Fig. 26.1 where:

• Q = {q ₀, q ₁, q ₂, q ₃} is the set of locations;

• q ₀ is the initial location;

• X = {x} is the finite set of clocks;

• I = {i} is the finite set of integer variables;

• E is the set of edges drawn in the figure.

The figure uses the following notation:

• “x := 0” means resetting the clock x to 0;

• “i := 0” means resetting the integer variable i to 0;

• “i + +” means incrementing i by 1;

• “i −−” means decrementing i by 1.

Fig. 26.1

An example of an extended timed automaton

3.3 Semantics of Extended Timed Automata

An extended timed automaton A = (Q, q ₀, X, I, A c, E) defines an infinite TLTS which is denoted $L_A=(S_A,s_0^A,\mathsf {Ac},T_d^A,T_t^A)$.

• Its states S _A are tuples s = (q, v _X, v _I), where:

  • q ∈ Q;

  • v _X : X →R is a clock valuation;

  • and v _I : I →N is a integer variable valuation.

• $s_0^A=(q_0,{\mathbf {0}}_{X},{\mathbf {0}}_{\mathsf {I}})$ is the initial state, where:

  • 0 _X is the valuation assigning 0 to every clock of A;

  • 0 _I is the valuation assigning 0 to every integer variable of A.

• Discrete transitions are of the form where a ∈A c and there is an edge (q, q ^′, ψ, r, inc, dec, d, a) such that (v _X, v _I) satisfies ψ and $(v^{\prime }_{X},v^{\prime }_{\mathsf {I}})$ is obtained by:

  • resetting to zero all clocks and integer variables in r;

  • incrementing integer variables in inc by one;

  • decrementing variables in dec by one;

  • leaving all other variables unchanged.

• Timed transitions are of the form where t ∈R, t > 0 and there is no edge (q, q ^′′, ψ, r, inc, dec, d, a) such that:

  • either d = d e l a y a b l e and there exist 0 ≤ t ₁ < t ₂ ≤ t such that (v _X + t ₁, v _I)⊧ψ and (v _X + t ₂, v _I)⊭ψ;

  • or d = e a g e r and (v _X, v _I)⊧ψ.

Lazy edges do not impact the semantics. They denote that an edge is neither delayable nor eager. More precisely, lazy edges cannot block time progress, whereas delayable and eager edges can. We do not allow d e l a y a b l e edges with guards of the form x < c since there is no latest time when the guard is still true. Similarly, we do not allow e a g e r edges with guards of the form x > c since there is no earliest time when the guard becomes true.

A state s ∈ S _A is reachable if there exists ρ ∈R T(A c) such that . The set of reachable states of A is denoted R e a c h(A).

For instance, for the TA presented in Fig. 26.1, the initial state is (q ₀, 0, 0). A possible timed transition of the system is which corresponds to the fact that the system spends 5 time units at node q ₀. A possible discrete transition is which corresponds to the execution of action a and results in the reset of clock x to 0. Another possible discrete transition is by which the integer variable i is incremented for the first time. The time constraint x ≤ 1 means that the execution of b must happen at most 1 time unit after the execution of a. The deadline delayable associated with this constraint means that time is blocked after one time unit and that it is compulsory to execute action b before that limit. It is not difficult to see that action b needs to be executed at least 5 times (resp., 10 times) in order to execute action c (resp., d).

3.4 Extended Timed Automata with Inputs and Outputs

An extended timed automaton with inputs and outputs (ETAIO) is an extended timed automaton over the partitioned set of actions A c _τ = A c _in ∪A c _out ∪{τ}. For clarity, we will explicitly include inputs and outputs in the definition of an ETAIO A and write (Q, q ₀, X, I, A c _in, A c _out, E) instead of (Q, q ₀, X, I, A c _τ, E).

• An ETAIO is called observable if none of its edges is labeled by τ.

• Given a set of inputs A c ^′⊆A c _in, an ETAIO A is called input-enabled with respect to A c ^′ if it can accept any input in A c ^′ at any state:

  

  It is simply said to be input-enabled when A c ^′ = A c _in.

• A is called l a z y -input with respect to A c ^′ if the deadlines on all the transitions labeled with input actions in A c ^′ are l a z y. It is called l a z y-input if it is l a z y-input with respect to A c _in. Note that input-enabled does not imply l a z y-input in general.

• A is called deterministic if:

  

• A is called non-blocking if:

  

  This condition guarantees that A will not block time in any environment.

The set of timed traces of an ETAIO A is defined to be

The set of observable timed traces of A is defined to be

The TLTS defined by an ETAIO is called a timed input–output LTS (TIOLTS). From now on, unless otherwise stated, all the considered ETAIO are defined with respect to the same sets A c _in and A c _out and unobservable action τ. As for ETAIO, a given TIOLTS L is denoted (S, s ₀, A c _in, A c _out, T _d, T _t) instead of (S, s ₀, A c _τ, T _d, T _t). The two operators T T r(⋅) and O T T r(⋅) are extended in a natural way to the case of TIOLTS.

3.5 Parallel Composition of ETAIO with Shared Integer Variables

The parallel composition we propose here is similar to the parallel composition for classical timed automata. The new thing here is that we consider shared variables between the different elements to compose. The shared variables can be incremented and decremented by any participant in the composition. These variables are used to formulate the constraints of the different automata. In this way the behaviors of the different components of the system are related to each other and depend on each other. For instance, the shared variables may represent the shared resources of the system.

Let n be a non-negative integer such that n ≥ 2. We consider n ETAIO (A _i)_1≤i≤n where $A_i=(Q^i,q^i_0,X^i,\mathsf {I},\mathsf {Ac}_{\mathsf {in}}^i,\mathsf {Ac}_{\mathsf {out}}^i,\mathsf {E}^i).$ That is the set of integer variables I is shared between all the considered ETAIO (A _i)_1≤i≤n while no other element from Q ⁱ, X ⁱ, $\mathsf {Ac}_{\mathsf {in}}^i$, and $\mathsf {Ac}_{\mathsf {out}}^i$ is shared with the other ETAIO (A _j)_j≠i.

The TIOLTS $L^{P}=(S^{P},s^{P}_0,\mathsf {Ac}_{\mathsf {in}}^{ P},\mathsf {Ac}_{\mathsf {out}}^{P},T_d^{P},T_t^{P})$ generated by the parallel product of the ETAIO (A _i)_1≤i≤n is defined as follows:

• $s^{P}_0=((q^1_0,\cdots ,q^n_0), ({\mathbf {0}}_{X^0},\cdots ,{\mathbf {0}}_{X^n}),{\mathbf {0}}_{\mathsf {I}})$;

• $\mathsf {Ac}_{\mathsf {in}}^{P}= \bigcup _{1\le i\le n}\mathsf {Ac}_{\mathsf {in}}^i,\, \mathsf {Ac}_{\mathsf {out}}^{P}=\bigcup _{1\le i\le n}\mathsf {Ac}_{\mathsf {out}}^i$;

• and S ^P, $T_d^{P}$, and $T_t^{P}$ are the smallest sets such that

  • $s_0^P\in S^P$;

  • For and δ ∈R:

    
    

  • For $s^P=((q^1,\cdots ,q^n), (v_{X^0},\cdots ,v_{X^n}),v_{\mathsf {I}})\in S^P$, 1 ≤ i ≤ n and $a_i\in {\mathsf {Ac}_\tau }^i=\mathsf {Ac}_{\mathsf {in}}^i\cup \mathsf {Ac}_{\mathsf {out}}^i\cup \{\tau \}$):

    
    

    where

    $$\displaystyle \begin{aligned}q^{\prime p}=(q^1,\cdots,q^{i-1},q^{\prime i},q^{i+1},\cdots,q^n)\end{aligned}$$

    and

    $$\displaystyle \begin{aligned}v^{\prime p}_{X}=(v_{X^0},\cdots,v_{X^{i-1}},v^{\prime}_{X^i},v_{X^{i+1}}\cdots,v_{X^n}).\end{aligned}$$

It is worth noticing here that it is possible to define the parallel composition of n copies (A _i)_1≤i≤n of the same ETAIO A. In this case we assume it is possible to distinguish the sets of inputs and outputs of the different instances by a particular identifier corresponding to each instance. Obviously, the n instances share the set of integer variables of the ETAIO A. The obtained TIOLTS is denoted $L_n^P$.

4 Conformance Testing Framework

In this section, we are going to define a new extended timed input–output conformance relation, etioco. Then, we propose a new approach for deriving analog-clock tests from the SUT specification. Finally, we discuss both test execution and correctness requirements.

4.1 Conformance Relation

In order to formally define the conformance relation, we define a number of operators. Given a TIOLTS $L=(S^L,s^L_0,\mathsf {Ac}_{\mathsf {in}}^L,\mathsf {Ac}_{\mathsf {out}}^L,T^L_d,T^L_t)$ and a timed trace σ ∈R T(A c ^L) L a f t e r σ is the set of all states of L that can be reached by some timed sequence ρ whose projection to observable actions is σ. Formally: Given state s ∈ S ^L, e l a p s e(s) is the set of all delays which can elapse from s without L making any observable action. Formally: Given state s ∈ S ^L, o u t(s) is the set of all observable “events” (outputs or the passage of time) that can occur when the system is at state s. The definition naturally extends to a set of states S. Formally: and

$$\displaystyle \begin{aligned} \mathsf{out}(S) = \bigcup_{s\in S} \mathsf{out}(s).\end{aligned}$$

The specification of the system to be tested is given as a non-blocking ETAIO A _S while the implementation can be modeled as a non-blocking, input-enabled ETAIO A _I. For n ≥ 1, let $L^P_{S,n}$ (resp., $L^P_{I,n}$) be the parallel composition of n copies of A _S (resp., A _I). Input-enabledness is required so that the implementation can accept inputs from the tester at any state. The extended timed input–output conformance relation, denoted e t i o c o, is an extension of our previous conformance relation t i o c o [17, 18]. The new relation e t i o c o is defined as $A_I \;\mathsf {etioco}\; A_S\ \textit {iff}\ \ \forall n\ge 1 \wedge \sigma \in \mathsf {OTTr}(L^P_{S,n}) \;:\ \mathsf {out}(L^P_{I,n} \;\mathsf {after}\; \sigma ) \subseteq \mathsf {out}(L^P_{S,n} \;\mathsf {after}\; \sigma ).$The relation states that an implementation A _I conforms to a specification A _S iff for any number of copies n of A _S and any observable behavior σ of $L^P_{S,n}$, the set of observable outputs of $L^P_{I,n}$ after any behavior “matching” σ must be a subset of the set of possible observable outputs of $L^P_{S,n}$. Notice that observable outputs are not only observable output actions but also time delays. Also notice that in case we consider only n = 1, the definitions of e t i o c o and t i o c o become the same.

4.2 Analog-Clock Tests

A test (or test case) is an experiment performed on the implementation by an agent (the tester). There are different types of tests, depending on the capabilities of the tester to observe and react to events. In general, one may consider either analog-clock or digital-clock tests [11]. In this work, we consider only analog-clock tests. The latter can measure precisely the delay between two observed actions and can emit an input at any point in time.

It should be noted that we consider adaptive tests (following the terminology of [21]), where the action the tester takes depends on the observation history. For n ≥ 1, let A c ⁿ (resp., $\mathsf {Ac}_{\mathsf {in}}^n$) denote the union of all observable actions (resp., all input actions) of n copies of the specification A _S. An analog-clock test for n parallel executions of A _S is a total function $T_n : \mathsf {RT}(\mathsf {Ac}^n) \rightarrow \mathsf {Ac}_{\mathsf {in}}^n \cup \{\mathsf {Wait},\mathsf {Pass},\mathsf {Fail}\}. \ T_n(\rho )$ specifies the action the tester must take once it observes ρ:

• If $T_n(\rho )=a\in \mathsf {Ac}_{\mathsf {in}}^n$, then the tester emits input a.

• If T _n(ρ) = W a i t, then the tester waits (lets time elapse).

• If T _n(ρ) ∈{P a s s, F a i l}, then the tester produces a verdict (and stops).

4.3 Test Execution and Correctness Requirements

The execution of the test T _n on the implementation A _I can be defined as the parallel composition of the TIOLTS defined by T _n and $L^P_{I,n}$ the TIOLTS corresponding to n copies of A _I, with the usual synchronization rules for transitions carrying the same label. We will denote the product TIOLTS by $L^P_{I,n} \| T_n$. The execution of the test reaches a pass/fail verdict after bounded time. Formally, we say that A _I passes the test, denoted A _I p a s s e s T _n, if state F a i l is not reachable in the product $L^P_{I,n} \| T_n$. We say that an implementation passes (resp. fails) a set of tests (or test suite) ${\mathcal {T}}$ if it passes all tests (resp. fails at least one test) in ${\mathcal {T}}$. We say that an analog-clock test suite ${\mathcal {T}}$ is sound with respect to A _S if

$$\displaystyle \begin{aligned}\forall A_I \;:\; A_I \;\mathsf{etioco}\; A_S \Rightarrow A_I \;\mathsf{passes}\; {\mathcal{T}}.\end{aligned}$$

We say that ${\mathcal {T}}$ is complete with respect to A _S if

$$\displaystyle \begin{aligned}\forall A_I \;:\; A_I \;\mathsf{passes}\; {\mathcal{T}} \Rightarrow A_I \;\mathsf{etioco}\; A_S.\end{aligned}$$

5 Proposed Approach

In this section, we define a workflow that covers the different steps of a classical model-based testing process, namely: model Specification, test generation, test selection, test execution, and evaluation activities as depicted in Fig. 26.2.

Fig. 26.2

Model-based security testing process

5.1 Test Generation and Selection

Test Generation

We adapt the untimed test generation algorithm of [30]. Roughly speaking, the algorithm builds a test in the form of a tree. A node in the tree is a set of states S of the specification and represents the “knowledge” of the tester at the current test state. The algorithm extends the test by adding successors to a leaf node, as illustrated in Fig. 26.3. For all illegal outputs a _i (outputs which cannot occur from any state in S) the test leads to F a i l. For each legal output b _i, the test proceeds to node S _i, which is the set of states the specification can be in after emitting b _i (and possibly performing unobservable actions). If there exists an input c which can be accepted by the specification at some state in S, then the test may decide to emit this input (dashed arrow from S to S ^′). At any node, the algorithm may decide to stop the test and label this node as P a s s.

Fig. 26.3

Test generation principle [18]

Algorithm 1 On-the-fly analog-clock test generation

Analog-clock tests cannot be directly represented as a finite tree, because there is an a-priori infinite set of possible observable delays at a given node. To remedy this, we use the idea of [31]. We represent an analog-clock test as an algorithm. The latter essentially performs subset construction on the specification automaton, during the execution of the test. Thus, our analog-clock testing method can be classified as on-the-fly or on-line, meaning that the test is generated at the same time it is executed. More precisely, the tester will maintain a set of states S of the TIOLTS $L^P_{S,n}$.

S will be updated every time an action is observed or some time delay elapses. Since the time delay is not known a-priori, it must be an input to the update function. We define the following operators:

and

where a ∈A c ⁿ and t ∈R. d s u c c(S, a) contains all states which can be reached by some state in S performing action a. t s u c c(S, t) contains all states which can be reached by some state in S via a sequence ρ which contains no observable actions and takes exactly t time units. The test operates as follows. It starts at state $S_0 = \mathsf {tsucc}(\{s_{n,0}^P\},0)$ where $s_{n,0}^P$ is the initial state of $L^P_{S,n}$. Given current state S:

• if output a is received t time units after entering S, then S is updated to d s u c c(t s u c c(S, t), a).

• If ever the set S becomes empty, the test announces F a i l.

• At any point, for an input b, if d s u c c(S, b) ≠ ∅, the test may decide to emit b and update its state accordingly.

On-line analog-clock test generation is performed by Algorithm 1. The algorithm keeps running as long as no non-conformance is detected. At any time the tester can stop testing and declare P a s s. The algorithm uses the following notation. Given a nonempty set X, p i c k(X) chooses randomly an element in X.

Given a set of states S, v a l i d_i n p u t s(S) is defined as the set of valid inputs at S, that is: $\mathsf {valid\_inputs}(S)=\{a\in \mathsf {Ac}_{\mathsf {in}}^n|\mathsf {dsucc}(\mathsf {tsucc}(S,0),a)\ne \emptyset \}.$ Following the same methodology as in [18] we can prove that the proposed test generation algorithm is both sound and complete. Indeed both frameworks and both approaches are based on IOLTS and at this level the algorithms are the same and the conformance relations are equivalent. The difference between the two frameworks is only at syntactic and structural levels. In [18] the authors consider only one instance of the system whereas in our case we consider many instances which interact with each other and the behaviors of which are influenced by the total number of active components and the state of the shared resources.

The used test generation technique is based on model checking. The main idea is to formulate the test generation problem as a reachability problem that can be solved with the model checker tool UPPAAL [3]. However, instead of using model annotations and reachability properties to express coverage criteria, the observer language is used.

In this direction, we reuse the finding of Hessel et al. [14] by exploiting its extension of UPPAAL, namely UPPAAL CO√ER.² This tool takes as inputs a model, an observer, and a configuration file. The model is specified as a network of timed automata (.xml) that comprises a SUT part and an environment part. The observer (.obs) expresses the coverage criterion that guides the model exploration during test case generation. The configuration file (.cfg) describes mainly the interactions between the system part and the environment part in terms of input/output signals. It may also specify the variables that should be passed as parameters in these signals. As output, it produces a test suite containing a set of timed traces (.xml).

Our test generation module is built upon these well-elaborated tools. The key idea here is to use UPPAAL CO√ER and its generic and formal specification language for coverage criteria to generate tests for security purposes.

Test Selection

Different coverage criteria have been proposed for software, such as statement coverage and branch coverage [24]. In the TA case existing methods attempt to cover either finite abstractions of the state space (e.g., the region graph [29]) or structural elements of the specification such as edges or locations [14]. Here, we propose a technique for covering states, locations, edges, actions, or shared variables of the specification:

• State coverage: As already mentioned each node of a given test case corresponds to a set of states S of $A_S^{\mathsf {Tick}}$. We say that the node covers S. We say that such a test covers the union of all sets of states covered by its nodes. We say that a set of tests (or test suite) achieves state coverage if every reachable state of $L^P_{S,n}$ is covered by some test in the suite.

• Location coverage: A test suite achieves location coverage if every reachable location of A _S is covered by some test in the suite.

• Edge coverage: Every edge of a test case can be associated with an edge of $L^P_{S,n}$. In particular, an edge will be associated with all edges which are visited during the reachability algorithm which computes S ^′ from S. We say that a test suite achieves edge coverage if every reachable edge of $L^P_{S,n}$ is covered by some test in the suite.

• Action coverage: We also define action coverage as follows. If a given edge is reachable, then the corresponding observable action a is said to be reachable as well. Action coverage is achieved if all the reachable observable actions are covered by the considered test suite.

• Shared integer variable coverage: Finally we define shared integer variable coverage which consists in generating tests which cover the different possible values of the system variables.

5.2 Test Execution and Verdict Analysis

For the execution of the obtained security tests, we aim to use a standard-based test execution platform, called TTCN-3 test system for runtime testing (TT4RT), developed in a previous work [20]. To do so, security tests should be mapped to the TTCN-3 notation since our platform supports only this test language. Then, test components are dynamically created and assigned to execution nodes in a distributed manner.

Each test component is responsible for (1) stimulating the SUT with input values, (2) comparing the obtained output data with the expected results (also called oracle), and (3) generating the final verdict. The latter can be pass, fail, or inconclusive. A pass verdict is obtained when the observed results are valid with respect to the expected ones. A fail verdict is obtained when at least one of the observed results is invalid with respect to the expected one. Finally, an inconclusive verdict is obtained when neither a pass nor a fail verdict can be given. After computing for each executed test case its single verdict, the proposed platform deduces the global verdict.

5.3 Cloud Testing

The emergent paradigm, cloud computing, is formally defined by U.S.NIST (National Institute of Standards and Technology) [23] as follows. Cloud computing is a model for enabling ubiquitous, convenient, on-demand network access to a shared pool of configurable computing resources (e.g., networks, servers, storage, applications, and services) that can be rapidly provisioned and released with minimal management effort or service provider interaction.

This cloud model is characterized with three service models: software as-a-service (SaaS), platform as-a-service (PaaS), and infrastructure as-a-service (IaaS). The SaaS refers to the capability provided to the consumer to use the provider’s applications running on a cloud infrastructure. With PaaS, the consumer is able to deploy his own applications without installing any platform or tools since he uses provided platform layer resources, including operating system support and software development frameworks. Regarding IaaS, it provides a collection of resources such as servers, storage, networks, and other computing resources in the form of virtualized systems, which are accessed through the Internet.

It is worthy to note that public cloud providers like Amazon Web Services³ and Google Cloud Platform⁴ offer a cloud infrastructure made up essentially of availability zones and regions. As shown in Fig. 26.4, a region is a specific geographical location in which public cloud service providers’ data centers reside. Each region is further subdivided into availability zones. Several resources can live in a zone, such as instances or persistent disks. In the context of Google Cloud Platform, the us-central1 region, for example, denotes a region in the Central United States that has four zones, namely us-central1-a, us-central1-b, us-central1-c, and us-central1-f.

Fig. 26.4

Illustration of cloud partitioning in regions and zones

Cloud computing has been used in the context of software testing to encounter the lack of resources and the expensiveness of building a distributed test environment during the testing process. As a result, the concept of cloud testing is newly emerging in order to provide cost-effective testing services. According to [7], it refers to testing activities, essentially test generation, test execution, and test evaluation on a cloud-based environment. The latter supports on-demand resource allocation to large-scale testers whenever and wherever they need by following the pay-per-use business model. Such virtualized and shared resources may reduce effectively the cost of building a distributed test environment for the runtime validation of dynamically adaptive systems.

Testing as-a-service (TaaS) is an innovative concept that provides end users with testing services such as test case generation, test execution, and test result evaluation. It has been proposed to improve the efficiency of software quality assurance. Notably, it is used for software systems that are remotely deployed in a virtualized runtime environment using shared hardware/software resources, and hosted in a third-party infrastructure (i.e., a cloud). One of the primary objectives is to reduce the cost of software testing tasks by providing on-demand testing services and also on-demand test environment services (i.e., establishing the required virtual (or physical) cloud-based computing resources and infrastructures for testing purposes).

5.4 Test Execution Platform as-a-Service

The proposed approach is built based on TaaS concepts. Figure 26.5 outlines an overview of its different constituents.

Fig. 26.5

Test execution platform overview

• Test management GUI: This component offers a graphical user interface (GUI) charged with managing the overall testing process: the automatic creation/deletion of VM instances, the dynamic allocation of test components to the appropriate VMs, the start-up of test component execution, and the computation of the final verdict. Moreover, it is responsible for querying the runtime monitoring component for information about the usage of resources in running VMs.

• Resource management: This component enables flexibility and elasticity during the testing process. If there is no adequate VM to handle the execution of a test component, a new VM can be created and started automatically. Moreover, it is possible to scale up or scale down an existing VM. The unused one can be released as well.

• Test component management: This component offers services for creating/deleting test components and starting/stopping their execution. A test component is an entity that interacts with the SUT to execute the available test cases (i.e., a set of input values and expected results) and to observe its response related to this excitation. Its main role consists of stimulating the SUT with the input values, comparing the obtained output values to the expected results and generating the final verdict that can be pass, fail, or inconclusive.

• Runtime monitoring: This component monitors VM instances during or even before the test execution and gives the status of each VM in terms of computing resources (such as CPU, memory, and storage).

As already discussed, several VM instances are created and started in the proposed cloud infrastructure in which several components under test are running too and can be evolved at runtime. To perform runtime tests in a cost-effective manner, several test components should be deployed in the final execution environment. The major question to be tackled here is how to assign efficiently test components to the existing VM instances?

Before answering to this question, we should mention that the components under test are distributed in several VM instances that can be located in the same region and in the same zone as well as in different zones and even in different regions of the cloud infrastructure. Such information is provided via a SUT deployment descriptor. In this file, the SUT manager defines, for each component under test, the VM instance hosting its execution and also its main characteristics (i.e., its IP address, its corresponding zone, and region). Hereafter, we denote the VM hosting a component under test by VM under test (VMUT) and the VM hosting the test component by test VM (T_VM).

6 Related Work

In this section we give an overview of contributions from the literature and from our previous work related to the security of IoT applications in smart cities.

Although the security protocols are well elaborated in the Internet domain, it is still not fully clear how these existing IP security protocols and architectures can be adapted and deployed in the context of distributed and heterogeneous environment like the Internet of Things (IoT). From its appearance as a promiscuous technology, several works are addressing the security problems of the IoT [4, 8, 12, 13, 26, 28, 32, 36], but until now there is no sufficient solutions that meet the users’ requirements and performance needs. In the following, we will provide an overview of the most important related works and clarify the contributions of our proposal in comparison to the state of the art.

The authors in [4] presented the security contributions of the SMARTIE work, which aims to provide secure IoT data management for smart cities. The authors first classified attacks to internal and external. Internal attacks are caused by devices and/or users of the smart city environment. Internal attackers are more dangerous than external ones as they have detailed knowledge about the infrastructure, they have access to part of the systems and they hold some keys. Internal attackers can be users or administrators of the smart city systems or any hackers that succeed to compromise a component of the system. Note that, due to the diversity of the IoT devices and their spread in different locations, device compromise attack is easier in IoT than in classical networks. On the other hand, external attackers may try to access private data from users, components, or subsystems of the IoT environment. Moreover, as in IoT some components are controlled remotely, attackers can exploit these features to gain control and manipulate victims devices. Two main security mechanisms are defined in [4] to address the above issues. First, DCapBAC [13] is an authorization scheme that takes access control decisions before the actual service is accessed. It does this by giving a signed authorization token to a user who is asking for any particular service or functionality offered by a thing. The authorization token is sent along with a request to the thing that verifies the validity of the request and the authorization token, delivering the requested data, if successful. Second, PrivLoc [33] offers secure location-based services, in particular a secure geo-fencing service that alerts users if objects enter or leave a defined area. Location-based services are increasingly gaining importance. Not only end users but also companies can make use of location data to track assets (e.g., public transport services, users looking for transportation, or logistics companies). PrivLoc scrambles location information in a way that allows computation on intersections of scrambled geometric objects, which is the main operation behind a geo-fencing service.

In paper [32], the authors proposed OSCAR (object security architecture for the Internet of Things), an architecture for end-to-end security in the Internet of Things. It is based on the concept of object security that relates security with the application payload. The architecture includes authorization servers that provide clients with access secrets that enable them to request resources from constrained nodes. The nodes reply with the requested resources that are signed and encrypted. Although this architecture solves some of disadvantages of Datagram Transport Layer Security (DTLS) since it supports multicast, asynchronous traffic, and caching, it has certain limitations. Indeed, OSCAR is vulnerable to the replay attack and its performance is affected with the eventual usage of larger elliptic curve cryptography (ECC) curves. In [12], an architectural reference model-compliant framework was proposed. This framework emphasizes on security and privacy aspects to be used on smart buildings scenarios. Additionally, authors proposed an extension of the security functional components of the reference architecture in order to enable more flexible sharing models, in which the physical context information is considered as a first-class component in order to realize the so-called context-aware security on IoT scenarios. As an instantiation of this framework, a platform for services management on smart buildings has been deployed and extended to offer both user-centric services, like comfort and energy saving, and discovery and security functionality for such services. The feasibility of the proposed mechanisms has been demonstrated through the instantiation of the platform and its evaluation in a smart building used as reference [4].

From a standardization perspective, the recently standardized constrained application protocol (CoAP) was proposed as a lightweight alternative to the HTTP protocol for web-based IoT applications, but security does not keep up. For this purpose, the IETF has thus taken a position to reuse the datagram transport layer security (DTLS), the all-round point-to-point security protocol, to secure the communication channel between a constrained device running CoAP and a client [32]. However, apart from its current incompatibility with caching and multicast traffic, the DTLS approach has an important impact on scalability: Memory limitations of constrained nodes restrict the number of DTLS sessions. In IoT scenarios such as smart cities in which a large number of clients may communicate with constrained CoAP nodes, the limitations lead to a considerable load that translates to an increased energy consumption and a shortened lifetime [32]. Several works have thus been proposed to overcome these limitations of DTLS.

The DTLS in constrained environments (DICE), an IETF working group, was formed to add multicast security to DTLS [15]. In [15], the authors present a method for securing IPv6 multicast communication based on the DTLS which is already supported for unicast communication for CoAP devices. They deal with the adaptation of the DTLS record layer to protect multicast group communication, assuming that all group members already have the group security association parameters in their possession. The adapted DTLS record layer provides message confidentiality, integrity, and replay protection to group messages using the group keying material before sending the message via IPv6 multicast to the group [15]. However, the authors did not present how group members can agree on the group security association.

In [33], the authors presented Lithe—an integration of DTLS and CoAP for the IoT. Lithe proposes a novel DTLS header compression scheme that aims to reduce the energy consumption by leveraging the 6LoWPAN standard based on reducing the number of transmitted bytes while maintaining DTLS standard compliance.

Granjal et al. [9], described mechanisms to enable security at the network layer, based on the IPSec protocol, and at the application layer, based on the DTLS protocol, and performed an extensive experimental evaluation study with the goal of identifying the most appropriate secure communication mechanisms and the limitations of current sensing platforms for supporting end-to-end secure communications in the context of Internet-integrated sensing applications [9]. These results showed a similar performance of the two approaches, except in the case when DTLS is additionally used to exchange keys with the elliptic curve Diffie-Hellman exchange.

Heer et al. [10] discussed the applicability and limitations of existing Internet protocols and security architectures in the context of IoT. They presented challenges and requirements for IP-based security solutions and highlighted specific technical limitations of standard IP security protocols. It was indicated that for supporting secure IoT, its security architecture should fit the life cycle of a thing and its capabilities, and scale from small-scale ad-hoc security domains of things to large-scale deployments, potentially spanning several security domains. Security protocols should further take into account the resource-constrained nature of things and heterogeneous communication models. Lightweight security mechanisms and group security that are feasible to be run on small things and in IoT context should be developed, with particular focus on possible DoS/DDoS attacks. In addition, cross layer concepts should be considered for an IoT-driven redesign of Internet security protocols.

The authors in [35] addressed the routing protocol for low-power and lossy networks (RPL) attacks and they provided a comprehensive analysis of IoT technologies and their new security capabilities that can be exploited by attackers or IDSs. One of the major contributions in [35] is the implementation and demonstration of well-known routing attacks against 6LoWPAN networks running RPL as a routing protocol. The implemented attacks are selective-forwarding attacks (where malicious nodes selectively forward packets and therefore can achieve a DoS attack), sinkhole attacks (where a malicious node advertises an artificial beneficial routing path and attracts many nearby nodes to route traffic through it), HELLO flood attacks (where the attackers by broadcasting a HELLO message with strong signal power and a favorable routing metric can introduce himself as a neighbor to many nodes, possibly the entire network), wormhole attacks, clone ID, and Sybil attacks. In order to mitigate these attacks, the authors proposed an intrusion detection system (IDS), called SVELTE [27].

SVELTE [27], an intrusion detection system for the IoT was designed, implemented, and evaluated against routing attacks such as spoofed or altered information, sinkhole, and selective-forwarding. SVELTE’s overhead is small enough to deploy it on constrained IoT nodes with limited energy and memory capacity. However, SVELTE assumes that it has access to the border router of the network to place heavyweight IDS parts there. This assumption is not always possible. For example in a smart city application, the messages can be routed over a cellular station that belongs to the network of another owner and therefore we did not have access to the border router.

The previously cited proposed solutions can be classified to three categories which are application layer security solutions [15, 33], network layer security solutions [27, 35], and context-aware security solutions [4, 12, 32]. Context-aware security solutions are very dependent to the specific characteristics of the applications use case and so suffer from the lack of inter-operability. Moreover, the existing solutions have a high computation and communication cost that make them inadequate to resource-constrained things. Network security solutions are limited to attacks related to network layer and so cannot mitigate attacks that target the application layer and cannot provide some security services such as authentication and access control.

Contrary to [27, 35] that proposed an IDS that is limited to routing attacks. In this work we aim to extend the functionality of the IDS and to address also the application layer attacks that target the CoAP protocol. This kind of IDS will present a first line of defense and will mitigate several attacks such as the DoS attack. In addition, this work will focus on providing security based on the DTLS protocol as there are several attempts to make this protocol as the standard for security in the IoT. Therefore, we will propose enhancements to the DTLS protocol to fit the IoT objects. Moreover, we will focus on not resolved aspects such as group key management and multicast communication.

The authors of [6] propose a good survey on more than one hundred publications on model-based security testing extracted from the most relevant digital libraries and classified according to specific criteria. Even though this survey reports on a large number of articles about MBST it does not contain any reference to IoT applications or smart cities. Contrary to that the authors of [1] propose a model-based approach to test IoT platforms (with tests provided as services) but they do not deal with security aspects at all.

7 Conclusion

In this work we aimed to combine these two directions, namely: model-based testing and security testing for IoT applications in smart cities. For that purpose we took advantage of our previous findings [5, 16, 20, 22] related to these fields. Moreover, we extended the notions proposed in the survey [5] to the case of IoT applications. We also exploited our previous results about test techniques of dynamic distributed systems [16, 20].

Our work is at its beginning and a lot of efforts are needed at all levels on both theoretical and experimental aspects. First we need to deal with modeling issues. In this respect we need to extend our modeling formalism and to identify the particular elements of IoT applications to model (using extended timed automata). Models must not be big in order to avoid test number explosion. For that purpose we need to keep an acceptable level of abstraction. As a second step we have to adapt our test generation and selection algorithms to take into account security requirements of the applications under test. The new algorithms must be validated theoretically and proved to be correct. In the same manner we need to upgrade our tools to implement new obtained algorithms. We also need to validate our approach with concrete examples with realistic size. Finally we propose to adopt the same methodology as in [22] to combine security and load tests for IoT applications.