learning_setup.tex 15.5 KB
 Paul Fiterau Brostean committed Jan 29, 2017 1 \section{The learning setup} \label{sec:setup}  Paul Fiterau Brostean committed Jan 20, 2017 2 3 4 5 6 7 8 9 10 11 12 %This chapter will cover the setup used to infer the state machines. We provide a general setup outline in Section~\ref{components}. The tested SSH servers are described in Section~\ref{suts}, which were queried with the alphabet described in Section~\ref{alphabet}. Section~\ref{setup-handling} will cover the challenging SUT behaviour faced when implementing the mapper, and the adaptations that were made to overcome these challenges. Section~\ref{layers-individual} will discuss the relation between state machines for individual layers and the state machine of the complete SSH protocol. The conventions on visualisation of the inferred state machines are described in Section~\ref{visualisation}. %Throughout this chapter, an individual SSH message to a SUT is denoted as a \textit{query}. A \textit{trace} is a sequence of multiple queries, starting from a SUT's initial state. Message names in this chapter are usually self-explanatory, but a mapping to the official RFC names is provided in Appendix~\ref{appendixa}. %\section{Components}\label{components} The learning setup consists of three components: a \emph{learner}, \emph{mapper} and the SUT. The {\dlearner} generates abstract inputs, representing SSH messages. The {\dmapper} transforms these messages into well-formed SSH packets and sends them to the {\dsut}. The {\dsut} sends response packets back to the {\dmapper}, which in turn, translates these packets to abstract outputs. The {\dmapper} then sends the abstract outputs back to the learner. The learner uses LearnLib ~\cite{LearnLib2009}, a Java library implementing $L^{\ast}$ based algorithms for learning Mealy machines. The {\dmapper} is based on Paramiko, an open source SSH implementation written in Python\footnote{Paramiko is available at \url{http://www.paramiko.org/}}. We opted for Paramiko because its code is relatively well structured and documented. The {\dsut} can be any existing implementation of a SSH server. The {\dlearner} communicates with the {\dmapper} over sockets. A graphical representation of our setup is shown in Figure~\ref{fig:components}. \begin{figure}  Paul Fiterau Brostean committed Jan 25, 2017 13  \centering  14  \includegraphics[scale=0.29]{components.pdf}  Paul Fiterau Brostean committed Jan 29, 2017 15  \caption{The SSH learning setup.}  Paul Fiterau Brostean committed Jan 20, 2017 16 17 18  \label{fig:components} \end{figure}  Paul Fiterau Brostean committed Feb 05, 2017 19 20 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  Paul Fiterau Brostean committed Feb 05, 2017 21 from a security perspective. Algorithms for encryption, compression and hashing are set to default settings and are not purposefully explored. Also, the starting  22 state of the {\dsut} is one where a TCP connection has already been established and where SSH versions have been exchanged, a required first step of the Transport layer protocol.  Paul Fiterau Brostean committed Jan 20, 2017 23   Paul Fiterau Brostean committed Feb 05, 2017 24 25 %figure %It is therefore important to focus on messages for which interesting state-changing behaviour can be expected.  Paul Fiterau Brostean committed Feb 07, 2017 26 \subsection{The learning alphabet}\label{subsec:alphabet}  Paul Fiterau Brostean committed Feb 05, 2017 27 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.  Paul Fiterau Brostean committed Feb 05, 2017 28 29 30 31 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  32 33 34 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 for channel management plus those relating to the terminal functionality. As mentioned previously, the starting state is already one where SSH versions have been exchanged, thus we also exclude these messages from our alphabet as they are no longer useful in exploring SSH's behavior once the initial exchange took place. From the inputs defined, we make a selection of essential inputs. The selection forms the \textit{restricted alphabet}, which we use in some experiments. The restricted alphabet significantly decreases the number of queries needed to learn while only marginally limiting explored behavior. We touch on this again in the Section~\ref{sec:result}. Inputs included in the restricted alphabet are marked by '*'.  Paul Fiterau Brostean committed Jan 20, 2017 35   36 37 38 39  %messages which don't adhere %to the binary packet p %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 these inputs is made implicit.  Paul Fiterau Brostean committed Jan 24, 2017 40   41 42  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. \textsc{ignore}, \textsc{unimpl} and \textsc{debug} are not expected to alter behavior so excluded from our restricted alphabet. \textsc{discon} proved costly time wise, so was also excluded.  Paul Fiterau Brostean committed Feb 05, 2017 43 %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.  Paul Fiterau Brostean committed Jan 20, 2017 44 45 46  \begin{table}[!ht] \centering  Paul Fiterau Brostean committed Jan 25, 2017 47 \small  Paul Fiterau Brostean committed Jan 20, 2017 48 49 50 51 52 53 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\ \textsc{discon} & Terminates the current connection~\cite[p. 23]{rfc4253} \\ \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} \\  Paul Fiterau Brostean committed Feb 05, 2017 54 \textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\  55 \textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\  Paul Fiterau Brostean committed Feb 05, 2017 56 57 58 59 \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}  Paul Fiterau Brostean committed Jan 20, 2017 60 \end{tabular}  61 \caption{Transport layer inputs}  Paul Fiterau Brostean committed Jan 20, 2017 62 63 64 \label{trans-alphabet} \end{table}  65 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. Our restricted alphabet supports only public key authentication, as it was processed the fastest by implementations out of all authentication forms.  Paul Fiterau Brostean committed Jan 20, 2017 66 67 68  \begin{table}[!ht] \centering  Paul Fiterau Brostean committed Jan 25, 2017 69 \small  Paul Fiterau Brostean committed Jan 20, 2017 70 71 72 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\ \textsc{ua\_none} & Authenticates with the none'' method~\cite[p. 7]{rfc4252} \\  Paul Fiterau Brostean committed Feb 06, 2017 73 74 \textsc{ua\_pk\_ok}* & Provides a valid name/key combination~\cite[p. 8]{rfc4252} \\ \textsc{ua\_pk\_nok}* & Provides an invalid name/key combination~\cite[p. 8]{rfc4252} \\  Paul Fiterau Brostean committed Jan 20, 2017 75 76 77 \textsc{ua\_pw\_ok} & Provides a valid name/password combination~\cite[p. 10]{rfc4252} \\ \textsc{ua\_pw\_nok} & Provides an invalid name/password combination~\cite[p. 10]{rfc4252} \\ \end{tabular}  78 \caption{Authentication layer inputs}  Paul Fiterau Brostean committed Jan 20, 2017 79 80 81 \label{auth-alphabet} \end{table}  82 The Connection layer allows the client manage channels and to request/run services over them. In accordance with our learning goal,  Paul Fiterau Brostean committed Feb 05, 2017 83 our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}.  84 The restricted alphabet only supports the most general channel management inputs. Those excluded are not expected to produce state change.  Paul Fiterau Brostean committed Feb 05, 2017 85   Paul Fiterau Brostean committed Jan 20, 2017 86 87 88  \begin{table}[!ht] \centering  Paul Fiterau Brostean committed Jan 25, 2017 89 \small  Paul Fiterau Brostean committed Jan 20, 2017 90 91 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\  Paul Fiterau Brostean committed Feb 06, 2017 92 93 94 95 \textsc{ch\_open}* & Opens a new channel~\cite[p. 5]{rfc4254} \\ \textsc{ch\_close}* & Closes a channel~\cite[p. 9]{rfc4254} \\ \textsc{ch\_eof}* & Indicates that no more data will be sent~\cite[p. 9]{rfc4254} \\ \textsc{ch\_data}* & Sends data over the channel~\cite[p. 7]{rfc4254} \\  Paul Fiterau Brostean committed Jan 20, 2017 96 97 \textsc{ch\_edata} & Sends typed data over the channel~\cite[p. 8]{rfc4254} \\ \textsc{ch\_window\_adjust} & Adjusts the window size~\cite[p. 7]{rfc4254} \\  Paul Fiterau Brostean committed Feb 06, 2017 98 \textsc{ch\_request\_pty}* & Requests terminal emulation~\cite[p. 11]{rfc4254} \\  Paul Fiterau Brostean committed Jan 20, 2017 99 \end{tabular}  100 \caption{Connection layer inputs}  Paul Fiterau Brostean committed Jan 20, 2017 101 102 \label{conn-alphabet} \end{table}  Paul Fiterau Brostean committed Jan 24, 2017 103 %The learning alphabet comprises of input/output messages by which the {\dlearner} interfaces with the {\dmapper}. Section~\ref{sec:ssh} outlines essential inputs, while Table X provides a summary  Paul Fiterau Brostean committed Jan 29, 2017 104 %of all messages available at each layer. \textit{\textit{}}  Paul Fiterau Brostean committed Jan 20, 2017 105   Paul Fiterau Brostean committed Jan 24, 2017 106 %table  Paul Fiterau Brostean committed Jan 20, 2017 107   Paul Fiterau Brostean committed Jan 24, 2017 108 \subsection{The mapper}  Paul Fiterau Brostean committed Feb 05, 2017 109 The {\dmapper} must provide translation between abstract message representations and well-formed SSH messages. A special case is for when no output is received from the {\dsut}, in which case the {\dmapper} gives back to the learner a {\dtimeout} message, concluding a timeout occurred. The sheer complexity of the {\dmapper}, meant that it was easier to adapt an existing SSH implementation, rather than construct the {\dmapper} from scratch. Paramiko already provides mechanisms for encryption/decryption, as well as routines for sending the different types of packets, and for receiving them. These routines are called by control logic dictated by Paramiko's own state machine. The {\dmapper} was constructed by replacing this control logic with one dictated by messages received from the {\dlearner}. %over a socket connection  Paul Fiterau Brostean committed Jan 29, 2017 110   Paul Fiterau Brostean committed Feb 05, 2017 111 The {\dmapper} maintains a set of state variables which have initial values, and which are updated on specific outputs and used in concretize certain inputs. On receiving a \textsc{kexinit}, the {\dmapper} saves the {\dsut}'s parameter preferences. These preferences define the key exchange, hashing and encryption algorithms supported by the {\dsut}. Before such receipt, these parameters are defaulted to those that any implementation should support, as required by the RFC. Based on these parameters, a key exchange algorithm may be run. The {\dmapper} supports Diffie-Hellman, which it can initiate via a \textsc{kex30} input from the learner. The {\dsut} responds with \textsc{kex31} if the inputs were orderly sent. From \textsc{kex31}, the {\dmapper} saves the hash, as well as the new keys. Receipt of the \textsc{newkeys} response from the {\dsut} will make the {\dmapper} use the new keys earlier negotiated in place of the older ones. The {\dmapper} contains two other state variables, used for storing the channel and sequence numbers respectively. The former is retrieved from a \textsc{ch\_accept} response and re-used in the other channel-type inputs, the latter each retrieved from each packet received and used in \textsc{unimpl} inputs. Both variables are initially set to 0.  Paul Fiterau Brostean committed Jan 29, 2017 112   Paul Fiterau Brostean committed Feb 07, 2017 113 In certain scenarios, inputs are answered by the {\dmapper} directly instead of being sent to the {\dsut}. These scenarios include the following:  Paul Fiterau Brostean committed Feb 05, 2017 114 \begin{enumerate}  Paul Fiterau Brostean committed Feb 07, 2017 115 \item if connection with the {\dsut} was terminated, the {\dmapper} responds with a \textsc{no\_conn} message  Paul Fiterau Brostean committed Feb 05, 2017 116 \item no channel has been opened or the maximum number of channels was reached (in our experiments 1), cases which prompt the {\dmapper}  Paul Fiterau Brostean committed Feb 07, 2017 117 to respond with \textsc{ch\_none}, or \textsc{ch\_max} respectively  Paul Fiterau Brostean committed Feb 05, 2017 118 \end{enumerate}  Paul Fiterau Brostean committed Jan 29, 2017 119   Paul Fiterau Brostean committed Feb 05, 2017 120 121 Overall, we notice that in many ways, the {\dmapper} acts similarly to an SSH client. Hence it is unsurprising that it was built off an existing implementation.  Paul Fiterau Brostean committed Jan 20, 2017 122 123 124   Paul Fiterau Brostean committed Jan 24, 2017 125 126 127 128 129 130 131 132 133 134 \subsection{Compacting SSH into a small Mealy machine} The {\dmapper} not only provides abstraction, it also ensures that the abstract representation shown to the learner behaves like a deterministic Mealy Machine. This is needed, as SSH implementations are inherently \textit{non-determistic}. Sources of non-determinism can be divided into three categories: \begin{enumerate} \item SSH's \textit{protocol design} is inherently non-deterministic. Firstly, because underspecification leads to multiple options for developers, from which one can be selected in a non-deterministic manner. Secondly, because non-deterministic behaviour directly results from the specifications. An example of the latter is allowing to insert \textsc{debug} and \textsc{ignore} messages at any given time. \item \textit{Response timing} is a source of non-determinism as well. For example, the {\dmapper} might conclude a timeout before the {\dsut} had sent its response. We had to set timeout values accordingly, so that enough time was allowed for the response to be received. \item Other \textit{timing-related quirks} can cause non-deterministic behaviour as well. Some {\dsuts} behave unexpectedly when a new query is received shortly after the previous one. %For example, a trace in which a valid user authentication is performed within five milliseconds after an authentication request on DropBear can cause the authentication to (wrongly) fail. \end{enumerate}  Paul Fiterau Brostean committed Jan 20, 2017 135   Paul Fiterau Brostean committed Jan 29, 2017 136 To detect non-determinism, we cache all new observations in an SqlLite database and verify observations against this cache. The cache also enables us to answer to queries answered before  Paul Fiterau Brostean committed Jan 24, 2017 137 without running inputs on the {\dsut}. A subsequent identical learning run can quickly resume from where the previous one was ended, as the cache from the previous run is used to quickly respond to all queries up to the point the previous run ended.  Paul Fiterau Brostean committed Jan 20, 2017 138   Paul Fiterau Brostean committed Jan 24, 2017 139 140 Aside from non-determinism, SSH implementations can also produce a sequence of outputs in response to an input, whereas Mealy machines allow for only one output. To that end, the {\dmapper} concatenates all outputs into one, delivering a single output to the {\dlearner}.  Paul Fiterau Brostean committed Jan 20, 2017 141   Paul Fiterau Brostean committed Jan 24, 2017 142 Another challenge is presented by buffering, leading to an explosion of states, as buffers cannot be described succintly by Mealy Machines.  Paul Fiterau Brostean committed Jan 29, 2017 143 We have encountered buffers in two occasions. Firstly, some implementations buffer certain responses when in re-key exchange. As soon as re-keying completes, these queued messages are released all at once. This leads to a \textsc{newkeys} response (indicating re-keying has completed), directly followed by all buffered responses. This, combined with concatenation of the multiple output responses would lead to non-termination of the learning algorithm, as for every variant of the response queue there would be a different output. To counter this, we replace the concatenation of queued output responses by the single string \textsc{buffered}, thus forming \textsc{newkeys\_buffered}.  Paul Fiterau Brostean committed Jan 25, 2017 144 145  Buffer behaviour can also be observed when opening and closing channels, since a SUT can close only as many channels as have previously been opened. For this reason, we restricted the number of simultaneously open channels to one. The {\dmapper} returns a custom response \textsc{ch\_max} to a \textsc{ch\_open} message whenever this limit is reached.