Commit d31ea149 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Some more updates on the model checking part, updated references...

parent 1c7fb75e
......@@ -18,23 +18,25 @@ The learner uses LearnLib ~\cite{LearnLib2009}, a Java library implementing $L^{
SSH is a complex client-server type protocol. It would be exceedingly difficult to learn all its facets, thus we narrow down the learning goal to learning SSH
server implementations. We further restrict learning to only exploring the terminal service of the connection layer, as we consider it to be the most interesting
from a security perspective. Algorithms for encryption, compression and hashing are set to default settings and are not purposefully explored.
from a security perspective. Algorithms for encryption, compression and hashing are set to default settings and are not purposefully explored. Also, the starting
state of the {\dsut} is one where a TCP connection has been established and where SSH versions have been exchanged, a required first step of the Transport Layer protocol.
%figure
%It is therefore important to focus on messages for which interesting state-changing behaviour can be expected.
\subsection{The learning alphabet}
We split the learning alphabet into 3 groups, corresponding to the three layers. Each input in the alphabet has a corresponding message type in the SSH specification.
We split the learning alphabet into 3 groups, corresponding to the three layers. %Each input in the alphabet has a corresponding message number in the SSH specification.
Learning doesn't scale with a growing alphabet, hence it is important to reduce the alphabet to those inputs that trigger interesting behavior. We do this by
only selecting inputs that are consistent with our learning goal.
Since we are learning only SSH server implementations, we filter out messages that were not intended to be sent to the server. \footnote{Applying this principle to
the RFC's messages results in not including \textsc{service\_accept}, \textsc{ua\_accept}, \textsc{ua\_failure}, \textsc{ua\_banner}, \textsc{ua\_pk\_ok}, \textsc{ua\_pw\_changereq}, \textsc{ch\_success} and \textsc{ch\_failure} in our alphabet.} Furthermore, from the Connection layer we only select general inputs plus those relating to the terminal functionality.
We reduce the alphabet further by only selecting inputs which follow the binary packet protocol, hence we don't include the identification input which should
be sent by both client and server at the start of every connection. The exchange of this inputs is made implicit. Finally, from the inputs defined, we make a selection
of essential inputs. These comprise the restricted alphabet, which we will use in some experiments.
be sent by both client and server at the start of every connection. The exchange of these inputs is made implicit. Finally, from the inputs defined, we make a selection
of essential inputs. These comprise the restricted alphabet, which we will use in some experiments. Essential inputs are marked with '*'.
Applying this ``outgoing only'' principle to the transport layer results in the messages of Table~\ref{trans-alphabet}. This is a special instance of \textsc{kexinit} for which \texttt{first\_kex\_packet\_follows} is enabled~\cite[p. 17]{rfc4253}. Our mapper can only handle correct key guesses, so the wrong-guess procedure as described in ~\cite[p. 19]{rfc4253} was not supported. When needed, SUTs were configured to make this guess work by altering their cipher preferences. The SSH version and comment string (described in Section~\ref{ssh-run-trans}) was not queried because it does not follow the binary packet protocol.
Table~\ref{trans-alphabet} introduces the Transport layer inputs. We include two versions of the \textsc{kexinit} message, one where \texttt{first\_kex\_packet\_follows} is disabled, the other when it is enabled, in which case, the message would make a guess on the security parameters~\cite[p. 17]{rfc4253}. Our mapper can only handle correct key guesses, so the wrong-guess procedure as described in ~\cite[p. 19]{rfc4253} was not supported.
%When needed, SUTs were configured to make this guess work by altering their cipher preferences. The SSH version and comment string (described in Section~\ref{ssh-run-trans}) was not queried because it does not follow the binary packet protocol.
\begin{table}[!ht]
\centering
......@@ -45,20 +47,18 @@ Applying this ``outgoing only'' principle to the transport layer results in the
\textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\
\textsc{unimpl} & Intended response to an unimplemented message~\cite[p. 25]{rfc4253} \\
\textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\
\textsc{kexinit} & Sends parameter preferences~\cite[p. 17]{rfc4253} \\
\textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\
\textsc{guessinit} & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\
\textsc{kex30} & Initializes the Diffie-Hellman key exchange~\cite[p. 21]{rfc4253} \\
\textsc{newkeys} & Requests to take new keys into use~\cite[p. 21]{rfc4253} \\
\textsc{sr\_auth} & Requests the authentication protocol~\cite[p. 23]{rfc4253} \\
\textsc{sr\_conn} & Requests the connection protocol~\cite[p. 23]{rfc4253}
\textsc{kex30}* & Initializes the Diffie-Hellman key exchange~\cite[p. 21]{rfc4253} \\
\textsc{newkeys}* & Requests to take new keys into use~\cite[p. 21]{rfc4253} \\
\textsc{sr\_auth}* & Requests the authentication protocol~\cite[p. 23]{rfc4253} \\
\textsc{sr\_conn}* & Requests the connection protocol~\cite[p. 23]{rfc4253}
\end{tabular}
\caption{Transport Layer inputs}
\label{trans-alphabet}
\end{table}
For the user authentication layer, applying our ``outgoing only'' principle results in just one message: the authentication request~\cite[p. 4]{rfc4252}. Its parameters contain all information needed for authentication. Four authentication methods exist: none, password, public key and host-based. Our mapper supports all methods except the host-based authentication because various SUTs lack support for this feature. For all other types, we define message
As shown in Table~\ref{auth-alphabet}, both the public key as well as the password method have a \textsc{ok} and \textsc{nok} variant which provides respectively correct and incorrect credentials.
The Authentication Layer defines one single client message type in the form of the authentication request~\cite[p. 4]{rfc4252}. Its parameters contain all information needed for authentication. Four authentication methods exist: none, password, public key and host-based. Our mapper supports all methods except the host-based authentication because various SUTs lack support for this feature. Both the public key and password methods have an \textsc{ok} and a \textsc{nok} variant which provides respectively correct and incorrect credentials.
\begin{table}[!ht]
\centering
......@@ -75,7 +75,9 @@ As shown in Table~\ref{auth-alphabet}, both the public key as well as the passwo
\label{auth-alphabet}
\end{table}
The connection protocol allows the client to request different processes over a single channel. Our mapper only implements requesting terminal emulation because availability of other processes depends heavily on a SUTs configuration. Moreover, little security-relevant information is expected to be gained by thoroughly testing other process requests. Combining this premise with the aforementioned ``outgoing only'' principle resulted in the alphabet of Table~\ref{conn-alphabet}.
The Connection Layer allows the client manage channels and to request services over a single channel. In accordance with our learning goal,
our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}.
\begin{table}[!ht]
\centering
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment