Keywords

4.1 Introduction

Vulnerability of communication protocols can cause various kinds of attacks, which cause substantial damage to systems connected to the Internet. A denial-of-service attack is one of the constant concerns of computer security. It can make the usual services of a computer or network inaccessible to the regular users. An archetypal example of DoS attack is a SYN flooding attack [1] on the Transmission Control Protocol (TCP) (Fig. 4.1).

Fig. 4.1
figure 1

Three-way handshake of TCP

Full size image

Before sending data from a source host S to a destination host D, the hosts have to establish a connection between S and D, called three-way handshake. The host S begins by sending a SYN packet including an initial sequence number x. The host D then replies to S with a message in which the SYN and ACK flags are set, indicating that D acknowledges the SYN packet from the S. The message includes D’s sequence number y and incremented S’s sequence number (x + 1) as an ACK number. The host S sends a message with an ACK bit, a SEQ number (x + 1), and an ACK number (y + 1).

Consider a situation that lasts for a short period during which an attacker, A, sends an enormous number of connection requests with spoofed source IP-addresses to a victim host, D. The number of actual implementations of half-opened connections per port is limited since the memory allocation of data structures for such a connection is limited (Fig. 4.2).

Recently, several researchers have studied DoS attacks from various viewpoints, such as protection from DoS attacks using resource monitoring [2] and the development of DoS resistance analysis [3, 4]. She extended the Alice-and-Bob notation by attaching an atomic procedure annotation to each communication.

Fig. 4.2
figure 2

SYN-flood attack

Full size image

4.2 Process Calculus for Analyzing Denial-of-Service Attacks

4.2.1 The Spice Calculus

Tomioka et al. [5] proposed a formal system for DoS resistance analysis, the Spice calculus, which is based on Milner’s process calculus [6] and its extension for secure computation [7]. A characteristic feature of the calculus is a type system which enables us to track the computational cost of each computer node. The type of the Spice calculus represents the configuration of a distributed system.

For example, a typing of the Spice-calculus

$$ \mathcal{A}|(\mathcal{B}|\mathcal{C}) \triangleright P_{1} |(Q|P_{2}) $$

means that the process P_1 has the type on the left hand side. This notation means that \( {\mathcal{A}},{\mathcal{B}},{\mathcal{C}} \)

P 1 ,Q, P 2 has type \( {\mathcal{A}},{\mathcal{B}},{\mathcal{C}} \), respectively; more intuitively, this means that processes P 1 ,Q, P 2 are executed on machines \( {\mathcal{A}},{\mathcal{B}},{\mathcal{C}} \), respectively. The type \( {\mathcal{A}}|({\mathcal{B}}|{\mathcal{C}}) \) means a distributed system which consists of \( {\mathcal{A}},{\mathcal{B}},{\mathcal{C}} \). The types of Spice-calculus [5] are defined by the following grammar.

$$ {\mathcal{A}}\,::\,= {\mathbf{a}}::\left\{{x_{1}, \ldots,x_{n}} \right\}\,|\,(\mathcal{A}|\mathcal{B}) $$

The typing of the Spice-calculus contributes to the following:

  • identifying the origins of computational costs and

  • formalizing current memory usage during execution of processes.

The type a ∷ {x 1 ,…,x n } means that in the single computer node a, memory cells x 1 ,…,x n are occupied.

In order to track memory usage accurately, stricter restriction is imposed in the Spice-calculus than in Milner’s original process calculus, the pi-calculus. For example, a typing rule [5]

$$ \frac{{{\mathbf{a}}::\mathcal{V} \triangleright P\,\,\mathcal{V} \supseteq fv(M)\,\,\mathcal{V} \supseteq fv(N)}}{{{\mathbf{a}}::\mathcal{V} \triangleright {\mathsf{out}}\,M\left\langle N \right\rangle;P}}\,{\mathbf{TypeOut}} $$

The first assumption of this rule forces the process P to be executed on the single computer node a. Consequently, a term

$$ {\mathsf{inp}}\,n(x);(p\,|\,Q) $$

is not allowed in the Spice-calculus, since (P | Q)$ must be executed on a distributed system composed of multiple computer nodes.

