Commit 1d645ada authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Rick replacement

parent 8e5245cb
\section{Introduction}\label{introduction}
SSH is a security protocol that is widely used to interact securely with
remote machines. SSH -- or more precisely, the transport layer
protocol of SSH -- has been subjected to security analysis
remote machines. The Transport layer of SSH has been subjected to security analysis
\cite{Williams2011Analysis}, incl.\ analyses that revealed
cryptographic shortcomings
\cite{Albrecht2009Plaintext,Bellare2004Breaking,Paterson2010PlaintextDependent}.
But whereas these analyses consider the abstract cryptographic
Whereas these analyses consider the abstract cryptographic
protocol, this paper looks at actual implementations of SSH, and
investigates flaws in the program logic of these implementations,
rather than cryptographic flaws. Such logical flaws have occurred in
......@@ -27,14 +26,21 @@ Moreover, by formalizing the
properties we can better assess and overcome vagueness or
under-specification in the RFC standards.
Model learning obtains a state machine model of a black-box system by
providing inputs and observing outputs. Since model learning uses a
finite number of observations, we can never be sure that the learned
model is correct. To that end, advanced conformance algorithms are employed
\cite{LeeY96}, which yield some confidence that the system inferred is
in fact complete. In the context of testing security protocols, model
learning can be seen as a form of fuzzing, where inputs are sent in
unexpected orders to expose any hidden anomalies.
This paper is born out of two recent theses \cite{Verleg2016,Toon2016},
and is to our knowledge the first combined application of model
learning and model checking in verifying SSH implementations, or more
generally, implementations of any network security protocol.
%Model learning obtains a state machine model of a black-box system by
%providing inputs and observing outputs. Since model learning uses a
%finite number of observations, we can never be sure that the learned
%model is correct. To that end, advanced conformance algorithms are employed
%\cite{LeeY96}, which yield some confidence that the system inferred is
%in fact complete. In the context of testing security protocols, model
%learning can be seen as a form of fuzzing, where inputs are sent in
%unexpected orders to expose any hidden anomalies.
\paragraph{Related work}
......@@ -68,11 +74,6 @@ testing of SSH implementations \cite{Boss2012}. All this research
only considered the SSH transport layer, and not the other SSH
protocol layers.
This paper is born out of two recent theses \cite{Verleg2016,Toon2016},
and is to our knowledge the first combined application of model
learning and model checking in verifying SSH implementations, or more
generally, implementations of any network security protocol.
Model learning has previously been used to infer state machines of
EMV bank cards~\cite{Aarts2013Formal}, electronic
passports~\cite{Aarts2010Inference}, hand-held readers for online
......
\section{Model learning background}\label{sec:prelims}
\section{Model learning}\label{sec:prelims}
\subsection{Mealy machines} \label{ssec:mealy}
A \emph{Mealy machine} is a tuple $\M = (I, O, Q, q_0, \delta, \lambda)$, where
$I$ is a finite set of inputs,
......
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