Commit 7823ec22 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Consistent Bitvise naming

parent 9de31186
\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.
We use the setup described in Section~\ref{sec:setup} to learn models for OpenSSH, Bitvise and DropBear SSH server implementations.
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})
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.
systems. Bitvise is a well-known proprietary Windows-only SSH implementation.
In our experimental setup, {\dlearner} and {\dmapper} ran inside a Linux Virtual Machine. OpenSSH and DropBear were
learned over a localhost connection, whereas BitVise was learned over a virtual connection with the Windows host machine.
learned over a localhost connection, whereas Bitvise was learned over a virtual connection with the Windows host machine.
We have adapted the setting of timing parameters to each implementation.
\begin{figure*}
......@@ -20,7 +20,7 @@ We have adapted the setting of timing parameters to each implementation.
\label{fig:sshserver}
\end{figure*}
OpenSSH was learned using a full alphabet, whereas DropBear and BitVise were learned using a restricted alphabet (as defined in Subsection~\ref{subsec:alphabet}).
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 reason for using a restricted alphabet was to reduce learning times. Based on the model learned for OpenSSH (the first implementation analyzed) and the specification, we excluded
inputs that seemed unlikely to produce state change (such as
\textsc{debug} or \textsc{unimpl}). We also excluded inputs that proved costly time-wise (such as \textsc{disconnect}) but were not were not needed to visit all states in the happy flow. We excluded, for example, the user/password based authentication inputs (\textsc{ua\_pw\_ok} and
......@@ -41,7 +41,7 @@ For the test queries we used random and exhaustive variants of the testing algor
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. We then ran an exhaustive test suite with {\dk} of 2 for all implementations.
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. We then ran an exhaustive test suite with {\dk} of 2 for all implementations.
%To that end, we built a java adapter that would automatically run the model checker on the hypothesis, and transform any counterexamples into tests. This proved essential in learning DropBear, as the last counterexample was generated by the model checker.
......@@ -49,7 +49,7 @@ can be set to higher values. We executed a random test suite with {\dk} of 4 com
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing:
(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 and the properties checked are at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}. The statistics
give a glimpse into the issue of scalability. Assuming each input took 0.5 seconds to process, and an average query length of 10, to perform 40000 queries would have taken roughly 55 hours. This is consistent with the time experiments took, which span several days. The long duration compelled us to resort to restricted alphabets, which lead to reduction in the number of queries needed. Our work could have benefited from parallel execution.
%BitVise: MemQ: 24996 TestQ: 58423
%Bitvise: MemQ: 24996 TestQ: 58423
%Dropbear: MemQ: 3561 TestQ: 30629
%OpenSSH: MemQ: 19836 TestQ: 76418
......@@ -60,7 +60,7 @@ give a glimpse into the issue of scalability. Assuming each input took 0.5 secon
\hline
{\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 \\
Bitvise 7.23 & 65 & 15 & 24996 & 58423 \\ %& 9549 & 65040 \\
DropBear v2014.65 & 29 & 8 & 8357 & 64478 \\ \hline %& 15268 & 56174 \\
\end{tabular}
\caption{Statistics for learning experiments}
......@@ -68,7 +68,7 @@ DropBear v2014.65 & 29 & 8 & 8357
%\vspace{-25mm}
\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
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 the {\dmapper} generated outputs \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.
......@@ -77,10 +77,10 @@ Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with some edits
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.
%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.
%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.
%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.
......
......@@ -326,7 +326,7 @@ G ( hasOpenedChannel ->
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for BitVise
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for Bitvise
as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}).
In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of successful authentication.
......@@ -358,7 +358,7 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of
%\end{center}
Properties marked with '*' did not hold because implementations chose to send \textsc{unimpl}, instead of the output suggested by the RFC. As an example,
after successful authentication, both BitVise and OpenSSH respond with \textsc{unimpl} to further authentication requests, instead of being silent, violating
after successful authentication, both Bitvise and OpenSSH respond with \textsc{unimpl} to further authentication requests, instead of being silent, violating
Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is acceptable is up for debate. Definitely the RFC does not suggest it, though the RFC
does leave room for interpretation.
......
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