Commit 9e5cf47d authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Some more shrinking

parent fcbbed49
......@@ -19,8 +19,7 @@ We have adapted the setting off 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}). The primary reason for using a restricted alphabet was to reduce learning times.
Most inputs excluded were inputs that either didn't change behavior (like \textsc{debug} or \textsc{unimpl}), or that proved costly time-wise,
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,
and were not critical to penetrating all layers. A concrete example is the user/password based authentication inputs (\textsc{ua\_pw\_ok} and
\textsc{ua\_pw\_nok}). It would take the system 2-3 seconds to respond to an invalid password, a typical countermeasure to slow down
brute force attacks. By contrast, public key authentication resulted in quick responses. The \textsc{disconnect} input presented similar
......@@ -48,7 +47,7 @@ Table~\ref{tab:experiments} describes the exact versions of the systems analyzed
%Dropbear: MemQ: 3561 TestQ: 30629
%OpenSSH: MemQ: 19836 TestQ: 76418
\begin{table}[t] % was !ht
\begin{table}[h] % was !ht
\centering
\small
\begin{tabular}{|l|l|l|l|l|l|l|}
......@@ -60,7 +59,7 @@ DropBear v2014.65 & 17 & 2 & 19863
\end{tabular}
\caption{Statistics for learning experiments}
\label{tab:experiments}
\vspace{-10mm}
%\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
......
......@@ -182,15 +182,20 @@ Lastly, the {\dmapper} also stores the sequence number of the last received mes
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:
\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}
instead of being sent to the {\dsut} to find out its response: (1) on receiving a \textsc{ch\_open} input
and the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max}; (2)
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}
%
In many ways, the {\dmapper} acts similar to an SSH client, hence the
decision to built it by adapting an existing client implementation.
......@@ -258,7 +263,7 @@ 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 a key re-exchange; only once the rekeying is
incoming requests during rekey; only once the 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
......
......@@ -46,7 +46,7 @@ the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~
Here learning is viewed as a game in which a \emph{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}).
Initially, the learner only knows the input alphabet $I$ and output alphabet $O$ of $\M$.
The task of the learner is to learn $\M$ through two types of queries:
The task of the learner is to learn $\M$ via two types of queries:
\begin{itemize}
\item
With a \emph{membership query}, the learner asks what the response is to an input sequence $\sigma \in I^{\ast}$.
......
......@@ -281,8 +281,7 @@ G ( (hasReqAuth & !O out=UA_SUCCESS) ->
\begin{property}
\vspace{-4mm}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (out=UA_SUCCESS) ->
X G (out!=UA_SUCCESS) )
G ( out=UA_SUCCESS -> X G out!=UA_SUCCESS)
\end{lstlisting}
%\caption{UA\_SUCCESS is sent at most once}
\label{prop:auth-post-ua-strong}
......@@ -292,8 +291,7 @@ In the same paragraph, it is stated that authentication requests received after
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=UA_SUCCESS ->
X ( ( authReq-> out=NO_RESP )
W endCondition ) )
X ( ( authReq-> out=NO_RESP ) W endCondition ) )
\end{lstlisting}
%\caption{Silence after UA\_SUCCESS}
\label{prop:auth-post-ua}
......@@ -351,7 +349,7 @@ In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest success
\end{tabular}
\caption{Model checking results}
\label{tab:mcresults}
\vspace{-10mm}
\vspace{-5mm}
\end{table}
%\end{center}
......
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