The Spice-calculus is given operational semantics as a transition relation, in other words, small-step semantics. We can find the computational cost consumed in each transition step of the semantics. Moreover, we can identify not only the level of the computational cost but also the origin of this cost. For example, [5], a rule

$$ \frac{M \downarrow V:c}{{{\mathsf{hash}}(M) \downarrow hash_{V} :c + hash}} $$

formulate hash-value computation. The cost c is incurred for evaluation of M and hash for the hash-value computation. There are two kinds of transition relation between processes giving the operational semantics of the Spice-calculus: one is a reduction relation and another commitment relation. Inner-process computation is formalized as the reduction relation and inter-process computation as the commitment relation. The following is one of the rules defining the reduction relation:

$$ \frac{M \downarrow V:c\,\,\,N \downarrow V:d}{{({\mathsf{match}}\,M\,{\text{is}}\,N\,{\text{err}}\,\{ P\} ;Q)\,\, > \,\,Q:{\mathbf{a}} \cdot (c + d + match)}}{\mathbf{RedMatch}} $$

The costs for evaluating M and N are c and d, respectively. The resulting value of M and N is V. The following is one of the rules defining the commitment relation:

$$ \frac{{}}{{{\bf{a}}::\mathcal{V}\vdash\,{\rm{inp}}\,n (x ) ;P\mathop \to \limits^{n} (x)P:{\text{\{\bf{a}}} \cdot store_{x} {\text{\}}}}}\bf{CommIn} $$

In this rule, the process inp n(x); P is transit to an intermediate form (x)P, which is waiting for arrival of a message at the port n. The cost store x occurs at the node a.

Recently, Cervesato proposed another formal approach to quantitative analysis of secure protocols [8].

4.2.2 Formalization of Process Creation

In the existing version of the Spice-calculus [5], the costs of memory and computation, such as hashing and arithmetic operations, are formalized. However, the cost of process creation is overlooked. In this paper, we improve the Spice-calculus by adding the costs of process creation.

Actually, process creation entails a certain amount of cost. For example, in a variation of the Unix system, a Process Control Block (PCB) is allocated in a kernel memory space to save the process context when the process is created. Hence process-creating is considered as expensive. In order to formulate process creation in the Spice-calculus, we introduce several new rules for the operational semantics. In the reduction relation between processes, the process replication is represented as a rule

$$ {\text{repeat}}\,P > P\,|\,({\text{repeat}}\,P) $$

The cost of creating a process is represented as process and is incorporated into the rule as follows.

$$ {\text{repeat}}\,P > P\,|\,({\text{repeat}}\,P):{\mathbf{a}}\, \cdot process $$

The terminated process is formalized as the nil stop. In order to formalize elimination of the terminated processes precisely, we introduce another kind of terminated process end and we add a new reduction rule in which stop is transit to end as follows.

$$ {\text{stop}} > {\text{end}}:{\mathbf{a}} \cdot - process $$

When a process is terminated and eliminated, a cost process is deducted.

4.3 Example of Formalization: Three-Way Handshake

TCP’s three-way handshake is described as follows in the Alice-and-Bob notation.

$$ \begin{array}{*{20}c} {A \to B:A,B,S_{A} } \hfill \\ {B \to A:B,A,S_{B} ,S_{A} + 1} \hfill \\ {A \to B:A,B,S_{A} + 1,S_{B} + 1} \hfill \\ \end{array} $$

In the Spice-calculus, we can write the protocol as the following process expressions.

