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

Added conclusions

parent d31ea149
\section{Conclusions}\label{sec:conclusions}
We have combined model learning with abstraction techniques to infer models of the OpenSSH, Bitvise and Dropbear SSH server implementations. We have also
formalized several security and functional properties drawn from the SSH RFC specifications. We have verified these
properties on the learned models using model checking and have uncovered several minor inconsistencies, though crucially, the main security goals were met
by all implementation.
Abstraction was provided by a {\dmapper} component placed between the {\dlearner} and the {\dsut}. The {\dmapper} was constructed from an existing SSH
implementation. The alphabet the {\dmapper} exposed to the {\dlearner} explored key exchange and setting up a secure connection, several authentication methods
and opening and closing single of channels over which the terminal service could be requested. We used two alphabets, a full version for OpenSSH, and
a restricted version for the other implementations. The restricted alphabet was still sufficient explore all aforementioned behavior.
There were several challenges encountered. Firstly, building a {\dmapper} presented a considerable technical challenge, as it required re-structuring of an actual
SSH implementation. Secondly, because we used classical learning algorithms, we had to ensure that the abstracted implementation behaved
like a deterministic Mealy Machine. Herein, time induced non-determinism, like in other works, was difficult to eliminate. Buffering also presented problems,
leading to a considerable increase in the number of states. Moreover, the systems analyzed were relatively slow, which meant learning and testing took
several days. This was compounded by the size of the learning alphabet, and it forced us into using a reduced alphabet for two of the analyzed implementations.
Limitations of the work, thus elements for future work, are several. First of all, the {\dmapper} was not formalized, unlike in~\ref{TCP2016}, thus we could not
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,
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.
Despite these limitations, our work provides a demonstrative 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.
\ No newline at end of file
......@@ -66,8 +66,8 @@ The Authentication Layer defines one single client message type in the form of t
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{ua\_none} & Authenticates with the ``none'' method~\cite[p. 7]{rfc4252} \\
\textsc{ua\_pk\_ok} & Provides a valid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pk\_nok} & Provides an invalid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pk\_ok}* & Provides a valid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pk\_nok}* & Provides an invalid name/key combination~\cite[p. 8]{rfc4252} \\
\textsc{ua\_pw\_ok} & Provides a valid name/password combination~\cite[p. 10]{rfc4252} \\
\textsc{ua\_pw\_nok} & Provides an invalid name/password combination~\cite[p. 10]{rfc4252} \\
\end{tabular}
......@@ -84,13 +84,13 @@ our mapper only supports inputs for requesting terminal emulation, plus inputs f
\small
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{ch\_open} & Opens a new channel~\cite[p. 5]{rfc4254} \\
\textsc{ch\_close} & Closes a channel~\cite[p. 9]{rfc4254} \\
\textsc{ch\_eof} & Indicates that no more data will be sent~\cite[p. 9]{rfc4254} \\
\textsc{ch\_data} & Sends data over the channel~\cite[p. 7]{rfc4254} \\
\textsc{ch\_open}* & Opens a new channel~\cite[p. 5]{rfc4254} \\
\textsc{ch\_close}* & Closes a channel~\cite[p. 9]{rfc4254} \\
\textsc{ch\_eof}* & Indicates that no more data will be sent~\cite[p. 9]{rfc4254} \\
\textsc{ch\_data}* & Sends data over the channel~\cite[p. 7]{rfc4254} \\
\textsc{ch\_edata} & Sends typed data over the channel~\cite[p. 8]{rfc4254} \\
\textsc{ch\_window\_adjust} & Adjusts the window size~\cite[p. 7]{rfc4254} \\
\textsc{ch\_request\_pty} & Requests terminal emulation~\cite[p. 11]{rfc4254} \\
\textsc{ch\_request\_pty}* & Requests terminal emulation~\cite[p. 11]{rfc4254} \\
\end{tabular}
\caption{Connection Layer inputs}
\label{conn-alphabet}
......
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