Commit 477037ed authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Some updates

parent 36a8011c
......@@ -15,7 +15,8 @@ We have adapted the setting of timing parameters to each implementation.
\caption{Model of the OpenSSH server. {\normalfont States are collected in 3 clusters,
indicated by the rectangles, where each cluster corresponds to
one of the protocol layers.
We eliminate redundant states and information induced by the {\dmapper}, as well as states present in successful rekeying sequences. Wherever rekeying was permitted, we replaced the rekeying states and transitions by a single \textsl{REKEY SEQUENCE} transition. We also factor out edges common to states within a cluster. We replace common disconnecting edges, by one edge from the cluster to the disconnect state. Common self loop edges are colored, and the actual i/o information only appears on one edge. Transitions with similar start and end states are joined together on the same edge. Transition labels are kept short by regular expressions(UA\_* stands for all inputs starting with UA\_) or by factoring out common start strings. Green edges highlight the happy flow. }}
We eliminate redundant states and information induced by the {\dmapper}, as well as states present in successful rekeying sequences. Wherever rekeying was permitted, we replaced the rekeying states and transitions by a single \textsl{REKEY SEQUENCE} transition. We also factor out edges common to states within a cluster. We replace common disconnecting edges, by one edge from the cluster to the disconnect state. Common self loop edges are colored, and the actual i/o information only appears on one edge. Transitions with similar start and end states are joined together on the same edge. Transition labels are kept short by regular expressions(UA\_* stands for inputs starting with UA\_) or by factoring out common start strings. Green edges highlight the happy flow. '+' concatenates
multiple outputs.}}
\label{fig:sshserver}
\end{figure*}
......@@ -34,7 +35,7 @@ challenges, as it would take a varying amount of time until the system responded
For the test queries we used random and exhaustive variants of the testing algorithm described in
\cite{SMJV15}, which generate efficient test suites. Tests generated comprise an access sequence, a middle section of length {\dk} and a
distinguishing sequence. The exhaustive variant for a set {\dk} generates tests for all possible middle sections and all states. Passing all tests then provides some notion of confidence,
distinguishing sequence. The exhaustive variant generates tests for all possible middle sections of length {\dk} and all states. Passing all tests then provides some notion of confidence,
namely, that the learned model is correct unless the (unknown) model of the implementation has at least {\dk} more states than the learned hypothesis. The random variant produces tests
with randomly generated middle sections. No formal confidence is provided, but past experience shows this to be more effective at finding counterexamples since {\dk}
can be set to higher values. We executed a random test suite with {\dk} of 4 comprising 40000 tests for OpenSSH, and 20000 tests for BitVise and DropBear.
......@@ -42,7 +43,7 @@ We then ran an exhaustive test suite with {\dk} of 2 for all implementations.
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing, namely:
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models along with the specifications checked can be found at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}.
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models plus the specifications checked can be found at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}.
%BitVise: MemQ: 24996 TestQ: 58423
%Dropbear: MemQ: 3561 TestQ: 30629
%OpenSSH: MemQ: 19836 TestQ: 76418
......@@ -64,19 +65,17 @@ DropBear v2014.65 & 29 & 8 & 8357
The large number of states is down to several reasons. First of all, some systems exhibited buffering behavior. In particular, BitVise would queue
responses for higher layer inputs sent during key re-exchange, and would deliver them all at once after rekeying was done. Rekeying was also
a major contributor to the number of states. For each state where rekeying
is possible, the sequence of transitions constituting the complete
rekeying process should lead back to that state. This
leads to two additional rekeying states for every state allowing rekey. Many states were also added due to {\dmapper} generated outputs such as \textsc{ch\_none} or \textsc{ch\_max}, outputs which signal that no channel is open or that the maximum number of channels have been opened.
a major contributor to the number of states. For each state where rekeying is possible, the sequence of transitions constituting the complete
rekeying process should lead back to that state. This leads to two additional rekeying states for every state allowing rekey. Many states were also added due to {\dmapper} generated outputs such as \textsc{ch\_none} or \textsc{ch\_max}, outputs which signal that no channel is open or that the maximum number of channels have been opened.
Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with some edits to improve readability. The happy flow, in green, is fully explored in the model and mostly matches our earlier description of it\footnote{The only exception is in the Transport layer, where unlike in our happy flow definition, the server is the first to send the \textsc{newkeys} message. This is also accepted behavior, as the protocol does not specify which side should send \textsc{newkeys} first.}. Also explored is what happens when a rekeying sequence is attempted. We notice that rekeying is only allowed in states of the Connection layer. Strangely, for these states, rekeying is not state preserving, as the generated output on receiving a \textsc{sr\_auth}, \textsc{sr\_conn} or \textsc{kex30} changes from \textsc{unimpl} to \textsc{no\_resp}. This leads to two sub-clusters of states, one before the first rekey, the other afterward. In all other states, the first step of a
rekeying (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect.
We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of a prior service request. That in itself was not strange, as authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
Unexpected was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected when requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
%We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of a prior service request. That in itself was not strange, as authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
%Unexpected was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected when requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
We also notice the intricate authentication behavior:
after an unsuccessful authentication attempt the only authentication method still allowed is password authentication. Finally, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior.
%Systems reacted differently to \textsc{sr\_conn}, input which requests services of the Connection layer. These services are automatically requested after successful authentication, so technically, this input is not required to open channels for example. Nevertheless, in authenticated states, OpenSSH responded with \textsc{unimpl} and maintained state. BitVise disconnected the user. Only DropBear generated \textsc{sr\_accept}, the output we were expecting in view of the RFC.
We also note the intricate authentication behavior: after an unsuccessful authentication attempt the only authentication method still allowed is password authentication. Finally, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior.
......
......@@ -26,14 +26,15 @@ state of the {\dsut} is one where a TCP connection has already been established
\subsection{The learning alphabet}\label{subsec:alphabet}
The alphabet we use consists of inputs, which correspond to messages
sent to the server, and outputs, which correspond to messages received
from the server. We split the input alphabet into three parts, one
from the server. We split \emph{the input alphabet} into three parts, one
for each of the protocol layers.
%\marginpar{\tiny Erik: the output alphabet is not discussed anywhere,
%but for the discussion of the mapper in the next section it should be}
Learning does not scale with a growing alphabet, and since we are only
Learning does not scale with a growing input alphabet, and since we are only
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},
......@@ -44,11 +45,25 @@ Connection layer we only use messages for channel management and the
terminal functionality. Finally, because we will only explore
protocol behavior after SSH versions have been exchanged, we exclude
the messages for exchanging version numbers.
%\marginpar{\tiny Erik: I
%rephrased all this to make it simpler. Is it still ok?}
%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.
The resulting lists of inputs for the three protocol layers are given
in tables~\ref{trans-alphabet}-\ref{conn-alphabet}. In some
in Tables~\ref{trans-alphabet}-\ref{conn-alphabet}. In some
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
......@@ -124,12 +139,14 @@ The restricted alphabet only supports the most general channel management inputs
\vspace{-7mm}
\label{conn-alphabet}
\end{table}
\emph{The output alphabet} subsumes all messages an SSH server generates, which may include, with identical meaning, any of the messages defined as inputs. They also include responses to various requests: \textsc{kex31}~\cite[p. ]{} 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} in response to authentication requests, and \textsc{ch\_open\_success}, \textsc{ch\_success} and \textsc{ch\_close}, which confirm the requested channel operation. 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.
%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
%of all messages available at each layer. \textit{\textit{}}
%table
\subsection{The mapper}\label{subsec:mapper}
The {\dmapper} must provide a translation between abstract messages
......@@ -153,29 +170,25 @@ 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
of the ongoing session, including for example the server's preferences
of the ongoing session, including the server's preferences
for key exchange and encryption algorithm, parameters of these
protocols, and -- once it has been established -- the session key.
These parameters are updated when receiving messages from the server,
and are used to concretize inputs to actual SSH messages to the server.
For example, upon receiving a \textsc{kexinit}, the {\dmapper} saves
For example, upon receiving a \textsc{kexinit} from the {\dsut}, the {\dmapper} saves
the {\dsut}'s preferences for key exchange, hashing and encryption
algorithms. Initially these parameters are all set to the defaults
that any server should support, as required by the RFC. The
{\dmapper} supports Diffie-Hellman key exchange, which it will
initiate if it gets a \textsc{kex30} input from the learner.
After this, the {\dsut} responds with a \textsc{kex31} message
(assuming the protocol run so far is correct), and from this
message, 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, if such existed.
The {\dmapper} contains a buffer for storing channels opened, which is initially empty.
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.
On a \textsc{ch\_open} from the learner, the {\dmapper} adds a channel to the buffer
with a randomly generated channel identifier, on a \textsc{ch\_close}, it removes the channel
(if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. Lastly, 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.
(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.
In the following cases, inputs are answered by the {\dmapper} directly
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)
......@@ -204,11 +217,10 @@ decision to built it by adapting an existing client implementation.
%\emph{sequence} of outputs ratheer than just a single output, and (3)
%\emph{buffering} behaviour of the server. These complication are
%discussed below.
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:
SSH implementations can exhibit non-determistic behavior. The
learning algorithm cannot cope with non-determinism -- learning will
not terminate -- so this has to be detected, which our {\dmapper} does.
There are a few sources of non-determinism in SSH:
\begin{enumerate}
\item Underspecification in the SSH specification (for example, by not
specifying the order of certain messages) allows some
......@@ -236,38 +248,42 @@ There are a few sources of non-determinism in SSH:
\end{enumerate}
%
To detect non-determinism, the {\dmapper} caches all observations
in an SQLite database and verifies if a new observation is different
to one cached from a previous protocol run. If so, it raises
a warning, which then needs to be manually investigated.
in an SQLite database and verifies if a new observations are consistent
with previous ones. If not, it raises a warning, which then needs to be manually investigated. We acted on
each case until we found a setting under which behavior was deterministic.
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.
An added benefit of this 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 of, without re-running all inputs. This
was an important benefit, as experiments could take several days.
%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.
%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.
Another practical problem besides non-determinism is that an SSH server
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
only one output. Dealing with this is simple: the {\dmapper}
only one output. To deal with this, the {\dmapper}
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
incoming requests during rekey; only once the rekeying is
incoming requests during rekey; only once rekeying is
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
sequence of buffered messages the response is different. To
prevent this, we treat the sequence of queued responses as a single
prevent this, we treat the sequence of queued responses as the single
output \textsc{buffered}.
Secondly, buffering happens when opening and closing channels, since a
A different form of buffering occurs when opening and closing channels, since a
{\dsut} can close only as many channels as have previously been opened.
Learning this behavior would lead to an infinite state machine, as we
would need a state `there are $n$ channels open' for every number $n$.
......
......@@ -41,7 +41,7 @@ $\M$ and $\N$ if and only if $A_{\M}(\sigma) \neq A_{\N}(\sigma)$.
\subsection{MAT Framework} \label{ssec:mat}
The most efficient algorithms for model learning all follow
The most efficient algorithms for model learning (see~\cite{Isberner2015} for a recent overview) all follow
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Angluin1987Learning}.
Here learning is viewed as a game in which a \textit{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a Mealy machine $\M$,
also called the System Under Learning ({\dsut}).
......@@ -65,8 +65,7 @@ An equivalence query can be approximated using a conformance testing tool \cite{
A test query consists of asking the {\dsut} for the response to an input sequence
$\sigma \in I^{\ast}$, similar to a membership query.
Note that this cannot rule out that there is more behavior
that has not been discovered. For a recent overview of model learning
algorithms for this setting see \cite{Isberner2015}.
that has not been discovered.
\subsection{Abstraction} \label{ssec:mappers}
Most current learning algorithms are only applicable to Mealy machines with small alphabets comprising abstract messages. Practical systems typically
......
......@@ -18,8 +18,7 @@ SSHv2 follows a client-server paradigm. The protocol consists of three layers (F
\end{figure}
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers. This means that different layers can interact. Hence, it makes sense to analyze SSH as a whole, instead of analyzing its constituent layers independently. Below we discuss each layer, outlining the relevant messages which are later used in learning, and characterising the so-called \textit{happy flow} that a normal protocol
run follows.
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers, and different layers can interact. For this reason, we opt to analyze SSH as a whole, instead of analyzing its constituent layers independently. Below we discuss each layer, outlining the relevant messages which are later used in learning, and characterizing the so-called \textit{happy flow} that a normal protocol run follows.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the Transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys, which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to access services on the server, for example the terminal service.
......
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