$$ \begin{array}{*{20}l} {P_{A} \,\mathop = \limits^{def} } \hfill & {{\text{new}}(S_{A} );} \hfill \\ {} \hfill & {{\text{store}}\,x_{sa} = S_{A} ;} \hfill \\ {} \hfill & {{\text{out}}\,c\left\langle {(A,\,B,\,x_{sa} )} \right\rangle ;} \hfill \\ {} \hfill & {{\text{inp}}\,c\,(p);} \hfill \\ {} \hfill & {{\text{split}}\,[x^{\prime}_{b} ,\,x^{\prime}_{a} ,\,x^{\prime}_{sb} ,\,x^{\prime}_{sa + 1} ]\,{\text{is}}\,p\,{\text{err}}\left\{ {{\text{free}}\,x_{sa} ,\,p} \right\};} \hfill \\ {} \hfill & {{\text{free}}\,p;} \hfill \\ {} \hfill & {{\text{match}}\,x^{\prime}_{sa} \,{\text{is}}\,A\,{\text{and}}\,x^{\prime}_{sb} \,{\text{is}}\,B\,{\text{and}}\,x^{\prime}_{sa + 1} \,{\text{is}}\,{\text{succ}}(x_{sa} )} \hfill \\ {} \hfill & {\,\,\,{\text{err}}\left\{ {{\text{free}}\,x_{sa} ,\,x^{\prime}_{b} ,\,x^{\prime}_{a} ,\,x^{\prime}_{sb} ,\,x^{\prime}_{sa + 1} } \right\};} \hfill \\ {} \hfill & {{\text{free}}\,x^{\prime}_{b} ,\,x^{\prime}_{a} ,\,x^{\prime}_{sa + 1} ;} \hfill \\ {} \hfill & {{\text{out}}\,c\,\left\langle {\left( {A,\,B\,{\text{succ}}\,(x_{sa} ),\,{\text{succ}}\,(x^{\prime}_{sb} )} \right)} \right\rangle ;} \hfill \\ {} \hfill & {P^{\prime}_{A} } \hfill \\ \end{array} $$
$$ \begin{array}{*{20}l} {P_{B}\, \mathop = \limits^{def} } \hfill & {{\text{new}}(S_{B} );} \hfill \\ {} \hfill & {{\text{inp}}\,c\,(q_{1} );} \hfill \\ {} \hfill & {{\text{split}}\,[y_{a} ,\,y_{b} ,\,y_{sa} ]\,{\text{is}}\,q_{1} \,{\text{err}}\left\{ {{\text{free}}\,q_{1} } \right\};} \hfill \\ {} \hfill & {{\text{free}}\,q_{1} ;} \hfill \\ {} \hfill & {{\text{match}}\,y_{b} \,{\text{is}}\,B\,{\text{err}}\left\{ {{\text{free}}\,y_{a} ,\,y_{b} ,\,y_{sa} } \right\};} \hfill \\ {} \hfill & {{\text{free}}\,y_{b} ;} \hfill \\ {} \hfill & {{\text{store}}\,y_{sb} = S_{B} ;} \hfill \\ {} \hfill & {{\text{out}}\,c\left\langle {\left( {B,\,y_{a} ,\,y_{sb} ,\,{\text{succ}}(y_{sa} )} \right)} \right\rangle ;} \hfill \\ {} \hfill & {{\text{inp}}\,c\,(q_{2} );} \hfill \\ {} \hfill & {{\text{split}}\,[y^{\prime}_{b} ,y^{\prime}_{a} ,\,y^{\prime}_{sa + 1} ,\,y^{\prime}_{sb + 1} ]\,{\text{is}}\,q_{2} \,{\text{err}}\left\{ {{\text{free}}\,y_{a} ,\,y_{sa} ,\,y_{sb} ,\,q_{2} } \right\};} \hfill \\ {} \hfill & {{\text{free}}\,q_{2} ;} \hfill \\ {} \hfill & {{\text{match}}\,y^{\prime}_{b} \,{\text{is}}\,B\,{\text{and}}\,y^{\prime}_{a} \,{\text{is}}\,y_{a} \,{\text{and}}\,y^{\prime}_{sa + 1} \,{\text{is}}\,{\text{succ}}(y_{a} )} \hfill \\ {} \hfill & {{\text{and}}\,y^{\prime}_{sb + 1} \,{\text{is}}\,{\text{succ}}\,(y_{sb} );} \hfill \\ {} \hfill & {\,\,\,{\text{err}}\left\{ {{\text{free}}\,y_{a} ,\,y_{sa} ,\,y_{sb} ,\,y^{\prime}_{b} ,\,y^{\prime}_{a} ,\,y^{\prime}_{sa + 1} ,\,y^{\prime}_{sb + 1} } \right\};} \hfill \\ {} \hfill & {{\text{free}}\,y^{\prime}_{b} ,\,y^{\prime}_{a} ,\,y^{\prime}_{sa + 1} ,\,y^{\prime}_{sb + 1} ;} \hfill \\ {} \hfill & {P^{\prime}_{B} } \hfill \\ \end{array} $$

Then a normal situation of communication between these two processes is represented as NormalConfig:

