Commit bf67ebf5 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated files. Now should work

parent be6ea791
......@@ -10,7 +10,7 @@ learned over a localhost connection, whereas BitVise was learned over a virtual
Certain arrangements had to be made including the setting of timing parameters to fit each implementation.
OpenSSH was learned using a full alphabet, whereas DropBear and BitVise were learned using a reduced alphabet. Both versions of
the alphabets are described in Subsection~\ref{sec:alphabet}. The primary reason for using a reduced alphabet was to reduce learning times.
the alphabets are described in Subsection~\ref{subsec:alphabet}. The primary reason for using a reduced alphabet was to reduce learning times.
Most inputs excluded were inputs that either didn't change behavior (like \textsl{debug} or \textsl{unimpl}), or that triggered behavior
predictably similar to other inputs. As an example, \textsl{ua\_pw\_ok} contours the same behavior as \textsl{ua\_pk\_ok}. But while authenticating
with a public key was done quickly, authenticating with a username/password proved expensive (it would take the system 2-3 seconds to respond to
......
......@@ -11,7 +11,7 @@ The learning setup consists of three components: a \emph{learner}, \emph{mapper}
The learner uses LearnLib ~\cite{LearnLib2009}, a Java library implementing $L^{\ast}$ based algorithms for learning Mealy machines. The {\dmapper} is based on Paramiko, an open source SSH implementation written in Python\footnote{Paramiko is available at \url{http://www.paramiko.org/}}. We opted for Paramiko because its code is relatively well structured and documented. The {\dsut} can be any existing implementation of a SSH server. The {\dlearner} communicates with the {\dmapper} over sockets. A graphical representation of our setup is shown in Figure~\ref{fig:components}.
\begin{figure}
\centering
\includegraphics[scale=0.35]{example-components.pdf}
\includegraphics[scale=0.60]{setup.png}
\caption{The SSH learning setup.}
\label{fig:components}
\end{figure}
......@@ -23,7 +23,7 @@ state of the {\dsut} is one where a TCP connection has been established and wher
%figure
%It is therefore important to focus on messages for which interesting state-changing behaviour can be expected.
\subsection{The learning alphabet}\label{subsec:setup}
\subsection{The learning alphabet}\label{subsec:alphabet}
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
only selecting inputs that are consistent with our learning goal.
......
......@@ -11,10 +11,10 @@
\makeatother
\newcommand{\A}{{\cal A}}
\newcommand\CH{{\cal H}}
\newcommand{\A}{{\mathcal A}}
\newcommand\CH{{\mathcal H}}
\newcommand{\M}{{\cal M}}
\newcommand{\M}{{\mathcal M}}
%MAPPERS
\newcommand{\abstr}{{\lambda}}
......
\documentclass[sigconf]{acmart}
\usepackage{booktabs} % For formal tables
%\usepackage{algorithm}% http://ctan.org/pkg/algorithms
\usepackage{amssymb} % math stuff
......@@ -13,18 +12,6 @@
tabsize=2
}
\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}
% Copyright
%\setcopyright{none}
%\setcopyright{acmcopyright}
......
......@@ -101,4 +101,4 @@ concrete inputs to abstract inputs and concrete outputs to abstract outputs. For
%\item The transport layer protocol. This creates the basis for communication between server and client, providing a key exchange protocol and server authentication. The key exchange protocol is performed through three roundtrips. During the first, both client and server send a KEXINIT message. Then, the client sends a KEX30 message, the server responds with a KEX31 message. Finally, both parties send a NEWKEYS message, which indicates that the keys sent in the second step can be used.
%\item The user authentication protocol. This component is used to authenticate a client to the server, for example, through a username and password combination, or through SSH-keys.
%\item The connection protocol. This is used to provide different services to the connected client, it can thus multiplex the encrypted channel into different channels. The provided services can be services like file transfer or a remote terminal. Typical messages are requests for opening or closing channels, or requests for earlier named services.
\end{itemize}
\ No newline at end of file
%\end{itemize}
\ No newline at end of file
......@@ -162,10 +162,12 @@ G ( ( (in = CH_OPEN & out = CH_OPEN_SUCCESS) ->
%The Connection Layer RFC states that upon receiving a CH_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH_CLOSE would no longer have to be issued.
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents the model checking results. Crucially, all the critical security properties hold.
\begin{center}\small
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the critical security properties hold.
%\begin{center}\small
% \centering
\begin{table}
\centering
\small
\begin{tabular}{| r | r | ccc |}
\hline
& & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5}
......@@ -179,10 +181,10 @@ Table~\ref{tab:mcresults} presents the model checking results. Crucially, all th
& Prop. 7 & & & \\ \cline{2-5}
& Prop. 8 & & & \\ \hline
\end{tabular}
\label{tab:mcresults}
\caption{Model checking results}
\end{table}
\end{center}
\label{tab:mcresults}
\end{table}
%\end{center}
......
......@@ -25,6 +25,19 @@
title = {Principles and methods of testing finite state machines --- a survey}
}
@inproceedings{SMJV15,
author = {W. Smeenk and J. Moerman and D.N. Jansen and F.W. Vaandrager},
booktitle = {Proceedings 17th International Conference on Formal Engineering Methods (ICFEM 2015), Paris, 3-6 November 2015},
series = {Lecture Notes in Computer Science},
volume = 9407,
pages = {1--17},
publisher = {Springer-Verlag},
year = 2015,
editor = {M. Butler and S. Conchon and F. Zaidi},
title = {Applying Automata Learning to Embedded Control Software}
}
@MastersThesis{Toon2016,
title={Improving Protocol State Fuzzing of SSH},
author={Lenaerts, T},
......@@ -135,7 +148,22 @@ machine learning algorithms},
year = {2014}
}
@electronic{FutoranskyAttack,
@article{AJUV15,
author = {F. Aarts and B. Jonsson and J. Uijen and F.W. Vaandrager},
title = {Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction},
journal= {Formal Methods in System Design},
year= {2015},
issn= {0925-9856},
doi= {10.1007/s10703-014-0216-x},
url= {http://dx.doi.org/10.1007/s10703-014-0216-x},
publisher= {Springer US},
keywords= {Active automata learning; Mealy machines; Abstraction techniques; Communication protocols; Session initiation protocol; Transmission control protocol},
volume = 46,
number = 1,
pages= {1-41}
}
@article{FutoranskyAttack,
author = {Futoransky, Ariel and Kargieman, Emiliano},
citeulike-article-id = {13837770},
edition = {oct. 1998},
......
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