preliminaries.tex 5.37 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
\section{Model learning background}
\subsection{Mealy machines} \label{mealy machines}
We use \textit{Mealy machines} to represent the state machine of SSH implementations. A Mealy machine is a a 6-tuple $\mathcal{M} = (Q, q_0, I, O, \delta, \lambda)$, where: 
\begin{itemize}
\item $Q$ is the set of states.
\item $q_0 \in Q$ is the initial state.
\item $I$ is the input alphabet.
\item $O$ is the output alphabet.
\item $\delta$ is the transition function $Q \times I \rightarrow Q$, which gives the resulting state from sending a certain input when in a certain state.
\item $\lambda$ is the transition function $Q \times I \rightarrow O$, which gives the received output when sending a certain input from a certain state.
\end{itemize}

A Mealy machine is deterministic, if for each state and input I, there exists 
Mealy machines can be graphically represented as a graph. States are shown as nodes and state transitions as edges. Edges are labeled as ``$<input>/<output>$'' corresponding to the transition functions: If $\delta(q_0, A) = q_1$ and $\lambda(q_0, A) = X$ then the label for the edge between $q_0$ and $q_1$ will be ``$A/X$''. An example visualization for a Mealy machine is shown in figure \ref{mealy example}.

\begin{figure}[h]
\centering
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
  \node[initial,state] (q0)      {$q_0$};
  \node[state]         (q1) [right of=q0]  {$q_1$};
  \node[state] 	(q2) [right of=q1] {$q_2$};

  \path[->]          (q0)  	edge                 node [below] {X/A} (q1);
  \path[->]          (q1)  	edge                 node [below] {Y/B} (q2);
  \path[->]		(q0)		edge 	[bend left]	node {Y/A} (q2);
  \path[->]		(q2) 	edge 	[loop right] 	node [text centered, text width = 1cm] {X/A \\ Y/B} (q2);
  \path[->]		(q1) 	edge	[loop below] node {X/B} (q1);
\end{tikzpicture}
\caption{Example Mealy machine}
\label{mealy example}
\end{figure}

\subsection{Learning state machines} \label{learning}
In protocol state fuzzing, a state machine of the implementation is learned by actively sending and receiving messages to and from the System Under Learning (SUL). A single message is called a \textit{query}, and a sequence of messages a \textit{trace}. The state machine is formed by sending consecutive traces to the SUL and analyzing the output. The trace to be sent is, in our case, determined by the L*-algorithm. When a trace is completed the SUL has to be reset to its initial state.  

After sending a sufficient amount of traces, a hypothesis is formed. The hypothesis is checked for  by a testing oracle. Said oracle sends traces to the SUL, predicts an output through the hypothesis, and compares this output to the actual output received by the SUL. 

In our case, sending messages to the SUL means sending packets that contain, for example, the length of the packet, a sequence number or a list of supported encryptions. This information is unnecessary for the learning process, and is not supported by the Learnlib implementation of L* that we use. We abstract all this information away, leaving us with an abstract representation of messages. To convert these abstract messages to correct packets and back, a mapper is used. This mapper has to keep track of state variables, and has to be able to perform actions such as encryption and compression. This means that the mapper itself contains a state machine, which is based on existing knowledge about the protocol used in the SUL.

\begin{figure}[h]
\centering
\includegraphics[scale=0.8]{Naamloos.png} 
\caption{A learning setup}
\label{learning setup}
\end{figure}

The setup shown in figure \ref{learning setup} is the setup Verleg used, and serves as an example for a typical learning setup, here ``Learner'' is the program that uses the L*-algorithm to generate traces to send to the SUL, these traces are in the form of abstract messages. The learner sends these messages to the mapper, which translates them to concrete packages which are sent to the SUL. A response of the SUL is then converted by the mapper to an abstract message and sent to the learner.

\subsection{Secure Shell} \label{secure shell}

The SSH-protocol uses a client-server structure consisting of three components. These components will be referred to as layers, however note that outer layers do not wrap inner layers, instead messages of different layers are distinguished through their message number. The three components are as follows: 
\begin{itemize}
\item The transport layer protocol. This creates the basis for communication between server and client, providing a key exchange protocol and server authentication. The key exchange protocol is performed through three roundtrips. During the first, both client and server send a KEXINIT message. Then, the client sends a KEX30 message, the server responds with a KEX31 message. Finally, both parties send a NEWKEYS message, which indicates that the keys sent in the second step can be used.
\item The user authentication protocol. This component is used to authenticate a client to the server, for example, through a username and password combination, or through SSH-keys.
\item The connection protocol. This is used to provide different services to the connected client, it can thus multiplex the encrypted channel into different channels. The provided services can be services like file transfer or a remote terminal. Typical messages are requests for opening or closing channels, or requests for earlier named services.
\end{itemize}