learning_results.tex 10 KB
Newer Older
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
1
2
3
\section{Learning results} \label{sec:result}
\newcommand{\dk}{\emph{k}}
We use the setup described in Section~\ref{sec:setup} to learn models for OpenSSH, BitVise and DropBear SSH server implementations. 
4
OpenSSH represents the focal point, as it is the most popular implementation of SSH (with over 80 percent of market share in 2008~\cite{Albrecht2009Plaintext}) 
Erik Poll's avatar
Erik Poll committed
5
6
and the default server for many UNIX-based systems. DropBear is an alternative to OpenSSH designed for low resource
systems. BitVise is a well-known proprietary Windows-only SSH implementation. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
7

Erik Poll's avatar
Erik Poll committed
8
In our experimental setup, {\dlearner} and {\dmapper} ran inside a Linux Virtual Machine. OpenSSH and DropBear were 
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
9
learned over a localhost connection, whereas BitVise was learned over a virtual connection with the Windows host machine. 
10
We have adapted the setting of timing parameters to each implementation.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
11

12
13
\begin{figure*}
\centering
14
  \includegraphics[scale=0.297]{ssh-server_cropped}
Erik Poll's avatar
.    
Erik Poll committed
15
  \caption{Model of the OpenSSH server. {\normalfont States are collected in 3 clusters,
Erik Poll's avatar
shit    
Erik Poll committed
16
17
  indicated by the rectangles, where each cluster corresponds to 
  one of the protocol layers. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
18
19
    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.}}
20
21
22
  \label{fig:sshserver}
\end{figure*}

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
23
OpenSSH was learned using a full alphabet, whereas DropBear and BitVise were learned using a restricted alphabet (as defined in Subsection~\ref{subsec:alphabet}). The primary reason for using a restricted alphabet was to speed up learning. Most inputs excluded were inputs that either didn't change behavior (like \textsc{debug} or \textsc{unimpl}), or that proved costly time-wise,
24
and were not critical to penetrating all layers. A concrete example is the user/password based authentication inputs (\textsc{ua\_pw\_ok} and 
Erik Poll's avatar
Erik Poll committed
25
\textsc{ua\_pw\_nok}). It would take the system 2-3 seconds to respond to an invalid password, a typical countermeasure to slow down 
26
brute force attacks. By contrast, public key authentication resulted in quick responses. The \textsc{disconnect} input presented similar
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
27
challenges, as it would take a varying amount of time until the system responded. This was particularly problematic for BitVise. 
28
29
30
31
32
33
34

%Not only that, but failed password authentication
%attempts are also likely to trigger security mechanisms that would block subsequent authentication attempts. While this is 

%As an example, \textsl{ua\_pw\_ok} contours the same behavior as \textsl{ua\_pk\_ok}. But while authenticating
%with a public key was done quickly, authenticating with a username/password proved time consuming (it would take the system 2-3 seconds to respond to 
%invalid credentials \textsl{ua\_pw\_ok}). The \textsl{disconnect} proved expensive in a similar way.
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
35

Erik Poll's avatar
Erik Poll committed
36
For the test queries we used random and exhaustive variants of the testing algorithm described in 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
37
\cite{SMJV15}, which generate efficient test suites. Tests generated comprise an access sequence, a middle section of length {\dk} and a 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
38
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,
39
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
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
40
41
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. 
Erik Poll's avatar
shit    
Erik Poll committed
42
We then ran an exhaustive test suite with {\dk} of 2 for all implementations. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
43

44

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
45
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing, namely:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
46
(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}. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
47
48
49
%BitVise: MemQ: 24996 TestQ: 58423
%Dropbear: MemQ: 3561 TestQ: 30629
%OpenSSH: MemQ: 19836 TestQ: 76418
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
50

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
51
\begin{table}[h] % was !ht
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
52
\centering
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
53
\small
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
54
55
\begin{tabular}{|l|l|l|l|l|l|l|}
\hline
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
56
57
58
{\centering{\textbf{SUT}}} & \textbf{States} & \textbf{Hypotheses }  & \textbf{Mem. Q.}      & \textbf{Test Q.}\\ \hline  %& \textbf{Tests to last Hyp.}			& \textbf{Tests on last Hyp.} \\ \hline
OpenSSH 6.9p1-2            & 31              & 4               			 & 19836                 & 76418                  \\ %& 1322      						& 50243         \\
BitVise 7.23               & 65              & 15              			 & 24996                 & 58423                  \\ %& 9549   							& 65040         \\
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
59
DropBear v2014.65          & 29              & 8               			 & 8357                  & 64478                  \\ \hline %& 15268  							& 56174        \\
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
60
61
62
\end{tabular}
\caption{Statistics for learning experiments}
\label{tab:experiments}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
63
%\vspace{-25mm}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
64
65
66
\end{table}

The large number of states is down to several reasons. First of all, some systems exhibited buffering behavior. In particular, BitVise would queue
Erik Poll's avatar
Erik Poll committed
67
responses for higher layer inputs sent during key re-exchange, and would deliver them all at once after rekeying was done. Rekeying was also
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
68
69
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. 
70

71
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
Erik Poll's avatar
Erik Poll committed
72
rekeying (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect. 
73

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
74
75
%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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
76

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
77
78
%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.
79
80
81



82
83


Paul Fiterau Brostean's avatar
Files    
Paul Fiterau Brostean committed
84
85
86
87
%To give a concrete example, the {\dmapper} on every \textsl{ch\_open} saves a channel identifier and sends
%a corresponding message to the {\dsut}. If \textsl{ch\_open} is called again, the {\dmapper} responds with a \textsl{ch\_max}. The channel identifier is removed 
%by a \textsl{ch\_close} input leading to pairs of  identical states with and without the channel identifier, even in states where channels are not relevant (like for example states prior to authentication). 

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
88