$$ NormalConfig\mathop = \limits^{def} ({\text{repeat}}\,P_{A}\, |\,{\text{repeat}}\,P_{B} ). $$

On the other hand, a situation of a SYN-flood attack [9] on the three-way handshake protocol is described in Alice-and-Bob notation as follows.

$$ \begin{aligned} I \to B:\, & I_{i} ,\,B,\,S_{I} \\ B \to I:\, & B,A,S_{B} ,S_{{I_{i} }} + 1 \\ & (i = 1,2, \ldots ) \\ \end{aligned} $$

The intruder in this attack is written as a process P I as follows.

$$ P_{I} \mathop = \limits^{def} {\text{new}}(i);\,{\text{new}}(s);{\text{out}}\,c\left\langle {(i,\,B,\,s)} \right\rangle ;{\text{stop}} . $$

Since the intruder spoofs the senders’ IP-addresses, the responding packets from the victim B are lost. In order to represent such lost packets, we introduce a process P N which formulates the network:

$$ P_{N} \mathop = \limits^{def} {\text{inp}}\,c(r);{\text{stop}} . $$

The attacking situation is written as a process AttackConfig:

$$ AttackConfig\mathop = \limits^{def} ({\text{repeat}}\,p_{I} \,|\,{\text{repeat}}\,p_{B} \,|\,{\text{repeat}}\,p_{N} ). $$

Then the process is typed as

$$ AttackConfig:({\mathbf{i}}|{\mathbf{b}}|{\mathbf{n}}) \triangleright ({\text{repeat}}\,p_{I}\, |\,{\text{repeat}}\,p_{B}\, |\,{\text{repeat}}\,p_{N} ). $$

Reducing the process AttackConfig, we know the level of costs consumed during execution.

$$ \begin{array}{*{20}l} {} \hfill & {AttackConfig} \hfill \\ { \to \to } \hfill & {new(S_{B} );({\text{stop}}\, | {\text{ repeat}}\,P_{A} |({\text{inp}}\,c\,(q_{2} ); \cdots )} \hfill \\ {} \hfill & {|{\text{repeat}}\,P_{B} |\,{\text{stop}}|{\text{repeat}}\,P_{N} )} \hfill \\ {} \hfill & {\,:\left\{ {{\mathbf{i}} \cdot proces,\,{\mathbf{b}} \cdot proces,\,{\mathbf{n}} \cdot proces} \right\}} \hfill \\ {} \hfill & {\,\, + \left\{ {{\mathbf{i}} \cdot pair,\,{\mathbf{b}} \cdot store} \right\}} \hfill \\ {} \hfill & {\,\, + \left\{ {{\mathbf{i}} \cdot - proces,\,{\text{b}} \cdot 2store,\,{\mathbf{b}} \cdot match} \right\}} \hfill \\ {} \hfill & {\,\, + \left\{ {{\mathbf{b}} \cdot pair,\,{\mathbf{n}} \cdot store} \right\}} \hfill \\ {} \hfill & {\,\, + \left\{ {{\mathbf{n}} \cdot - proces} \right\}} \hfill \\ {} \hfill & {\,\, = \left\{ {{\mathbf{i}} \cdot pair,\,{\mathbf{b}} \cdot proces,\,{\mathbf{b}} \cdot pair,} \right.} \hfill \\ {} \hfill & {\,\quad \left. {{\mathbf{b}} \cdot 3store,\,{\mathbf{b}} \cdot match,\,{\mathbf{n}} \cdot store} \right\}} \hfill \\ \end{array} $$

Here we know that not only memory cost but also process creation is consumed by the SYN-flood attack.

4.4 Conclusion

In our previous works, the Spice-calculus could analyze computational costs such as arithmetic operations, hash computation, and message transmission. However, the cost of process creation was disregarded. In this paper, we improved the Spice-calculus through adding cost evaluation of process creation and elimination. We extended the syntax of the cost in the Spice-calculus and operational semantics of the Spice-calculus. We then described TCP’s three-way handshake and the SYN-flood attack as examples of our new calculus.

As well as the work presented in this paper, we have several other subjects to study in future. One of the most important ones is formalizing and analyzing the SYN-cookie method against the SYN-flood attack and other DoS-resistant methods [10, 11].