More smart objects and more applications on the Internet of Things (IoT) mean more security challenges. In IoT security is crucial but difficult to obtain. On the one hand the usual trade-off between highly secure and usable systems is more impelling than ever; on the other hand security is considered a feature that has a cost often unaffordable. To relieve this kind of problems, IoT designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. Here, we present a preliminary methodology, based on the process calculus I o T - Ly S a, to infer quantitative measures on systems evolution. The derived quantitative evaluation is exploited to establish the cost of the possible security countermeasures.
Within few years the objects we use every day will have computational capabilities and will be always connected to the Internet. In this scenario, called the Internet of Things (IoT), these “smart” devices are equipped with sensors to automatically collect different pieces of information, store them on the cloud or use them to affect the surrounding environment through actuators. For instance, our smart alarm clock can drive our heating system to prepare us a warm bathroom in the morning, while an alarm sensor in our place can directly trigger an emergency call to the closest police station. Also, in a storehouse stocking perishable food, equipped with sensors to determine the internal temperature and other relevant attributes, the refrigeration system can automatically adapt the temperature according to the information collected by sensors.
The IoT paradigm introduces new pressing security challenges. On the one hand, the usual trade-off between highly secure and usable systems is more critical than ever. On the other hand, security is considered a costly feature for devices with limited computational capabilities and with limited battery power.
Back to the refrigerator system above, an attacker can easily intercept sensors communications, manipulate and falsify data. We can resort to cryptography and ? Work supported by project PRA_2016_64 “Through the fog” (University of Pisa). Copyright c by the paper’s authors. Copying permitted for private and academic purposes. to consistency checks to prevent falsification and to detect anomalies. But is it affordable to secure all the communications? Can we still obtain a good level of security by protecting only part of communications?
IoT designers have to be selective, e.g. in choosing which packets to encrypt. To this aim, designers not only need tools to assess possible risks and to study countermeasures, but also methodologies to estimate their costs. The cost of security can be computed in terms of time overhead, energy consumption, bandwidth, and so on. All these factors must be carefully evaluated for achieving an acceptable balance among security, cost and usability of the system.
First, we introduce functions over the enhanced labels to associate costs to transitions. Here, the cost of a system is specified in term of the time spent for transitions, and it depends on the performed action as well as on the involved nodes. However, we can easily treat other quantitative properties, e.g. energy consumption. Intuitively, cost functions define exponential distributions, from which we compute the rates at which a system evolves and the corresponding CTMC. Then, to evaluate the performance we calculate the stationary distribution of the CTMC and the transition rewards.
Usually, formal methods provide designers with tools to support the development of systems and to reason about their properties, both qualitative and quantitative. Here, we present some preliminary steps towards the development of a formal methodology to support the analysis of the security cost in IoT systems. We aim at providing a general framework with a mechanisable procedure (with a small amount of manual tuning), where quantitative aspects are symbolically represented by parameters. Their instantiation is delayed until hardware architectures and cryptographic algorithms are fixed. By only changing these parameters designers could compare different implementations of an IoT system and could choose the better trade-off between security and costs.
Technically, we define an enhanced semantics for I o T - Ly S a, a process
calculus recently proposed to model and reason about IoT systems [
Structure of the paper. In the next section, we briefly introduce the process calculus I o T - Ly S a. In Section 3, we present a simple function that assigns rates to transitions, and we show how to obtain the CTMC associated with a given system of nodes and how to extract performance measures from it. Concluding remarks and related work are in Section 4.
In [
Syntax. In I o T - Ly S a systems N ∈ N consist of a fixed number of nodes that host control processes P ∈ P and sensors S ∈ S. The syntax is in Tab. 1, where V denotes the set of values, while X and Z are the local and the global variables, respectively, and K ⊆ V denotes the set of cryptographic keys (e.g. K0). N 3 N ::= systems of nodes 0 ` : [B] N1 | N2 inactive node single node composition
B 3 B ::= node components
P S B k B process sensor composition P ::= control processes 0 hE1, · · · , Eki. P hhE1, · · · , Ekii . L. P (E1, · · · , Ej ; xj+1, · · · , xk). P P1 + P2 A(y1, . . . , yn) decrypt E as {E1, · · · , Ej ; xj+1, · · · , xk}K0 in P (i; zi).P ({i; zi}K ).P S ::= sensor processes τ.S hi, vi. S h{i, v}K i. S A(y1, . . . , yn) nil intra-node output multi-output L⊆ L input (with match.) summation recursion decryption (with match.) clear input from sensor i crypto input from sensor i
E ::= terms internal action v value ith output x variable ith enc. output z sensor’s variable recursion {E1, · · · , Ek}K0 encryption
f (E1, · · · , En) function appl.
In the syntax of systems, 0 denotes the null inactive system; a single node ` : [B] is uniquely identified by a label ` ∈ L (which represents a node property such as location). Node components B are obtained by the parallel composition (through the operator ||) of control processes P , and of a fixed number of sensors S. We assume that sensors are identified by an unique identifier i ∈ I`.
In the syntax of processes, 0 represents the inactive process (inactive components of a node are all coalesced). The process hE1, · · · , Eki. P sends the tuple E1, · · · , Ek to another process in the same node and then continues like P .
The process hhE1, · · · , Ekii . L.P sends the tuple E1, . . . , Ek to the nodes whose labels are in L and evolves as P . The process (E1, · · · , Ej ; xj+1, · · · , xk). P receives a tuple E10, · · · , Ek0: if the first j terms of the received message pairwise match the first j terms of the input tuple, the message is accepted, otherwise is discarded (see later for details). The operator k describes parallel composition of processes, while + denotes non-deterministic choice. An agent is a static definition of a parameterised process. Each agent identifier A has a unique defining equation of the form A(y1, . . . , yn) = P , where y1, . . . , yn are distinct names occurring free in P . The process decrypt E as {E1, · · · , Ej ; xj+1, · · · , xk}K0 in P tries to decrypt an encrypted value using the key K0, provided that the first j elements of the decrypted term coincide with the terms Ej .
A sensor can perform an internal action τ or send an (encrypted) value v, gathered from the environment, to its controlling process and continues as S. We do not provide an explicit operation to read data from the environment but it can be easily implemented as an internal action.
Finally, in the syntax of term, a value represents a piece of data (e.g. keys or values read the environment). As said above, we have two kinds of disjoint variables: x are standard local variables, used as in π-calculus; while sensor variables z belong to a node and are globally accessible within it. As usual, we require that variables and names are disjoint. The encryption function {E1, · · · , Ek}K0 returns the result of encrypting values Ei for i ∈ [1, k] with the key K0. The term f (E1, · · · , En) is the application of function f to n arguments; we assume given a set of primitive aggregation functions, e.g. functions for comparing values. Working Example We set a simple IoT system up to keep the temperature under control inside a storehouse with perishable food (a big quadrangular room). We install four sensors, one for each corner of the storehouse. Each sensor Si periodically senses (by means of the function sensei()) the temperature and sends it through a wireless communication to a control unit Pc in the same node N1. The unit Pc computes the average temperature and checks if it is within accepted bounds. If this is not the case, Pc sends an alarm through other nodes and the Cloud. We want to prevent an attacker from intercepting and manipulating data sent by sensors. A possible approach consists in exploiting the fact that sensors on the same side should sense the same temperature, with a difference that can be at most a given value . The control unit can easily detect anomalies and discard data tailored by an attacker, comparing values coming from the sensors that are on the same side of the room. But what happens if the attacker falsifies the data sent by more than one sensor? A possible solution consists in enabling some sensors (in our example S1 and S3) to use cryptography for obtaining reliable data. Nevertheless, before adopting this solution we would like to evaluate it by estimating its cost. The control process Pc in the node N1 reads data from sensors, compares them and compute their average and sends them to the node N2. The process Qc of N2 sends an alarm or an ok message to the node N3 depending on the received data, together with the average temperature. The process Rc of N3 is an Internet service that waits for messages from N2 and handles them (through the internal action τ ). The I o T - Ly S a specification of the storehouse system follows:
N = N1 | N2 | N3 = `1 : [Pc k (S0k S1k S2k S3)] | `2 : [Qc k 0] | `3 : [Rc k 0] Pc = (0; z0). τ.({1; z1}K1 ).τ.(2; z2). τ.({3; z3}K3 ).τ.
hhcmp(z0, ..., z3), avg(z0, ..., z3)ii . {`2}.τ.Pc Qc = (true; xavg).hhok, xavgii . {`3}.τ.Qc + (false; xavg).hhalarm, xavgii . {`3}.τ.Qc Rc = (; wres, wavg).τ.Rc Sm = hm, sensem()i. τ.Sm m = 0, 2 Sj = h{j, sensej()}Kj i. τ.Sj j = 1, 3 The function cmp performs consistency checks, by comparing data coming from insecure sensors with data from secure ones: it returns true if data are within the established bounds, false otherwise. The function avg computes the average of its arguments. We suppose that processes and sensors perform some internal activities (τ -actions). Another possible solution consists in having just one sensor that uses cryptography. This new system of nodes Nˆ differs from the previous one in the specification of the process Pˆc in the first node:
Pˆc = (0; z0). τ.({1; z1}K1 ).τ.(2; z2). τ.(3; z3). τ.
hhhalfcmp(z0, z1), avg(z0, ..., z3)ii . {`2}.τ.Pˆc where the comparison function halfcmp uses only two arguments. We expect that this second solution is less expensive, and we apply our methodology to formally compare the relative costs of the two solutions.
Enhanced Operational Semantics. To estimate cost, we give an enhanced
reduction semantics following [
As usual, our semantics consists of the standard structural congruence ≡ on nodes, processes and sensors and of a set of rules defining the transition relation. Our notion of structural congruence ≡ is standard except for the following congruence rule for processes that equates a multi-output with empty set of receivers to the inactive process: hhE1, · · · , Ekii . ∅.0 ≡ 0.
θ
Our reduction relation −→⊆ N × N is defined as the least relation on closed nodes, processes and sensors that satisfies a set of inference rules. Our rules are quite standard apart from the five rules for communications shown in Tab. 2 and briefly commented below. We assume the standard meaning for terms [[E]]. (Sensor-Com) ` : [hi, vii. Si k (i; zi). P k B] h` out,` ini ` : [Si k P {vi/zi} k B{vi/zi}]
−→ (Crypto-Sensor-Com) ` : [h{i, vi}K i. Si k ({i; zi}K ).P k B] h` {out},` {in}i ` : [Si k P {vi/zi} k B{vi/zi}] → (Intra-Com)
Vk i=1 vi = [[Ei]] ∧
Vj
i=1 [[Ei]] = [[Ei0]] ` : [hE1, ..., Eki. P k (E10, ..., Ej0 ; xj+1, ..., xk).Q k B] h` out,` ini
→ ` : [P k Q{vj+1/xj+1, ..., vk/xk} k B] (Multi-Com) `2 ∈ L ∧ Comp(`1, `2) ∧
Vk i=1 vi = [[Ei]] ∧
The rule (Sens-Com) is for communications among sensors and processes: the variables used in the input are assumed global inside the node, in such a way that sensors are considered as a shared data structure z1, · · · , zn. Therefore, the substitution is performed in all the processes of the node. The rule (CryptoSens-Com) is similar but it also requires that the receiving process successfully decrypts the encrypted data sent by a sensor. The rule (Intra-Com) is for intranode communications. This construct implements also a matching feature: the communication succeeds, as long as the first j values of the message match the evaluations of the first j terms in the input. If this is the case, the result of evaluating each Ei is bound to each xi.
The rule (Multi-Com) implements the inter nodes communication: the communication between the node labelled `1 and the node `2 succeeds, provided that (i) `2 is in the set L of receivers, (ii) the two nodes are compatible according to the compatibility function Comp, and (iii) the matching mechanism succeeds. If this is the case, the sender removes `0 from the set of receivers L, while in the second node, the receiving process continues bounding the result of each Ei to each variable xi. Outputs terminate when all the nodes in L have received the message (see the congruence rule). Note that point-to-point communication amounts to the case in which L is a singleton. The compatibility function Comp defined over node labels is used to model constraints on communication, e.g. proximity, with Comp(`1, `2) that yields true only when the two nodes `1, `2 are in the same transmission range. Of course, this function could be enriched for considering other notions of compatibility.
Hereafter, we assume the standard notion of transition system. Intuitively, it is a graph, in which systems of nodes form the nodes and (labelled) arcs represent the possible transitions between them. As will be clearer in the next section, we will only consider finite state systems, because finite states have an easier stochastic analysis. Note that this does not mean that the behaviour of such processes is finite, because their transition systems may have loops. Example (cont’d) Back to our example, consider the following run of the first system where, for brevity, we ignored their internal actions τ
N −θ→0 N 0 −θ→1 N 00 −θ→2 N 000 −θ→3 N 0000 −θ→4i ( N000000 −θ→50 N if i = 0
N100000 −θ→51 N if i = 1 the systems of nodes N 0, N 00, N 000, N 0000, N 00000 are the intermediate ones reached from N during the computation and the labels θj annotate the jth transition (θji depending on the branch of the summation). In the run, fully specified below, the sensors of N1 send a message to the process Pc, which checks the received data and sends the checking result to N2. We denote with Pc0 (Q0c, Rc0, resp.) the continuations of Pc (Qc, Rc, resp.) after the first input prefixes, with vcomp the value cmp(v0, ..., v3), with vavg the value avg(v0, ..., v3), and with vresi (with i = 0, 1) the value ok (alarm respectively), depending on which branch of the summation is chosen. The evolution of the second system Nˆ is analogous to the one of N : the transition labels are such that θ4i = h`1hhhalfcmp(v0, v1), avg(v0, · · · , v3)ii, `2(vbool; xavg)i and θˆl = θl for l 6= 4i ˆ (the transition labels θl are presented below, after the run of N ). N = `1 : [(0; z0). Pc0 k P k (h0, sense0()i. τ.S0k S1k S2k S3)] | N2 | N3 −θ→0 N 0 = `1 : [Pc0{0/z0} k (τ.S0k S1k S2k S3)] | N2 | N3 −θ→1−θ→2−θ→3 N 0000 = `1 : [Pc0{0/z0, 1/z1, 2/z2, 3/z3} k (S0k S1k S2k S3)] | N2 | N3 = `1 : [hhvcomp, vavgii . {`2}.τ.Pc k (S0k S1k S2k S3)] | `2 : [(true; xavg).hhok, xavgii . {`3}.τ.Qc +
(false; xavg).hhalarm, xavgii . {`3}.τ.Qc] | N3 −θ→4i
Ni00000 = `1 : [Pc k P k (S0k S1k S2k S3)] |
`2 : [Q0c{vavg/xavg}) k 0] |`3 : [(; wres, wavg).τ.Rc k 0] =
`1 : [Pc k P k (S0k S1k S2k S3)] |
`2 : [hhvresi , vavgii . {`3}.τ.Qc k 0] | `3 : [(; wres, wavg).τ.Rc k 0] −θ→5i
N
= `1 : [Pc k P k (S0k S1k S2k S3)] |`2 : [Qck0] |`3 : [Rc0{vresi /wres, vavg/wavg}k0]
θ0 = θ2 = h`1hj, vji, `1(j; zi)i
θ1 = θ3 = h`1h{j, vj}Ki i, `1({j; zj}Ki )i
θ4i = h`1hhcmp(v0, · · · , v3), avg(v0, · · · , v3)ii, `2(vbool; xavg)i
θ5i = h`2 hhvresi , vavgii, `3(wres, wavg)i
We now show how to generate a Continuous Time Markov Chains (CTMC) from
a transition system (see [
Technically, we interpret costs as parameters of exponential distributions
F (t) = 1 − e−rt, with rate r and t as time parameter (general distributions
are also possible see [
We define in a few steps the function that associates rates with the (enhanced
labels of) communication and decryption transitions. For the sake of simplicity, we
ignore the costs for other primitives, e.g. constant invocation, parallel composition,
summation, τ actions (see [
• $α(hE1, . . . , Eki) = fout(fE (E1), ..., fE (E1), bw) • $α((E1, . . . , Ej ; xj+1, . . . , xk)) = fin(fE (E1), ..., fE (Ej ), match(j), bw) • $α(decrypt E as {E1, · · · , Ej ; xj+1, · · · , xk}E0 ) =
fdec(fE (E), crypto_system, kind(K0), match(j)) the send and receive primitives. Besides the implementation cost due to their own algorithms, the functions above depend on the bandwidth of the channel (represented by bw), on the cost of the exchanged terms (computed by fE ), and on the nodes involved in the communication. Moreover, the inter-node communication depends on the proximity-relation (e.g. the transmission range between nodes), represented here by the function f<>(`O, `I ). Also, the cost of an input depends on the number of required matchings (represented by match(j)). Finally, the function fdec represents the cost of a decryption, whose cost is similar to the one for encryption, with the additional cost of matchings. Finally, the function $ : Θ → IR+ associates rates with enhanced labels.
• $(h`O out, `I ini) = f<>(`O, `I ) · min{$α(out, `O), $α(in, `I )} • $h` deci = $α(dec, `) As mentioned above, the two partners independently perform some low-level operations locally to their nodes, labelled `O and `I . Each label leads to a delay in the rate of the corresponding action. Thus, the cost of the slower partner corresponds to the minimum cost of the operations performed by the participants in isolation. Indeed the lower the cost, i.e. the rate, the greater the time needed to complete an action and hence the slower the speed of the transition (and the slower F (t) = 1 − e−rt approaches its asymptotic value).
Note that we do not fix the actual cost function: we only propose for it a set of parameters to reflect some features of an idealised architecture. Although very abstract, this suffices to make our point. A precise instantiation comes with the refinement steps from specification to implementations as soon as actual parameters become available.
Example (cont’d) We now associate a rate to each transition in the transition system of the system of nodes N , just N for brevity. To illustrate our methodology, we assume that the coefficients due to the nodes amount to 1. We instantiate the cost functions given above, by using the following parameters in the denominator: (i) e and d for encrypting and for decrypting; (ii) s and r for sending and for receiving; (iii) m for pattern matching; and (iv) f for the application of the aggregate function f , whose cost is proportional to the number of its arguments. • fE (a) = 1
Pk
• fE ({E1, . . . , Ek}K0 ) = se · 1 i=1 fE (Ei) + 1
• $α(hE1, . . . , Eki) = s·Pii=1 fE(Ei) 1
• $α((E1, . . . , Ej ; xj+1, . . . , xk)) = r·k+m·j
1
• $α(decrypt E as {E1, · · · , Ej ; xj+1, · · · , xk}K0 ) = d·k+m·j
• $α(f (E1, · · · , Ek)) = f1·k
These parameters represent the time spent performing the corresponding action
on a single term. Intuitively, the greater the time duration is, the smaller the rate.
Since transmission is usually more time-consuming than reception, the rate of a
communication is that of output. The rates of the transitions of N and Nˆ are
cj = $(θj ) and cˆj = $(θˆj ), and cji = $(θji) and cˆji = $(θˆji) (j ∈ [
1 1 cˆ4i = 6f+2s
For instance, the rate of the second transition is: c1 = $(θ1) = 2e1+s , where 2e1+s = min{ 2e1+s , 2d+1r+m }. Note that our costs can be further refined; we could e.g. make the transmission rate also depend on the distance between the nodes, when non internal to a node.
Stochastic Analysis Now, we transform the transition system N into its
corresponding CT M C(N ), by using the above rates. Afterwards, we can calculate
the actual performance measures, e.g. the throughput or utilisation of a certain
resource (see [
Actually, the transition rate q(Ni, Nj ) at which a system jumps from Ni to Nj is the sum of the single rates ϑk of all the possible transitions from Ni to Nj . Given a transition system N , the corresponding CTMC has a state for each node in N , and the arcs between states are obtained by coalescing all the arcs with the same source and target in N . Recall that a CTMC can be seen as a directed graph and that its matrix Q, the generator matrix, (apart from its diagonal) represents its adjacency matrix. Note that q(Ni, Nj ) coincides with the off-diagonal element qij of the generator matrix Q. Hence, hereafter we will use indistinguishably CTMC and its corresponding Q to denote a Markov chain. More formally, the entries of Q are defined as follows.
q(Ni, Nj ) = P $(θk) if i 6= j ∧ Ni −θ→k Nj qij = θk
n − P qij if i = j
j=0,j6=i Performance measures are usually obtained by computing the stationary distributions of CT M Cs, since they should be taken over long periods of time to be significant. The stationary probability distribution of a CTMC is Π = (X0, . . . , Xn−1) s.t. ΠT Q = 0 and Pn
i=0 Xi = 1, which uniquely exists if the transition system is finite and has a cyclic initial state. Example (cont’d) Consider the transition system corresponding to N that is, as required above, finite and with a cyclic initial state. We derive the following generator matrix Q1 of CT M C(N ) and the corresponding stationary distribution Π1, where C = 4s + 2e + 2f, by solving the system of linear equations Π1T Q1 = 0 and Pn
i=0 Xi = 1, where Π1 = (X0, · · · , X6). Similarly, we can derive the generator matrix Qˆ01 and the corresponding stationary distribution Πˆ1 for the transition system corresponding to Nˆ , where Cˆ = 9s + 2e + 3f. Πˆ1 = h 2Cˆs , (2eCˆ+s) , 2ˆCs , 2ˆCs , (3fˆC+s) , 2sCˆ , 2sCˆ i
To define performance measures for a system N , we define the corresponding
reward structure, following [
Definition 2. Given a system N , let Π = (X0, . . . , Xn−1) be its stationary distribution and ρ = ρ(0), ..., ρ(n − 1) be its reward structure. The total reward of N is computed as R(N ) = Pi ρ(i) · Xi.
Example (cont’d) To evaluate the relative efficiency of the two systems of nodes,
we compare the throughput of both, i.e. the number of instructions executed per
time unit. The throughput for a given activity is found by first associating a
transition reward equal to the activity rate with each transition. In our systems
each transition is fired only once. Also, the graph of the corresponding CTMC is
cyclic and all the labels represent different activities. Therefore the throughput
of all the activities is the same, and we can freely choose one of them to compute
the throughput of N . Thus we associate a transition reward equal to its rate with
the last communication and a null transition reward with all the others
communi1
cations. The total reward R(N ) of the system then amounts to 2(8s+4e+4f) , while
R(Nˆ ) to 2(9s+2e+3f) . By comparing the two throughputs, it is straightforward to
1
obtain that R(N ) < R(Nˆ ), i.e. that, as expected, Nˆ performs better. To use this
measure, it is necessary to instantiate our parameters under various hypotheses,
depending on several factors, such as the network load, the packet size, and so on.
Furthermore, we need to consider the costs of cryptographic algorithms and how
changing their parameters impact on energy consumption and on the guaranteed
security level (see e.g. [
In the IoT scenario security is critical but it is hard to address in an affordable
way due to the limited computational capabilities of smart objects. We have
presented the first steps towards a formal framework that supports designers in
specifying an IoT system and in estimating the cost of security mechanisms. A
key feature of our approach is that quantitative aspects are symbolically
represented by parameters. Actual values are obtained as soon as the designer provides
some additional information about the hardware and the network architecture
and the cryptographic algorithms relative to the system in hand. By abstractly
reasoning about these parameters designers can compare different
implementations of the same IoT system, and choose the one that ensures the best trade-off
between security guarantees and their price. In practice, we considered a subset
of the process algebra I o T - Ly S a [
Our approach follows the well-established line of research about performance
evaluation through process calculi and probabilistic model checking (see [