Commit e3da9bb9 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Files

parent dd958809
...@@ -20,7 +20,7 @@ Limitations of the work, thus elements for future work, are several. First of al ...@@ -20,7 +20,7 @@ Limitations of the work, thus elements for future work, are several. First of al
produce a concretization of the abstract models. Consequently, model checking results cannot be fully transferred to the actual implementations. Moreover, produce a concretization of the abstract models. Consequently, model checking results cannot be fully transferred to the actual implementations. Moreover,
abstraction produced by the {\dmapper} could be made less coarse, so more insight into the implementation is gained. Parameters which are now abstracted, abstraction produced by the {\dmapper} could be made less coarse, so more insight into the implementation is gained. Parameters which are now abstracted,
such as the channel identifier or data sent over channels, could be extracted and potentially handled by Register Automata learners. Another thing which such as the channel identifier or data sent over channels, could be extracted and potentially handled by Register Automata learners. Another thing which
beg for improvement is the handling of buffering behavior. Buffering leads to many uninteresting states and greatly lengthens the learning process. begs for improvement is the handling of buffering behavior. Buffering leads to many uninteresting states and greatly lengthens the learning process.
Despite these limitations, our work provides a compelling application of learning and model checking in a security setting, on a widely used protocol. We hope this lays Despite these limitations, our work provides a compelling application of learning and model checking in a security setting, on a widely used protocol. We hope this lays
some more groundwork for further case studies, as well as fresh advancements in learning techniques. some more groundwork for further case studies, as well as fresh advancements in learning techniques.
\ No newline at end of file
...@@ -31,13 +31,12 @@ learning and test queries run. ...@@ -31,13 +31,12 @@ learning and test queries run.
\begin{table}[!ht] \begin{table}[!ht]
\centering \centering
\scriptsize
\begin{tabular}{|l|l|l|l|l|l|l|} \begin{tabular}{|l|l|l|l|l|l|l|}
\hline \hline
{\centering{\textbf{SUT}}} & \textbf{States} & \textbf{Hypotheses } & \textbf{Num. Queries} \\ \hline %& \textbf{Tests to last Hyp.} & \textbf{Tests on last Hyp.} \\ \hline {\centering{\textbf{SUT}}} & \textbf{States} & \textbf{Hypotheses } & \textbf{Num. Queries} \\ \hline %& \textbf{Tests to last Hyp.} & \textbf{Tests on last Hyp.} \\ \hline
OpenSSH 6.9p1-2 & 31 & 4 & tbc \\ %& 1322 & 50243 \\ OpenSSH 6.9p1-2 & 31 & 4 & tbc \\ %& 1322 & 50243 \\
BitVise 7.23 & 65 & 15 & tbc \\ %& 9549 & 65040 \\ BitVise 7.23 & 65 & 15 & tbc \\ %& 9549 & 65040 \\
DropBear v2014.65 & 17 & 2 & tbc \\ %& 15268 & 56174 \\ DropBear v2014.65 & 17 & 2 & tbc \\ \hline %& 15268 & 56174 \\
\end{tabular} \end{tabular}
\caption{Statistics for learning experiments} \caption{Statistics for learning experiments}
\label{tab:experiments} \label{tab:experiments}
...@@ -47,7 +46,9 @@ DropBear v2014.65 & 17 & 2 & tbc ...@@ -47,7 +46,9 @@ DropBear v2014.65 & 17 & 2 & tbc
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 inputs sent during a key re-exchange and would deliver them all once the exchange was done. responses for inputs sent during a key re-exchange and would deliver them all once the exchange was done.
A considerable number of states were added due to {\dmapper} generated outputs such as \textsl{ch\_none} or \textsl{ch\_max}, outputs which signal that no channel is open or A considerable number of states were added due to {\dmapper} generated outputs such as \textsl{ch\_none} or \textsl{ch\_max}, outputs which signal that no channel is open or
that the maximum number of channels have been opened. To give a concrete example, the {\dmapper} on every \textsl{ch\_open} saves a channel identifier. If \textsl{ch\_open} that the maximum number of channels have been opened.
is called again, a \textsl{ch\_max} output is generated. The channel identifier is removed by a \textsl{ch\_close} input leading to pairs of %To give a concrete example, the {\dmapper} on every \textsl{ch\_open} saves a channel identifier and sends
states with existing and non-existing channel identifiers, even in states where channels are not relevant (like for example states before authentication). %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).
...@@ -23,7 +23,7 @@ state of the {\dsut} is one where a TCP connection has been established and wher ...@@ -23,7 +23,7 @@ state of the {\dsut} is one where a TCP connection has been established and wher
%figure %figure
%It is therefore important to focus on messages for which interesting state-changing behaviour can be expected. %It is therefore important to focus on messages for which interesting state-changing behaviour can be expected.
\subsection{The learning alphabet} \subsection{The learning alphabet}\label{subsec:setup}
We split the learning alphabet into 3 groups, corresponding to the three layers. %Each input in the alphabet has a corresponding message number in the SSH specification. We split the learning alphabet into 3 groups, corresponding to the three layers. %Each input in the alphabet has a corresponding message number in the SSH specification.
Learning doesn't scale with a growing alphabet, hence it is important to reduce the alphabet to those inputs that trigger interesting behavior. We do this by Learning doesn't scale with a growing alphabet, hence it is important to reduce the alphabet to those inputs that trigger interesting behavior. We do this by
only selecting inputs that are consistent with our learning goal. only selecting inputs that are consistent with our learning goal.
...@@ -75,7 +75,7 @@ The Authentication Layer defines one single client message type in the form of t ...@@ -75,7 +75,7 @@ The Authentication Layer defines one single client message type in the form of t
\label{auth-alphabet} \label{auth-alphabet}
\end{table} \end{table}
The Connection Layer allows the client manage channels and to request services over a single channel. In accordance with our learning goal, The Connection Layer allows the client manage channels and to request/run services over them. In accordance with our learning goal,
our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}. our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}.
...@@ -105,11 +105,11 @@ The {\dmapper} must provide translation between abstract message representations ...@@ -105,11 +105,11 @@ The {\dmapper} must provide translation between abstract message representations
The {\dmapper} maintains a set of state variables which have initial values, and which are updated on specific outputs and used in concretize certain inputs. On receiving a \textsc{kexinit}, the {\dmapper} saves the {\dsut}'s parameter preferences. These preferences define the key exchange, hashing and encryption algorithms supported by the {\dsut}. Before such receipt, these parameters are defaulted to those that any implementation should support, as required by the RFC. Based on these parameters, a key exchange algorithm may be run. The {\dmapper} supports Diffie-Hellman, which it can initiate via a \textsc{kex30} input from the learner. The {\dsut} responds with \textsc{kex31} if the inputs were orderly sent. From \textsc{kex31}, 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. The {\dmapper} contains two other state variables, used for storing the channel and sequence numbers respectively. The former is retrieved from a \textsc{ch\_accept} response and re-used in the other channel-type inputs, the latter each retrieved from each packet received and used in \textsc{unimpl} inputs. Both variables are initially set to 0. The {\dmapper} maintains a set of state variables which have initial values, and which are updated on specific outputs and used in concretize certain inputs. On receiving a \textsc{kexinit}, the {\dmapper} saves the {\dsut}'s parameter preferences. These preferences define the key exchange, hashing and encryption algorithms supported by the {\dsut}. Before such receipt, these parameters are defaulted to those that any implementation should support, as required by the RFC. Based on these parameters, a key exchange algorithm may be run. The {\dmapper} supports Diffie-Hellman, which it can initiate via a \textsc{kex30} input from the learner. The {\dsut} responds with \textsc{kex31} if the inputs were orderly sent. From \textsc{kex31}, 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. The {\dmapper} contains two other state variables, used for storing the channel and sequence numbers respectively. The former is retrieved from a \textsc{ch\_accept} response and re-used in the other channel-type inputs, the latter each retrieved from each packet received and used in \textsc{unimpl} inputs. Both variables are initially set to 0.
In certain scenarios, inputs are answered by the {\dmapper} directly instead of being sent to the {\dsut}. These scenarios are the following: In certain scenarios, inputs are answered by the {\dmapper} directly instead of being sent to the {\dsut}. These scenarios include the following:
\begin{enumerate} \begin{enumerate}
\item connection with the {\dsut} was terminated, case in which the {\dmapper} responds with a \textsc{no\_conn} message \item if connection with the {\dsut} was terminated, the {\dmapper} responds with a \textsc{no\_conn} message
\item no channel has been opened or the maximum number of channels was reached (in our experiments 1), cases which prompt the {\dmapper} \item no channel has been opened or the maximum number of channels was reached (in our experiments 1), cases which prompt the {\dmapper}
to respond with \textsc{ch\_none}, and \textsc{ch\_max} respectively to respond with \textsc{ch\_none}, or \textsc{ch\_max} respectively
\end{enumerate} \end{enumerate}
Overall, we notice that in many ways, the {\dmapper} acts similarly to an SSH client. Hence it is unsurprising that it was built off an existing Overall, we notice that in many ways, the {\dmapper} acts similarly to an SSH client. Hence it is unsurprising that it was built off an existing
......
...@@ -10,6 +10,18 @@ ...@@ -10,6 +10,18 @@
} }
\makeatother \makeatother
\newcommand{\A}{{\cal A}}
\newcommand\CH{{\cal H}}
\newcommand{\M}{{\cal M}}
%MAPPERS
\newcommand{\abstr}{{\lambda}}
\newcommand{\ABS}[2]{{\alpha_{#2}(#1)}}
\newcommand{\CONC}[2]{{\gamma_{#1}(#2)}}
\newcommand{\hypo}{\CH\xspace}
% %
\specialterms{server,client,learner,segments,{\sc sul} adapter,network adapter,observation tree} \specialterms{server,client,learner,segments,{\sc sul} adapter,network adapter,observation tree}
......
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