learning_setup.tex 20.1 KB
Newer Older
 Paul Fiterau Brostean committed May 17, 2017 1 Paul Fiterau Brostean committed Jan 29, 2017 2 \section{The learning setup} \label{sec:setup} Paul Fiterau Brostean committed Jan 20, 2017 3 4 5 6 7 8 %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} Paul Fiterau Brostean committed Feb 17, 2017 9 The learning setup consists of three components: the {\dlearner}, the {\dmapper} and the {\dsut}. 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 {\dlearner}. Paul Fiterau Brostean committed Jan 20, 2017 10 11 Erik Poll committed Feb 15, 2017 12 The {\dlearner} 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 an SSH server. The three components communicate over sockets, as shown in Figure~\ref{fig:components}. Paul Fiterau Brostean committed Jan 20, 2017 13 \begin{figure} Paul Fiterau Brostean committed Jan 25, 2017 14 \centering Paul Fiterau Brostean committed Feb 17, 2017 15 \includegraphics[scale=0.29]{components_cropped.pdf} Paul Fiterau Brostean committed Jan 29, 2017 16 \caption{The SSH learning setup.} Paul Fiterau Brostean committed Jan 20, 2017 17 18 19 \label{fig:components} \end{figure} Erik Poll committed Feb 15, 2017 20 21 22 23 SSH is a complex client-server protocol. In our work so far we concentrated on learning models of the implementation of the server, and not of the client. 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 left to default settings and are not purposefully explored. Also, the starting state of the {\dsut} is one where a TCP connection has already been established and where SSH versions have been exchanged, which are prerequisites for starting the Transport layer protocol. Paul Fiterau Brostean committed Jan 20, 2017 24 Paul Fiterau Brostean committed Feb 05, 2017 25 26 %figure %It is therefore important to focus on messages for which interesting state-changing behaviour can be expected. Erik Poll committed Feb 15, 2017 27 Paul Fiterau Brostean committed Feb 07, 2017 28 \subsection{The learning alphabet}\label{subsec:alphabet} Paul Fiterau Brostean committed Feb 05, 2017 29 Paul Fiterau Brostean committed May 16, 2017 30 Erik Poll committed Feb 15, 2017 31 32 The alphabet we use consists of inputs, which correspond to messages sent to the server, and outputs, which correspond to messages received Paul Fiterau Brostean committed May 16, 2017 33 from the server. We split \emph{the input alphabet} into three parts, one Paul Fiterau Brostean committed Feb 16, 2017 34 for each of the protocol layers. Paul Fiterau Brostean committed May 16, 2017 35 Paul Fiterau Brostean committed Feb 16, 2017 36 37 %\marginpar{\tiny Erik: the output alphabet is not discussed anywhere, %but for the discussion of the mapper in the next section it should be} Paul Fiterau Brostean committed May 16, 2017 38 Learning does not scale with a growing input alphabet, and since we are only Erik Poll committed Feb 15, 2017 39 40 41 42 43 learning models of servers, we remove those inputs that are not intended to ever be sent to the server\footnote{This means we exclude the messages \textsc{service\_accept}, \textsc{ua\_accept}, \textsc{ua\_failure}, \textsc{ua\_banner}, \textsc{ua\_pk\_ok}, \textsc{ua\_pw\_changereq}, \textsc{ch\_success} and Erik Poll committed Feb 17, 2017 44 \textsc{ch\_failure} from our alphabet.}. Furthermore, from the Erik Poll committed Feb 15, 2017 45 46 Connection layer we only use messages for channel management and the terminal functionality. Finally, because we will only explore Paul Fiterau Brostean committed Feb 17, 2017 47 protocol behavior after SSH versions have been exchanged, we exclude Erik Poll committed Feb 17, 2017 48 the messages for exchanging version numbers. Paul Fiterau Brostean committed May 16, 2017 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 %The alphabet comprises abstract messages corresponding to the concrete messages exchanged during client/server interactions, as per RFC. All included messages follow %the Byte Protocol format, and all are processable, that is, the SSH server should react to all of them. Hence, all messages could be %included as inputs in the alphabet. Doing so, however, would lead to prohibitively %long learning times. Consequently, we restrict the input alphabet to messages a server %is expected to receive from the client. \footnote{Which means we exclude %the messages \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} from our input alphabet.} % % %For the same reason, from the Connection layer we only use as inputs messages for channel management and the %terminal functionality. Finally, as we only explore protocol behavior after SSH versions have been exchanged, we exclude %the messages for exchanging version numbers. We don't place any restrictions on the %output of the server. All outputs the server generates are also included in the output alphabet. Paul Fiterau Brostean committed Jan 24, 2017 65 Erik Poll committed Feb 15, 2017 66 The resulting lists of inputs for the three protocol layers are given Paul Fiterau Brostean committed May 16, 2017 67 in Tables~\ref{trans-alphabet}-\ref{conn-alphabet}. In some Erik Poll committed Feb 15, 2017 68 69 70 71 72 73 experiments, we used only a subset of the most essential inputs, to further speed up experiments. This \textit{restricted alphabet} significantly decreases the number of queries needed for learning models while only marginally limiting explored behavior. We discuss this again in Section~\ref{sec:result}. Inputs included in the restricted alphabet are marked by '*' in the tables below. 74 Erik Poll committed Feb 17, 2017 75 Table~\ref{trans-alphabet} lists the Transport layer inputs. We include a version of the \textsc{kexinit} message with \texttt{first\_kex\_packet\_follows} disabled. Paul Fiterau Brostean committed Feb 12, 2017 76 This means no guess~\cite[p. 17]{rfc4253} is attempted on the {\dsut}'s parameter preferences. Consequently, the {\dsut} will have to send its own \textsc{kexinit} in order to Paul Fiterau Brostean committed Feb 14, 2017 77 convey its own parameter preferences before key exchange can proceed. Also included are inputs for establishing new keys (\textsc{kex30}, \textsc{newkeys}), disconnecting (\textsc{disconnect}), as well as the special inputs \textsc{ignore}, \textsc{unimpl} and \textsc{debug}. The latter are not interesting, as they are normally ignored by implementations. Hence they are excluded from our restricted alphabet. \textsc{disconnect} proved costly time wise, so was also excluded. Paul Fiterau Brostean committed Feb 12, 2017 78 79 %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} Paul Fiterau Brostean committed Feb 05, 2017 80 %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 81 82 83 \begin{table}[!ht] \centering Paul Fiterau Brostean committed Jan 25, 2017 84 \small Paul Fiterau Brostean committed Jan 20, 2017 85 86 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\ Paul Fiterau Brostean committed Feb 12, 2017 87 \textsc{disconnect} & Terminates the current connection~\cite[p. 23]{rfc4253} \\ Paul Fiterau Brostean committed Jan 20, 2017 88 \textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\ Paul Fiterau Brostean committed Feb 18, 2017 89 \textsc{unimpl} & Intended response to unrecognized messages~\cite[p. 25]{rfc4253} \\ Paul Fiterau Brostean committed Jan 20, 2017 90 \textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\ Paul Fiterau Brostean committed Feb 05, 2017 91 \textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\ Paul Fiterau Brostean committed Feb 12, 2017 92 %\textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\ Paul Fiterau Brostean committed Feb 05, 2017 93 94 95 96 \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 97 \end{tabular} 98 \caption{Transport layer inputs} Paul Fiterau Brostean committed Feb 17, 2017 99 \vspace{-7mm} Paul Fiterau Brostean committed Jan 20, 2017 100 101 102 \label{trans-alphabet} \end{table} Erik Poll committed May 19, 2017 103 The Authentication layer defines a single client message type for the authentication requests~\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 host-based authentication because some SUTs don't support this feature. Both the public key and password methods have \textsc{ok} and \textsc{nok} variants, which provide respectively correct and incorrect credentials. Our restricted alphabet supports only public key authentication, as the implementations processed this faster than the other authentication methods. Paul Fiterau Brostean committed Jan 20, 2017 104 105 106 \begin{table}[!ht] \centering Paul Fiterau Brostean committed Jan 25, 2017 107 \small Paul Fiterau Brostean committed Jan 20, 2017 108 109 110 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\ \textsc{ua\_none} & Authenticates with the none'' method~\cite[p. 7]{rfc4252} \\ Paul Fiterau Brostean committed Feb 18, 2017 111 112 113 114 \textsc{ua\_pk\_ok}* & Provides a valid name/key pair~\cite[p. 8]{rfc4252} \\ \textsc{ua\_pk\_nok}* & Provides an invalid name/key pair~\cite[p. 8]{rfc4252} \\ \textsc{ua\_pw\_ok} & Provides a valid name/password pair~\cite[p. 10]{rfc4252} \\ \textsc{ua\_pw\_nok} & Provides an invalid name/password pair~\cite[p. 10]{rfc4252} \\ Paul Fiterau Brostean committed Jan 20, 2017 115 \end{tabular} 116 \caption{Authentication layer inputs} Paul Fiterau Brostean committed Feb 17, 2017 117 \vspace{-7mm} Paul Fiterau Brostean committed Jan 20, 2017 118 119 120 \label{auth-alphabet} \end{table} Erik Poll committed May 19, 2017 121 The Connection layer allows clients to manage channels and request services over them. In accordance with our learning goal, Paul Fiterau Brostean committed Feb 05, 2017 122 our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}. Erik Poll committed May 19, 2017 123 The restricted alphabet only supports the most general channel management inputs, and excludes those not expected to produce state change. Paul Fiterau Brostean committed Feb 05, 2017 124 Paul Fiterau Brostean committed Jan 20, 2017 125 126 127 \begin{table}[!ht] \centering Paul Fiterau Brostean committed Jan 25, 2017 128 \small Paul Fiterau Brostean committed Jan 20, 2017 129 130 \begin{tabular}{ll} \textbf{Message} & \textbf{Description} \\ Paul Fiterau Brostean committed Feb 06, 2017 131 132 133 134 \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 135 136 \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 137 \textsc{ch\_request\_pty}* & Requests terminal emulation~\cite[p. 11]{rfc4254} \\ Paul Fiterau Brostean committed Jan 20, 2017 138 \end{tabular} 139 \caption{Connection layer inputs} Paul Fiterau Brostean committed Feb 17, 2017 140 \vspace{-7mm} Paul Fiterau Brostean committed Jan 20, 2017 141 142 \label{conn-alphabet} \end{table} Paul Fiterau Brostean committed May 16, 2017 143 Erik Poll committed May 19, 2017 144 \emph{The output alphabet} includes all messages an SSH server generates, which may include, with identical meaning, any of the messages defined as inputs. This also includes responses to various requests: \textsc{kex31}~\cite[p. 21]{rfc4253} as reply to \textsc{kex30}, \textsc{sr\_succes} in response to service requests (\textsc{sr\_auth} and \textsc{sr\_conn}), \textsc{ua\_success} and \textsc{ua\_failure}~\cite[p. 5,6]{rfc4252} in response to authentication requests, and \textsc{ch\_open\_success}~\cite[p. 6]{rfc4254} and \textsc{ch\_success}~\cite[p. 10]{rfc4254} , in positive response to \textsc{ch\_open} and \textsc{ch\_request\_pty} respectively. To these outputs, we add \textsc{no\_resp} for when the {\dsut} generates no output, and the special outputs \textsc{ch\_none}, \textsc{ch\_max} and \textsc{no\_conn}, and \textsc{buffered}, which we discuss in the next subsections. Paul Fiterau Brostean committed May 16, 2017 145 Paul Fiterau Brostean committed Jan 24, 2017 146 %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 147 %of all messages available at each layer. \textit{\textit{}} Paul Fiterau Brostean committed Jan 20, 2017 148 Paul Fiterau Brostean committed Jan 24, 2017 149 %table Paul Fiterau Brostean committed Jan 20, 2017 150 Paul Fiterau Brostean committed Feb 17, 2017 151 \subsection{The mapper}\label{subsec:mapper} Paul Fiterau Brostean committed Jan 29, 2017 152 Erik Poll committed Feb 15, 2017 153 154 The {\dmapper} must provide a translation between abstract messages and well-formed SSH messages: it has to translate abstract inputs Paul Fiterau Brostean committed Feb 18, 2017 155 listed in Tables~\ref{trans-alphabet}-\ref{conn-alphabet} to actual Erik Poll committed Feb 15, 2017 156 SSH packets, and translate the SSH packets received in answer Paul Fiterau Brostean committed May 17, 2017 157 158 159 to our abstract outputs. If no answer it received on an input, the {\dmapper} must return an output indicating timeout, which in our case is the \textsc{no\_resp} message. Erik Poll committed Feb 15, 2017 160 161 162 The sheer complexity of the {\dmapper} meant that it was easier to adapt an existing SSH implementation, rather than construct the Erik Poll committed May 19, 2017 163 164 165 {\dmapper} from scratch. After all, in many ways the {\dmapper} acts similar to an SSH client. Paramiko already provides mechanisms for Erik Poll committed Feb 15, 2017 166 167 168 169 170 171 172 173 encryption/decryption, as well as routines for constructing and 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 The {\dmapper} maintains a set of state variables to record parameters Paul Fiterau Brostean committed May 16, 2017 174 of the ongoing session, including the server's preferences Erik Poll committed Feb 15, 2017 175 for key exchange and encryption algorithm, parameters of these Paul Fiterau Brostean committed May 17, 2017 176 177 178 protocols, and, once it has been established, the session key. These parameters are updated when receiving messages from the server and used to concretize inputs to actual SSH messages to the server. Paul Fiterau Brostean committed Jan 29, 2017 179 Paul Fiterau Brostean committed May 16, 2017 180 For example, upon receiving a \textsc{kexinit} from the {\dsut}, the {\dmapper} saves Erik Poll committed Feb 15, 2017 181 182 the {\dsut}'s preferences for key exchange, hashing and encryption algorithms. Initially these parameters are all set to the defaults Paul Fiterau Brostean committed May 16, 2017 183 184 185 186 187 188 189 that any server should support, as required by the RFC. On receiving \textsc{kex31} in response to the \textsc{kex30} input, the {\dmapper} saves the hash, as well as the new keys. Finally, a \textsc{newkeys} response prompts the {\dmapper} to use the new keys negotiated earlier in place of the older ones, if such existed. The {\dmapper} also contains a buffer for storing opened channels, which is initially empty. Paul Fiterau Brostean committed Feb 16, 2017 190 On a \textsc{ch\_open} from the learner, the {\dmapper} adds a channel to the buffer Erik Poll committed May 19, 2017 191 with a randomly generated channel identifier; on a \textsc{ch\_close}, it removes the channel Paul Fiterau Brostean committed May 16, 2017 192 (if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. The {\dmapper} also stores the sequence number of the last received message from the {\dsut}. This number is then used when constructing \textsc{unimpl} inputs. Erik Poll committed Feb 15, 2017 193 194 In the following cases, inputs are answered by the {\dmapper} directly Paul Fiterau Brostean committed Feb 18, 2017 195 instead of being sent to the {\dsut} to find out its response: (1) on receiving a \textsc{ch\_open} input if the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max}; (2) Paul Fiterau Brostean committed Feb 17, 2017 196 197 198 199 200 201 202 203 204 205 206 207 on receiving any input operating on a channel (all Connection layer inputs other than \textsc{ch\_open}) when the buffer is empty, the {\dmapper} directly responds with \textsc{ch\_none}; (3) if connection with the {\dsut} was terminated, the {\dmapper} responds with a \textsc{no\_conn} message, as sending further messages to the {\dsut} is pointless in that case. %\begin{enumerate} %\item on receiving a \textsc{ch\_open} input and the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max}; %\item on receiving any input operating on a channel (all Connection layer inputs other than \textsc{ch\_open}) when the buffer is empty, the %{\dmapper} directly responds with \textsc{ch\_none}; %\item if connection with the {\dsut} was terminated, the {\dmapper} % responds with a \textsc{no\_conn} message, as sending further % messages to the {\dsut} is pointless in that case; %\end{enumerate} Erik Poll committed Feb 17, 2017 208 % Paul Fiterau Brostean committed Jan 20, 2017 209 210 Erik Poll committed Feb 16, 2017 211 \subsection{Practical complications} Erik Poll committed Feb 15, 2017 212 Erik Poll committed Feb 16, 2017 213 214 215 216 217 218 %There are three practical complications in learning models of SSH %servers: (1) an SSH server may exhibit \emph{non-determistic} %behaviour; (2) a single input to the server can produce a %\emph{sequence} of outputs ratheer than just a single output, and (3) %\emph{buffering} behaviour of the server. These complication are %discussed below. Paul Fiterau Brostean committed May 16, 2017 219 220 221 SSH implementations even behind the {\dmapper} abstraction may not behave like deterministic Mealy Machines, a prerequisite for the learning algorithm to succeed. Sources of non-determinism are: Erik Poll committed Feb 15, 2017 222 Paul Fiterau Brostean committed Jan 24, 2017 223 \begin{enumerate} Erik Poll committed Feb 15, 2017 224 \item Underspecification in the SSH specification (for example, by not Erik Poll committed Feb 16, 2017 225 specifying the order of certain messages) allows some Paul Fiterau Brostean committed Feb 17, 2017 226 non-deterministic behavior. Even if client Erik Poll committed Feb 15, 2017 227 and server do implement a fixed order for messages they sent, the Erik Poll committed Feb 16, 2017 228 229 asynchronous nature of communication means that the interleaving of sent and received messages may vary. Moreover, Erik Poll committed Feb 15, 2017 230 client and server are free to intersperse \textsc{debug} and Erik Poll committed Feb 16, 2017 231 232 \textsc{ignore} messages at any given time\footnote{The \textsc{ignore} messages are aimed to thwart traffic analysis.} Paul Fiterau Brostean committed Feb 16, 2017 233 \item Timing is another source of non-deterministic behavior. For Erik Poll committed Feb 15, 2017 234 example, the {\dmapper} might time-out before the {\dsut} had Paul Fiterau Brostean committed Feb 17, 2017 235 sent its response. Some {\dsuts} also behave Paul Fiterau Brostean committed May 17, 2017 236 unexpectedly when a new input is received too shortly after the Paul Fiterau Brostean committed Feb 17, 2017 237 238 239 240 241 242 243 244 245 previous one. Hence in our experiments we adjusted time-out periods accordingly so that neither of these events occur, and the {\dsut} behaves deterministically all the time. %did not occur. %However, other timing-related quirks can still %cause non-determinism. For example, some {\dsuts} behave %unexpectedly when a new query is received too shortly after the %previous one. Paul Fiterau Brostean committed Jan 24, 2017 246 247 %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} Erik Poll committed Feb 15, 2017 248 % Erik Poll committed Feb 16, 2017 249 To detect non-determinism, the {\dmapper} caches all observations Paul Fiterau Brostean committed May 17, 2017 250 251 252 in an SQLite database and verifies if new observations are consistent with previous ones. If not, it raises a warning, which then needs to be manually investigated. We analyzed each warning until we found a setting under which behavior was deterministic. Paul Fiterau Brostean committed May 16, 2017 253 254 255 256 The cache also acts as a cheap source of responses for already answered queries. Finally, by re-loading the cache from a previous experiment, we were able to start from where this experiment left off. This proved useful, as experiments could take several days. Erik Poll committed Feb 16, 2017 257 Paul Fiterau Brostean committed May 16, 2017 258 259 260 261 262 263 %An added benefit of the cache is that it allows the {\dmapper} to %supply answer to some inputs without actually sending them to the %{\dsut}. This sped up learning a lot when we had to restart %experiments: any new experiment on the same {\dsut} could start where %the previous experiment left off, without re-running all inputs. This %was an important benefit, as experiments could take several days. Paul Fiterau Brostean committed Feb 14, 2017 264 265 %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 266 Paul Fiterau Brostean committed Feb 18, 2017 267 Another practical problem besides non-determinism is that an SSH server Erik Poll committed Feb 16, 2017 268 269 may produce a sequence of outputs in response to a single input. This means it is not behaving as a Mealy machines, which allows for Paul Fiterau Brostean committed May 16, 2017 270 only one output. To deal with this, the {\dmapper} Erik Poll committed Feb 16, 2017 271 272 273 274 275 concatenates all outputs into one, and it produces this sequence as the single output to the {\dlearner}. A final challenge is presented by forms of buffering', which we encountered in two situations. Firstly, some implementations buffer Paul Fiterau Brostean committed May 16, 2017 276 incoming requests during rekey; only once rekeying is Erik Poll committed Feb 16, 2017 277 278 279 280 complete are all these messages processed. This leads to a \textsc{newkeys} response (indicating rekeying has completed), directly followed by all the responses to the buffered requests. This would lead to non-termination of the learning algorithm, as for every Erik Poll committed May 19, 2017 281 sequence of buffered messages the response differs. To Paul Fiterau Brostean committed May 16, 2017 282 prevent this, we treat the sequence of queued responses as the single Erik Poll committed Feb 16, 2017 283 284 output \textsc{buffered}. Paul Fiterau Brostean committed May 16, 2017 285 A different form of buffering occurs when opening and closing channels, since a Erik Poll committed Feb 16, 2017 286 {\dsut} can close only as many channels as have previously been opened. Paul Fiterau Brostean committed Feb 16, 2017 287 Learning this behavior would lead to an infinite state machine, as we Erik Poll committed Feb 16, 2017 288 289 would need a state there are $n$ channels open' for every number $n$. For this reason, we restrict the number of simultaneously open Erik Poll committed Feb 15, 2017 290 291 292 channels to one. The {\dmapper} returns a custom response \textsc{ch\_max} to a \textsc{ch\_open} message whenever this limit is reached.