Commit 55c219d0 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated tex files

parent 75be428d
This diff is collapsed.
\section{Learning results} \label{sec:result}
\section{Learning Results} \label{sec:result}
\newcommand{\dk}{\emph{k}}
We use the setup described in Section~\ref{sec:setup} to learn models for OpenSSH, Bitvise and DropBear SSH server implementations.
OpenSSH represents the focal point, as it is the most popular implementation of SSH (with over 80 percent of market share in 2008~\cite{Albrecht2009Plaintext})
......@@ -57,6 +57,7 @@ give a glimpse into the issue of scalability. Assuming each input took 0.5 secon
\centering
\small
\caption{Statistics for learning experiments}
\vspace{-2mm}
\begin{tabular}{|l|l|l|l|l|l|l|}
\hline
{\centering{\textbf{SUT}}} & \textbf{States} & \textbf{Hypotheses } & \textbf{Mem. Q.} & \textbf{Test Q.}\\ \hline %& \textbf{Tests to last Hyp.} & \textbf{Tests on last Hyp.} \\ \hline
......
\section{The learning setup} \label{sec:setup}
\section{The Learning Setup} \label{sec:setup}
%This chapter will cover the setup used to infer the state machines. We provide a general setup outline in Section~\ref{components}. The tested SSH servers are described in Section~\ref{suts}, which were queried with the alphabet described in Section~\ref{alphabet}. Section~\ref{setup-handling} will cover the challenging SUT behaviour faced when implementing the mapper, and the adaptations that were made to overcome these challenges. Section~\ref{layers-individual} will discuss the relation between state machines for individual layers and the state machine of the complete SSH protocol. The conventions on visualisation of the inferred state machines are described in Section~\ref{visualisation}.
%Throughout this chapter, an individual SSH message to a SUT is denoted as a \textit{query}. A \textit{trace} is a sequence of multiple queries, starting from a SUT's initial state. Message names in this chapter are usually self-explanatory, but a mapping to the official RFC names is provided in Appendix~\ref{appendixa}.
......@@ -25,7 +25,7 @@ state of the {\dsut} is one where a TCP connection has already been established
%figure
%It is therefore important to focus on messages for which interesting state-changing behaviour can be expected.
\subsection{The learning alphabet}\label{subsec:alphabet}
\subsection{The Learning Alphabet}\label{subsec:alphabet}
The alphabet we use consists of inputs, which correspond to messages
......@@ -154,7 +154,7 @@ The restricted alphabet only supports the most general channel management inputs
%table
\subsection{The mapper}\label{subsec:mapper}
\subsection{The Mapper}\label{subsec:mapper}
The {\dmapper} must provide a translation between abstract messages
and well-formed SSH messages: it has to translate abstract inputs
......@@ -214,7 +214,7 @@ responds with a \textsc{no\_conn} message, as sending further messages to the {\
%
\subsection{Practical complications}
\subsection{Practical Complications}
%There are three practical complications in learning models of SSH
%servers: (1) an SSH server may exhibit \emph{non-determistic}
......
......@@ -11,7 +11,7 @@
\usepackage{ upgreek }
\usepackage{graphicx}
\usepackage{tikz}
\pagestyle{plain} % EP These lines to add page numbers,
%\pagestyle{plain} % EP These lines to add page numbers,
\thispagestyle{plain} % EP which is useful for reviewers.
%\usepackage{subcaption}
......@@ -155,7 +155,7 @@ all tested SSH server models satisfy the stated security properties,
% We no longer use \terms command
%\terms{Theory}
\keywords{Model learning, model checking, SSH protocol}
\keywords{Model learning, Model checking, SSH protocol}
\maketitle
......
\section{Model learning}\label{sec:prelims}
\subsection{Mealy machines} \label{ssec:mealy}
\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,
$O$ is a finite set of outputs,
......
\section{Security specifications} \label{sec:specs}
\section{Security Specifications} \label{sec:specs}
%\newfloat{property}{thp}{lop}
%\floatname{property}{Property}
......@@ -73,6 +73,7 @@ This function updates the output and state variables for a given valuation of th
\end{lstlisting}
\end{minipage}
\end{tabular}
\vspace{-3mm}
\caption{Mealy machine + associated NuSMV code}
\label{fig:nusmvex}
\end{figure}
......@@ -129,7 +130,7 @@ $p\,W\,q\, =\, p \,U\, q\, | \, G\, p$. Many of the higher layer properties we
%In the actual specification, W was replaced by this re-formulation. %Finally, we may define properties which we later use when defining other properties. This feature again isn't supported by NuSMV, hence the properties appear in expanded form in the run specification.
\subsection{Basic characterizing properties}
\subsection{Basic Characterizing Properties}
%cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met.
In our setting, a single TCP connection is made and once this connection is lost (e.g.\ because the system disconnects) it cannot be re-established. The moment
......@@ -159,7 +160,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\label{prop:channel}
\end{property}
\subsection{Security properties}
\subsection{Security Properties}
In SSH, upper layer services rely on security guarantees ensured by lower layers. So these services should not be available before the lower layers have completed. For example, the authentication service should only become available \emph{after} a successful key exchange and the seting up of a secure tunnel by the Transport layer, otherwise the service would be running over an unencrypted channel. Requests for this service should therefore not succeed unless key exchange was performed successfully.
Key exchange involves three steps that have to be performed in order but may be interleaved by other actions. Successful authentication necessarily implies successful execution of the key exchange steps. We can tell each key exchange step was successful from the values of the input and output variables. Successful authentication request is indicated by the predicate defined earlier, {\dreqauth}. Following these principles, we define the LTL specification in Property~\ref{prop:sec-trans}, where O is the once operator. Formula $O p$ is true at time $t$ if $p$ held in at least one of the previous time steps $t' \leq t$.
......@@ -194,7 +195,7 @@ Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$
\label{prop:sec-auth}
\end{property}
\subsection{Key re-exchange properties}
\subsection{Key Re-exchange Properties}
According to the RFC \cite[p. 24]{rfc4254}, re-exchanging keys (or rekeying) (1) is preferably allowed in all states of the protocol, and (2) its successful execution does not affect operation of the higher layers. We consider two general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These may map to multiple states in the learned models. We formalized requirement (1) by
two properties, one for each general state. In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request, indicated by the predicate {\dreqauth}. Once here, performing the inputs for rekey in succession should imply success until one of two things happen, the connection is lost(\dconnlost) or we have authenticated. This is asserted in Property~\ref{prop:rpos-pre-auth}. A similar property is defined for the authenticated state.
\begin{property}
......@@ -226,7 +227,7 @@ We therefore checked this requirement directly, by writing a simple script which
%\textit{Perhaps this could be merged into one property?}
\subsection{Functional properties}
\subsection{Functional Properties}
We formalized and checked several other properties drawn from the RFCs. We found parts of the specification unclear, which sometimes meant that we had to give our own interpretation. A first general property can be defined for the \textsc{disconnect} output. The RFC specifies that after sending this message, a party MUST not send or receive any data \cite[p. 24]{rfc4253}. While we cannot tell what the server actually receives, we can check that the server does not generate any output after sending \textsc{disconnect}. After a \textsc{disconnect} message, subsequent outputs should be solely derived by the {\dmapper}. Knowing the {\dmapper} induced outputs are \textsc{no\_conn}, \textsc{ch\_max} and \textsc{ch\_none}, we formulate by Property~\ref{prop:trans-disc} to describe
expected outputs after a \textsc{disconnect}.
......@@ -325,7 +326,7 @@ G ( hasOpenedChannel ->
\newcommand{\df}{\color{red}X}
\subsection{Model checking results}
\subsection{Model Checking Results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for Bitvise
as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}).
In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of successful authentication.
......@@ -336,6 +337,7 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of
\centering
\small
\caption{Model checking results}
\vspace{-3mm}
\begin{tabular}{| l | l | c | c |c | c |}
\hline
% & & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
......@@ -353,7 +355,7 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of
& Prop.~\ref{prop:conn-close} & MUST & \dt & \dt & \dfce{sends CH\_EOF} \\ \hline
\end{tabular}
\label{tab:mcresults}
%\vspace{-5mm}
%\vspace{-2mm}
\end{table}
%\end{center}
......
\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 standard violations.
The security-critical properties were met by all implementations.
Abstraction was provided by a {\dmapper} component placed between the
{\dlearner} and the {\dsut}. The {\dmapper} was constructed from an
existing SSH implementation. The input alphabet of the {\dmapper}
explored key exchange, setting up a secure connection, several
authentication methods, and opening and closing channels over which the
terminal service could be requested. We used two input alphabets, a
full version for OpenSSH, and a restricted version for Bitvise and
DropBear. The restricted alphabet was still sufficient to
explore most aforementioned behavior.
We encountered several challenges. 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. Here time-induced non-determinism 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 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 implementations.
Limitations of the work, hence possibilities for future work, are several. First of all, the {\dmapper} was not formalized, unlike in~\cite{TCP2016}, thus we did not
produce a concretization of the abstract models. Consequently, model checking results cannot be fully transferred to the actual implementations. Formal definition
of the mapper and concretization of the learned models (as defined in \cite{AJUV15}) would tackle this. The {\dmapper} also caused considerable redundancy in the learned models; tweaking the abstractions used, in particular those for managing channels, could alleviate this problem while also improving learning times. This in turn would facilitate learning using expanded alphabets instead of resorting to restricted alphabets.
Furthermore, the {\dmapper} abstraction could be refined, to give more
insight into the implementations. In particular, parameters
such as the session identifier could be extracted from the {\dmapper} and potentially handled by existing Register Automata learners\cite{ralib2015,tomte2015}. These learners
can infer systems with parameterized alphabets, state variables and simple operations on data. Finally, we suppressed all timing-related behavior, as it could not be handled by the classical learners used; there is preliminary work on learning timed automata\cite{GrinchteinJL10} which could use timing behavior.
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 advances in learning techniques.
\section{Introduction}\label{introduction}
SSH is a security protocol that is widely used to interact securely with
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}.
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
implementations of other security protocols, notably TLS, with Apple's
'goto fail' bug and the FREAK attack \cite{Beurdouche:2017}. For this
we use model learning (a.k.a.\ active automata learning)
\cite{Angluin1987Learning,PeVaYa02,Vaa17} to infer state machines of three SSH
implementations, which we then analyze by model checking for
conformance to both functional and security properties.
The properties we verify for the inferred state machines are based on
the RFCs that specify SSH \cite{rfc4251,rfc4252,rfc4253,rfc4254}.
These properties are formalized in LTL and verified using
NuSMV~\cite{NuSMV2}.
We use a model checker since the models are too complex for manual inspection (they are trivial for NuSMV).
Moreover, by formalizing the
properties we can better assess and overcome vagueness or
under-specification in the RFC standards.
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}
%The SSH protocol has been investigated for cryptographic flaws, e.g.\
%\cite{Williams2011Analysis,Albrecht2009Plaintext,Bellare2004Breaking,Paterson2010PlaintextDependent},
%but that research does not consider logical flaws in actual software
%implementations.
Chen et al.\cite{ChenDW04} use the MOPS software model checking tool
to detect security vulnerabilities in the OpenSSH C implementation
due to violation of folk rules for the construction of secure programs
such as ``Do not open a file in writing mode to stdout or stderr''.
Udrea et al.\cite{Udrea_rule-based_2008} also investigated SSH
implementations for logical flaws. They used a static analysis tool to
check two C implementations of SSH against an extensive set of rules.
These rules not only express properties of the SSH protocol logic, but
also of message formats and support for earlier versions and various
options. Our analysis only considers the protocol logic. However,
their rules were tied to routines in the code, so had to be slightly adapted
to fit the different implementations. In contrast, our properties are
defined at an abstract level so do not need such tailoring. Moreover,
our black box approach means we can analyze any implementation
of SSH, not just open source C implementations.
Formal models of SSH in the form of state machines have been used
before, namely for a manual code review of OpenSSH
\cite{Poll_rigorous_2011}, formal program verification of a Java
implementation of SSH \cite{PollSchubert07}, and for model based
testing of SSH implementations \cite{Boss2012}. All this research
only considered the SSH Transport layer, and not the other SSH
protocol layers.
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
banking~\cite{Chalupar2014Automated}, and implementations of
TCP~\cite{TCP2016} and TLS~\cite{RuiterProtocol}. Some of these
studies relied on manual analysis of learned models
\cite{Aarts2013Formal,Aarts2010Inference,RuiterProtocol}, but some
also used model checkers \cite{TCP2016,Chalupar2014Automated}.
Instead of using active learning as we do, it is also possible to use
passive learning to obtain protocol state machines
\cite{Wang2011Inferring}. Here network traffic is observed, and not
actively generated. This can then provide a probabilistic
characterization of normal network traffic, but it cannot uncover
implementation flaws that occur in strange message flows, which is our
goal.
%Our approach, most closely resembles work on TCP~\cite{TCP2016},
%where they also combine classical learning and model checking to
%analyze various TCP implementations, with our work being more focused
%on security properties. Other case studies involving model learning
%rely on manual analysis of the learned models
%~\cite{Aarts2013Formal,TCP2016,Chalupar2014Automated,RuiterProtocol}.
%Our work differs, since we use a model checker to automatically check
%specifications. Inference of protocols has also been done from
%observing network traffic ~\cite{Wang2011Inferring}. Such inference
%is limited to the traces that occur over a network. Inference is
%further hampered if the analyzed protocols communicate over encrypted
%channels, as this severely limits information available from traces without knowledge of the security key.
%In this thesis, we will be using protocol state fuzzing to extract an implementations state machine. All fuzzing algorithms rely on the idea of sending unexpected input data to a system under test (SUT) in the hope that this triggers anomalies. Using protocol state fuzzing, however, we will fuzz on the \textit{order} of otherwise correctly-formed messages.
%This technique has previously been applied to infer state machines of EMV bank cards~\cite{Aarts2013Formal}, electronic passports~\cite{Aarts2010Inference} and hand-held readers for online banking~\cite{Chalupar2014Automated}. Furthermore, implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol} have state-fuzzed. As in these works, we implement state fuzzing
%
%State machines inferred are large and hard to check manually.
%Once a state machine has been inferred, security-related logical flaws are usually easily spotted by an auditor with some knowledge about the protocol~\cite{RuiterProtocol}. An example of a logical flaw is exchanging user credentials before an encrypted connection has been established.
%
%Besides security-related logical flaws, inferred state machines can show quirks such as superfluous states. Although these might not be directly exploitable, OpenBSD auditors illustrate why these small bugs should be resolved: ``we are not so much looking for security holes, as we are looking for basic software bugs, and if years later someone discovers the problem used to be a security issue, and we fixed it because it was just a bug, well, all the better''\footnote{\url{http://www.openbsd.org/security.html}}.
%
%\textit{Organization.} An outline of the SSH protocol will be provided in Section~\ref{ssh}. The experimental setup is discussed in Section~\ref{setup}. The results are subsequently discussed in Section~\ref{results}, after which we conclude in Section~\ref{conclusions}.
%
This diff is collapsed.
This diff is collapsed.
% Code to set up special term treatment: every first occurence is emphasized
\makeatletter
\newcommand{\specialterms}[1]{%
\@for\next:=#1\do
{\@namedef{specialterm@\detokenize\expandafter{\next}}{}}%
}
\newcommand\term[1]{%
\@ifundefined{specialterm@\detokenize{#1}}
{#1}{\emph{#1}\global\expandafter\let\csname specialterm@\detokenize{#1}\endcsname\relax}%
}
\makeatother
\newcommand{\A}{{\mathcal A}}
\newcommand\CH{{\mathcal H}}
\newcommand{\N}{{\mathcal N}}
\newcommand{\M}{{\mathcal 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}
%utils
\newcounter{quotecount}
\newcommand{\countquote}[1]{\vspace{1cm}\addtocounter{quotecount}{1}%
\parbox{10cm}{\em #1}\hspace*{2cm}(\arabic{quotecount})\\[1cm]}
% automata learning theory
\newcommand{\lstar}{\cal{L}*}
% learning components
\newcommand{\dlearner}{\sc learner}
\newcommand{\dmapper}{\sc mapper}
\newcommand{\dsut}{\sc sul}
\newcommand{\dsuts}{\sc suls}
%alphabet related
\newcommand{\dtimeout}{\sc noresp}
\ No newline at end of file
\documentclass[sigconf]{acmart}
\usepackage{booktabs} % For formal tables
%\usepackage{algorithm}% http://ctan.org/pkg/algorithms
\usepackage{amssymb} % math stuff
\usepackage{amsmath} % more math stuff
\usepackage{mathtools} % for \coloneqq (defines-symbol := )
\usepackage{graphicx} % for graphics
\usepackage{listings}
\usepackage{float}
\usepackage{color}
\usepackage{ upgreek }
\usepackage{graphicx}
\usepackage{tikz}
\pagestyle{plain} % EP These lines to add page numbers,
\thispagestyle{plain} % EP which is useful for reviewers.
%\usepackage{subcaption}
%\usepackage{subcaption}
\usetikzlibrary{automata, arrows,shapes.multipart}
\lstset{
tabsize=2
}
% Copyright
%\setcopyright{none}
%\setcopyright{acmcopyright}
%\setcopyright{acmlicensed}
\setcopyright{rightsretained}
%\setcopyright{usgov}
%\setcopyright{usgovmixed}
%\setcopyright{cagov}
%\setcopyright{cagovmixed}
% DOI
%\acmDOI{10.475/123_4}
% ISBN
%\acmISBN{123-4567-24-567/08/06}
%Conference
%%% The following is specific to SPIN'17 and the paper
%%% 'Model Learning and Model Checking of SSH Implementations'
%%% by Paul Fiterau-Brostean, Frits Vaandrager, Erik Poll, Joeri de Ruiter, Toon Lenaerts, and Patrick Verleg.
\setcopyright{acmcopyright} % Adjust this to match your publishing-rights agreement with ACM.
\acmDOI{10.1145/3092282.3092289}
\acmISBN{978-1-4503-5077-8/17/07}
\acmConference[SPIN'17]{International SPIN Symposium on Model Checking of Software }{July 2017}{Santa Barbara, CA, USA}
\acmYear{2017}
\copyrightyear{2017}
\acmPrice{15.00}
\include{macros}
\begin{document}
\graphicspath{{images/}}
\title{Model Learning and Model Checking of SSH Implementations}
%\title{Leveraging Model Learning and Model Checking to Infer and Verify SSH Implementations}
\renewcommand{\shorttitle}{Inference and Verification of SSH Implementations}
\author{Paul Fiter\u{a}u-Bro\c{s}tean}
\authornote{Supported by NWO project 612.001.216, Active Learning of Security Protocols (ALSEP).}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{p.fiterau-brostean@science.ru.nl}
\author{Toon Lenaerts}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{toon.lenaerts@student.ru.nl}
\author{Erik Poll}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{erikpoll@cs.ru.nl}
\author{Joeri de Ruiter}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{joeri@cs.ru.nl}
\author{Frits Vaandrager}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{F.Vaandrager@cs.ru.nl}
\author{Patrick Verleg}
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{patrickverleg@gmail.com}
\begin{abstract}
We apply model learning on three SSH implementations to infer state machine models, and then use model checking
to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that
all tested SSH server models satisfy the stated security properties,
but uncovered several violations of the standard.
%Frits: I would say the fingerprinting is a detail, standard violations much more important.
%The state machines of the implementations differ significantly, allowing them to be
%effectively fingerprinted.
%Various shortcomings with regards to the RFCs were found. Opening multiple channels is not properly implemented on CiscoSSH and PowerShell. OpenSSH contains a bug which can result in connection closure after rekeying in some circumstances. Both Tectia and OpenSSH implement a liberal message acceptance policy in the first phase of the protocol. Such a liberal policy is unwise in this error-prone stage.
\end{abstract}
%
% The code below should be generated by the tool at
% http://dl.acm.org/ccs.cfm
% Please copy and paste the code instead of the example below.
%
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003033.10003039.10003041</concept_id>
<concept_desc>Networks~Protocol correctness</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10010070.10010071.10010286</concept_id>
<concept_desc>Theory of computation~Active learning</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10010940.10010992.10010998.10003791</concept_id>
<concept_desc>Software and its engineering~Model checking</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10002978.10002986.10002990</concept_id>
<concept_desc>Security and privacy~Logic and verification</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10002978.10003014</concept_id>
<concept_desc>Security and privacy~Network security</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Networks~Protocol correctness}
\ccsdesc[500]{Theory of computation~Active learning}
\ccsdesc[500]{Software and its engineering~Model checking}
\ccsdesc[300]{Security and privacy~Logic and verification}
\ccsdesc[300]{Security and privacy~Network security}
% We no longer use \terms command
%\terms{Theory}
\keywords{Model learning, Model checking, SSH protocol}
\maketitle
\renewcommand{\shortauthors}{Fiter\u{a}u-Bro\c{s}tean et al.}
\input{introduction}
\input{preliminaries}
\input{the_sut}
\input{learning_setup}
\input{learning_results}
\input{security_definitions}
\input{conclusions}
\bibliographystyle{ACM-Reference-Format}
\bibliography{sigproc}
\end{document}
\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,
$O$ is a finite set of outputs,
$Q$ is a finite set of states,
$q_0 \in Q$ is the initial state,
$\delta: Q \times I \rightarrow Q$ is a transition function, and
$\lambda: Q \times I \rightarrow O$ is an output function.
%
Output function $\lambda$ is extended to sequences of inputs by defining,
for all $q \in Q$, $i \in I$ and $\sigma \in I^{\ast}$,
%\begin{eqnarray*}
%\delta(q, \epsilon) = q &,~~~ & \delta(q, i \sigma) = \delta(\delta(q,i), \sigma),\\
$\lambda(q, \epsilon) = \epsilon$ and $\lambda(q, i \sigma) = \lambda(q, i) \lambda(\delta(q, i), \sigma)$.
%\end{eqnarray*}
%
The behavior of Mealy machine $\M$ is defined by function $A_\M : I^{\ast} \rightarrow O^{\ast}$ with
$A_\M(\sigma) = \lambda (q^0, \sigma)$, for $\sigma \in I^{\ast}$.
Mealy machines $\M$ and $\N$ are \emph{equivalent}, denoted $\M \approx \N$, iff $A_{\M} = A_{\N}$.
Sequence $\sigma \in I^{\ast}$ \emph{distinguishes}
$\M$ and $\N$ if and only if $A_{\M}(\sigma) \neq A_{\N}(\sigma)$.
%\begin{figure}[h]
%\centering
%\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
% \node[initial,state] (q0) {$q_0$};
% \node[state] (q1) [right of=q0] {$q_1$};
% \node[state] (q2) [right of=q1] {$q_2$};
%
% \path[->] (q0) edge node [below] {X/A} (q1);
% \path[->] (q1) edge node [below] {Y/B} (q2);
% \path[->] (q0) edge [bend left] node {Y/A} (q2);
% \path[->] (q2) edge [loop right] node [text centered, text width = 1cm] {X/A \\ Y/B} (q2);
% \path[->] (q1) edge [loop below] node {X/B} (q1);
%\end{tikzpicture}
%\caption{Example Mealy machine}
%\label{mealy example}
%\end{figure}
\subsection{MAT Framework} \label{ssec:mat}
The most efficient algorithms for model learning (see~\cite{Isberner2015} for a recent overview) all follow
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Angluin1987Learning}.
Here learning is viewed as a game in which a \textit{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 {\dlearner} only knows the input alphabet $I$ and output alphabet $O$ of $\M$.
The task of the {\dlearner} is to learn $\M$ via two types of queries:
\begin{itemize}
\item
With a \emph{membership query}, the {\dlearner} asks what the response is to an input sequence $\sigma \in I^{\ast}$.
The teacher answers with the output sequence in $A_{\M}(\sigma)$.
\item
With an \emph{equivalence query}, the {\dlearner} asks whether a hypothesized Mealy machine $\CH$ is correct, that is,
whether $\CH \approx \M$. The teacher answers \emph{yes} if this is the case. Otherwise it answers
\emph{no} and supplies a \emph{counterexample}, which is a sequence $\sigma \in I^{\ast}$ that triggers
a different output sequence for both Mealy machines, that is, $A_{\CH}(\sigma) \neq A_{\M}(\sigma)$.
\end{itemize}
%
The MAT framework can be used to learn black box models of software.
If the behavior of a software system, or System Under Learning ({\dsut}), can be described by some unknown Mealy machine $\M$,
then a membership query can be implemented by sending inputs to the {\dsut} and observing resulting outputs.
An equivalence query can be approximated using a conformance testing tool \cite{LeeY96} via a finite number of \emph{test queries}.
A test query consists of asking the {\dsut} for the response to an input sequence
$\sigma \in I^{\ast}$, similar to a membership query.
Note that this cannot rule out that there is more behavior
that has not been discovered.
\subsection{Abstraction} \label{ssec:mappers}
Most current learning algorithms are only applicable to Mealy machines with small alphabets comprising abstract messages. Practical systems typically
have parameterized input/output alphabets, whose application triggers updates on the system's state variables. To learn
these systems we place a \emph{mapper} between the {\dlearner} and the {\dsut}. The {\dmapper} is a transducer which translates
concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough discussion of mappers, we refer to \cite{AJUV15}.
%Perhaps some explanation
%
%
%concrete inputs in $I$ to abstract inputs in $X$,
%concrete outputs in $O$ to abstract outputs in $Y$, and vice versa.
%alphabets
%
%
%Starting from Angluin's seminal $L^{\ast}$ algorithm \cite{Ang87}, many
%algorithms have been proposed for learning finite, deterministic Mealy machines
%via a finite number of queries. We refer to \cite{Isberner2015} for recent overview.
%In applications in which one wants to learn a model of a black-box reactive system, the teacher typically
%consists of a System Under Learning (\dsut) that answers the membership queries, and a conformance
%testing tool \cite{LeeY96} that approximates the equivalence queries using a set
%of \emph{test queries}. A test query consists of asking to the \dsut for the response to an input sequence
%$\sigma \in I^{\ast}$, similar to a membership query.
%
%
%
%
%
%
%In protocol state fuzzing, a state machine of the implementation is learned by actively sending and receiving messages to and from the System Under Learning (SUL). A single message is called a \textit{query}, and a sequence of messages a \textit{trace}. The state machine is formed by sending consecutive traces to the SUL and analyzing the output. The trace to be sent is, in our case, determined by the L*-algorithm. When a trace is completed the SUL has to be reset to its initial state.
%
%After sending a sufficient amount of traces, a hypothesis is formed. The hypothesis is checked for by a testing oracle. Said oracle sends traces to the SUL, predicts an output through the hypothesis, and compares this output to the actual output received by the SUL.
%
%In our case, sending messages to the SUL means sending packets that contain, for example, the length of the packet, a sequence number or a list of supported encryptions. This information is unnecessary for the learning process, and is not supported by the Learnlib implementation of L* that we use. We abstract all this information away, leaving us with an abstract representation of messages. To convert these abstract messages to correct packets and back, a mapper is used. This mapper has to keep track of state variables, and has to be able to perform actions such as encryption and compression. This means that the mapper itself contains a state machine, which is based on existing knowledge about the protocol used in the SUL.
%
%\begin{figure}[h]
%\centering
%\includegraphics[scale=0.8]{Naamloos.png}
%\caption{A learning setup}
%\label{learning setup}
%\end{figure}
%
%The setup shown in figure \ref{learning setup} is the setup Verleg used, and serves as an example for a typical learning setup, here ``Learner'' is the program that uses the L*-algorithm to generate traces to send to the SUL, these traces are in the form of abstract messages. The learner sends these messages to the mapper, which translates them to concrete packages which are sent to the SUL. A response of the SUL is then converted by the mapper to an abstract message and sent to the learner.
%
%\subsection{Secure Shell} \label{secure shell}
%
%The SSH-protocol uses a client-server structure consisting of three components. These components will be referred to as layers, however note that outer layers do not wrap inner layers, instead messages of different layers are distinguished through their message number. The three components are as follows:
%\begin{itemize}
%\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}
This diff is collapsed.
\section{The Secure Shell Protocol} \label{sec:ssh}
The Secure Shell Protocol (or SSH) is a protocol used for secure remote login and other secure network services over an insecure network. It runs as an application layer protocol on top of TCP, which provides reliable data transfer, but does not provide any form of connection security. The initial version of SSH was superseded by a second version (SSHv2), after the former was found to contain design flaws which could not be fixed without losing backwards compatibility~\cite{FutoranskyAttack}. This work focuses on SSHv2.
SSHv2 follows a client-server paradigm. The protocol consists of three layers (Figure~\ref{fig:sshcomponents}):
\begin{enumerate}
\item The \textit{transport layer protocol} (RFC 4253~\cite{rfc4253}) forms the basis for any communication between a client and a server. It provides confidentiality, integrity and server authentication as well as optional compression.
\item The \textit{user authentication protocol} (RFC 4252~\cite{rfc4252}) is used to authenticate the client to the server.
\item The \textit{connection protocol} (RFC 4254~\cite{rfc4254}) allows the encrypted channel to be multiplexed in different channels. These channels enable a user to run multiple applications, such as terminal emulation or file transfer, over a single SSH connection.
\end{enumerate}
\begin{figure}[t] % was !hb
\centering
\includegraphics[scale=0.20]{SSH_protocols.png}
\caption{SSH protocol layers}
\label{fig:sshcomponents}
\vspace{-3mm}
\end{figure}
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers, and different layers can interact. For this reason, we opt to analyze SSH as a whole, instead of analyzing its constituent layers independently. Below we discuss each layer, outlining the relevant messages which are later used in learning, and characterizing the so-called \textit{happy flow} that a normal protocol run follows.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the Transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys, which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to access services on the server, for example the terminal service.
%Different layers are identified by their message numbers. These message numbers will form the basis of the state fuzzing. The SSH protocol is especially interesting because outer layers do not encapsulate inner layers. This means that different layers can interact. One could argue that this is a less systematic approach, in which a programmer is more likely to make state machine-related errors.
\subsection{Transport layer}\label{ssh-run-trans}
SSH runs over TCP, and provides end-to-end confidentiality and integrity using session keys. Once a TCP connection has been established with the server, these session keys are securely negotiated using a \textsl{key exchange} algorithm, the first step of the protocol. The key exchange begins by the two sides exchanging their preferences for the key exchange algorithm to be used, as well as encryption, compression and hashing algorithms. Preferences are sent with a \textsc{kexinit} message.
%TODO How is the algorithm picked?
Subsequently, key exchange using the negotiated algorithm takes place. Following this algorithm, one-time session keys for encryption and hashing are generated by each side, together with an identifier for the session. The main key exchange algorithm is Diffie-Hellman, which is also the only one required by the RFC. For the Diffie-Hellman scheme, \textsc{kex30} and \textsc{kex31} are exchanged to establish fresh session keys. These keys are used from the moment the \textsc{newkeys} command has been issued by both parties. A subsequent \textsc{sr\_auth} requests the authentication service. The happy flow thus consists of the succession of the three steps comprising key exchange, followed up by a successful authentication service request. The sequence is shown in Figure~\ref{fig:hf-trans}.
\begin{figure}[!hb]
%\vspace{-1cm}
\includegraphics[scale=0.285]{hf-trans_cropped.pdf}
\caption{The happy flow for the Transport layer.}
\label{fig:hf-trans}
\vspace{-3mm}
\end{figure}
\textsl{Key re-exchange}~\cite[p. 23]{rfc4253}, or \textsl{rekeying}, is an almost identical process, the difference being that instead of taking place at the beginning, it takes place once session keys are already in place. The purpose is to renew session keys so as to foil potential replay attacks~\cite[p. 17]{rfc4251}. It follows the same steps as key exchange. A fundamental property of rekeying is that it should preserve the state; that is, after the rekeying procedure is completed, the protocol should be in the same state as
it was before the rekeying started, with as only difference that new keys are now in use. %Some implementations are known not support rekeying in certain states of the protocol.
%We consider an transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.
\subsection{Authentication layer}\label{ssh-run-auth}
Once a secure tunnel has been established, the client can authenticate. For this, four authentication methods are defined in RFC 4252~\cite{rfc4252}: password, public-key, host-based and none. The authentication request includes a user name, service name and authentication data, which consists of both the authentication method as well as the data needed to perform the actual authentication, such as the password or public key. The happy flow for this layer, as shown in Figure~\ref{fig:hf-auth}, is simply a single protocol step that results in a successful authentication. The messages \textsc{ua\_pw\_ok} and \textsc{ua\_pk\_ok} achieve this for respectively password and public key authentication.
%Figure~\ref{fig:hf-auth} presents the case for password authentication.
%We consider a user authentication layer state machine secure if there is no path from the unauthenticated state to the authenticated state without providing correct credentials.
\begin{figure}[!ht]
%\vspace{-1cm}
\includegraphics[scale=0.45]{hf-auth_cropped.pdf}
\caption{The happy flow for the user Authentication layer.}
\label{fig:hf-auth}
\vspace{-3mm}
\end{figure}
\subsection{Connection layer}\label{ssh-run-conn}
Successful authentication makes services of the Connection layer available. The Connection layer enables the user to open and close channels of various types, with each type providing access to specific services. Of the various services available, we focus on the remote terminal over a session channel, a classical use of SSH. The happy flow consists of opening a session channel, \textsc{ch\_open}, requesting a ``pseudo terminal'' \textsc{ch\_request\_pty}, optionally sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}, as depicted in Figure~\ref{fig:hf-conn}.
%\marginpar{\tiny Erik: to match this text, the figure should include a cycle
%for \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}??}
%Because the connection protocol offers a wide range of functionalities, we it is hard to define a single happy flow. Requesting a terminal is one of the main features of SSH and has therefore been selected as the happy flow. This behaviour is typically triggered by the trace \textsc{ch\_open}; \textsc{ch\_request\_pty}. Other
%Its hard to define which behaviour would result in a state machine security flaw in this layer. We will therefore take a more general approach and look at unexpected state machine transitions that can point towards potential implementation flaws.
%TODO Perhaps change this figure so to reflect text
\begin{figure}[!ht]
%\vspace{-1cm}
\includegraphics[scale=0.35]{hf-conn_cropped.pdf}
\caption{The happy flow for the Connection layer.}
\label{fig:hf-conn}
\vspace{-3mm}
\end{figure}
......@@ -24,7 +24,7 @@ At a high level, a typical SSH protocol run uses the three constituent protocols
%Different layers are identified by their message numbers. These message numbers will form the basis of the state fuzzing. The SSH protocol is especially interesting because outer layers do not encapsulate inner layers. This means that different layers can interact. One could argue that this is a less systematic approach, in which a programmer is more likely to make state machine-related errors.
\subsection{Transport layer}\label{ssh-run-trans}
\subsection{Transport Layer}\label{ssh-run-trans}
SSH runs over TCP, and provides end-to-end confidentiality and integrity using session keys. Once a TCP connection has been established with the server, these session keys are securely negotiated using a \textsl{key exchange} algorithm, the first step of the protocol. The key exchange begins by the two sides exchanging their preferences for the key exchange algorithm to be used, as well as encryption, compression and hashing algorithms. Preferences are sent with a \textsc{kexinit} message.
%TODO How is the algorithm picked?
Subsequently, key exchange using the negotiated algorithm takes place. Following this algorithm, one-time session keys for encryption and hashing are generated by each side, together with an identifier for the session. The main key exchange algorithm is Diffie-Hellman, which is also the only one required by the RFC. For the Diffie-Hellman scheme, \textsc{kex30} and \textsc{kex31} are exchanged to establish fresh session keys. These keys are used from the moment the \textsc{newkeys} command has been issued by both parties. A subsequent \textsc{sr\_auth} requests the authentication service. The happy flow thus consists of the succession of the three steps comprising key exchange, followed up by a successful authentication service request. The sequence is shown in Figure~\ref{fig:hf-trans}.
......@@ -43,7 +43,7 @@ it was before the rekeying started, with as only difference that new keys are no
%We consider an transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.
\subsection{Authentication layer}\label{ssh-run-auth}
\subsection{Authentication Layer}\label{ssh-run-auth}
Once a secure tunnel has been established, the client can authenticate. For this, four authentication methods are defined in RFC 4252~\cite{rfc4252}: password, public-key, host-based and none. The authentication request includes a user name, service name and authentication data, which consists of both the authentication method as well as the data needed to perform the actual authentication, such as the password or public key. The happy flow for this layer, as shown in Figure~\ref{fig:hf-auth}, is simply a single protocol step that results in a successful authentication. The messages \textsc{ua\_pw\_ok} and \textsc{ua\_pk\_ok} achieve this for respectively password and public key authentication.