Commit 75be428d authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated. Removed some vspaces

parent 7823ec22
......@@ -56,6 +56,7 @@ give a glimpse into the issue of scalability. Assuming each input took 0.5 secon
\begin{table}[h] % was !ht
\centering
\small
\caption{Statistics for learning experiments}
\begin{tabular}{|l|l|l|l|l|l|l|}
\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
......@@ -63,7 +64,6 @@ OpenSSH 6.9p1-2 & 31 & 4 & 19836
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}
\label{tab:experiments}
%\vspace{-25mm}
\end{table}
......
......@@ -82,6 +82,9 @@ convey its own parameter preferences before key exchange can proceed. Also inclu
\begin{table}[!ht]
\centering
\small
\caption{Transport layer inputs}
\vspace{-2mm}
%\vspace{-7mm}
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{disconnect} & Terminates the current connection~\cite[p. 23]{rfc4253} \\
......@@ -95,14 +98,16 @@ convey its own parameter preferences before key exchange can proceed. Also inclu
\textsc{sr\_auth}* & Requests the authentication protocol~\cite[p. 23]{rfc4253} \\
\textsc{sr\_conn}* & Requests the connection protocol~\cite[p. 23]{rfc4253}
\end{tabular}
\caption{Transport layer inputs}
\vspace{-7mm}
\label{trans-alphabet}
\vspace{-1mm}
\end{table}
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.
\begin{table}[!ht]
\caption{Authentication layer inputs}
\vspace{-2mm}
%\vspace{-7mm}
\centering
\small
\begin{tabular}{ll}
......@@ -113,9 +118,8 @@ The Authentication layer defines a single client message type for the authentica
\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} \\
\end{tabular}
\caption{Authentication layer inputs}
\vspace{-7mm}
\label{auth-alphabet}
\vspace{-1mm}
\end{table}
The Connection layer allows clients to manage channels and request services over them. In accordance with our learning goal,
......@@ -126,6 +130,8 @@ The restricted alphabet only supports the most general channel management inputs
\begin{table}[!ht]
\centering
\small
\caption{Connection layer inputs}
\vspace{-2mm}
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{ch\_open}* & Opens a new channel~\cite[p. 5]{rfc4254} \\
......@@ -136,9 +142,9 @@ The restricted alphabet only supports the most general channel management inputs
\textsc{ch\_window\_adjust} & Adjusts the window size~\cite[p. 7]{rfc4254} \\
\textsc{ch\_request\_pty}* & Requests terminal emulation~\cite[p. 11]{rfc4254} \\
\end{tabular}
\caption{Connection layer inputs}
\vspace{-7mm}
%\vspace{-7mm}
\label{conn-alphabet}
\vspace{-1mm}
\end{table}
\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.
......
......@@ -38,9 +38,16 @@ tabsize=2
%\acmISBN{123-4567-24-567/08/06}
%Conference
\acmConference[SPIN'17]{SPIN Symposium}{July 2017}{California, USA}
%%% The following is specific to SPIN'17 and the paper
%%% 'Model Learning and Model Checking of SSH Implementations'
%%% by Paul Fiterau-Brostean, Frits Vaandrager, Erik Poll, Joeri de Ruiter, Toon Lenaerts, and Patrick Verleg.
\setcopyright{acmcopyright} % Adjust this to match your publishing-rights agreement with ACM.
\acmDOI{10.1145/3092282.3092289}
\acmISBN{978-1-4503-5077-8/17/07}
\acmConference[SPIN'17]{International SPIN Symposium on Model Checking of Software }{July 2017}{Santa Barbara, CA, USA}
\acmYear{2017}
\copyrightyear{2017}
\acmPrice{15.00}
\include{macros}
......
......@@ -335,6 +335,7 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of
\begin{table}[h!]
\centering
\small
\caption{Model checking results}
\begin{tabular}{| l | l | c | c |c | c |}
\hline
% & & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
......@@ -351,15 +352,14 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of
& Prop.~\ref{prop:auth-post-ua} & SHOULD & \dfce{sends unimpl}* & \dfce{sends unimpl}* & \dt \\ \cline{3-6}
& Prop.~\ref{prop:conn-close} & MUST & \dt & \dt & \dfce{sends CH\_EOF} \\ \hline
\end{tabular}
\caption{Model checking results}
\label{tab:mcresults}
\vspace{-5mm}
%\vspace{-5mm}
\end{table}
%\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
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
Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is acceptable is up for debate. Certainly the RFC does not suggest it, though it
does leave room for interpretation.
DropBear is the only implementation that allows rekeying in both general states of the protocol. DropBear also satisfies all Transport and Authentication layer specifications, however,
......
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