Skip to content

GitLab

Commit 03dbe5e1 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Some more .tex plus (rather empty) spec document

parent 0a1d1c31
Expand all Hide whitespace changes
Inline Side-by-side
ACM-Reference-Format.bst 0 → 100644
View file @ 03dbe5e1
This diff is collapsed.
images/logo.eps 0 → 100644
View file @ 03dbe5e1
This diff is collapsed.
introduction.tex
View file @ 03dbe5e1
......@@ -2,15 +2,19 @@
The SSH protocol is used interact securely with remote machines. Alongside TLS and IPSec, SSH is amongst the most frequently used security suites~\cite{Albrecht2009Plaintext}. Due to its significant user base and sensitive nature, flaws in the protocol or its implementation could have major impact. It therefore comes as no surprise that SSH has attracted scrutiny from the security community. Problems with information leakage via unencrypted MACs were identified~\cite{Bellare2004Breaking}, as well as possibilities for plain text recovery when a block cipher in cipher block chaining mode was used~\cite{Albrecht2009Plaintext}. Other analysis found no serious issues~\cite{Williams2011Analysis}\cite{Paterson2010PlaintextDependent}. Academic researchers have so far focused more on the theoretical aspects than on implementations of the protocol.
In this work, we use model learning to infer state machines of 3 SSH implementations. Model learning 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}. More recently, it was used to learn implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol}. Model learning's goal is obtaining (or learning) a state model of a black-box system by providing inputs and observing outputs. The learned state model corresponds to the observed behavior, and can be used in system analysis. Since model learning builds from a finite number of observations, we can never be sure that the learned model is correct. To that end, advanced conformance algorithms are employed, which yield some confidence that the system inferred is in fact correct. In the context of testing protocols, model learning can be seen as a form of protocol state fuzzing, whereby unexpected inputs are sent to a system under test in the hope of exposing hidden anomalies. In model learning, inputs are sent with no regard to the order imposed by the protocol.
In this work, we use classical active automata learning, which we refer to as model learning, to infer state machines of 3 SSH implementations. Model learning 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}. More recently, it was used to learn implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol}. Model learning's goal is obtaining a state model of a black-box system by providing inputs and observing outputs. The learned state model corresponds to the observed behavior, and can be used in system analysis. Since model learning builds from a finite number of observations, we can never be sure that the learned model is correct. To that end, advanced conformance algorithms are employed, which yield some confidence that the system inferred is in fact correct. In the context of testing protocols, model learning can be seen as a form of protocol state fuzzing, whereby unexpected inputs are sent to a system under test in the hope of exposing hidden anomalies. In model learning, inputs are sent with no regard to the order imposed by the protocol.
Inputs can therefore be sent disorderly. Any anomalies are then exposed in the learned model.
Having obtained models, we use model checkers to automatically verify their conformance to security properties. Such verification would be difficult manually, as the learned models are large. Moreover, the very satisfaction of properties can be used to refine the learned model. In cases where the learned model does not satisfy a security property, the proving sequence of inputs can either signal non-conformance of the system, or can be used to further refine the learned model.
Our work most closely resembles work on TCP~\cite{Janssen2015Learning}, where they also combine learning and model checking to analyze
Our work most closely resembles work on TCP~\cite{Janssen2015Learning}, 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 rely on
manual analysis of the learned models ~\cite{Aarts2013Formal},\cite{Chalupar2014Automated},\cite{Aarts2013Formal}. Our work differs, since we use a model checker to automatically check formalized
specifications. Moreover, the model checker is also used as means of testing the learned model.
manual analysis of the learned models ~\cite{Aarts2013Formal},\cite{Chalupar2014Automated}, \cite{RuiterProtocol}. Our work differs,
since we use a model checker to automatically check specifications. Moreover, the model checker is also used as means of testing the learned model.
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. Such 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.
%Model checkers provide for an automatic way of verifying properties.
......
learning_setup.tex 0 → 100644
View file @ 03dbe5e1
This diff is collapsed.
macros.tex 0 → 100644
View file @ 03dbe5e1
% 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
%
\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}*}
\newcommand{\dlearner}{\term{learner}\xspace}
\newcommand{\dmapper}{\term{mapper}\xspace}
\newcommand{\dsut}{{\sc sul}\xspace}
\ No newline at end of file
preliminaries.tex
View file @ 03dbe5e1
\section{Model learning background}
\subsection{Mealy machines} \label{mealy machines}
We use \textit{Mealy machines} to represent the state machine of SSH implementations. A Mealy machine is a a 6-tuple $\mathcal{M} = (Q, q_0, I, O, \delta, \lambda)$, where:
\begin{itemize}
\item $Q$ is the set of states.
\item $q_0 \in Q$ is the initial state.
\item $I$ is the input alphabet.
\item $O$ is the output alphabet.
\item $\delta$ is the transition function $Q \times I \rightarrow Q$, which gives the resulting state from sending a certain input when in a certain state.
\item $\lambda$ is the transition function $Q \times I \rightarrow O$, which gives the received output when sending a certain input from a certain state.
\end{itemize}
A Mealy machine is deterministic, if for each state and input I, there exists
Mealy machines can be graphically represented as a graph. States are shown as nodes and state transitions as edges. Edges are labeled as ``$<input>/<output>$'' corresponding to the transition functions: If $\delta(q_0, A) = q_1$ and $\lambda(q_0, A) = X$ then the label for the edge between $q_0$ and $q_1$ will be ``$A/X$''. An example visualization for a Mealy machine is shown in figure \ref{mealy example}.
\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$};
\section{Model learning background}\label{sec:prelims}
\subsection{Mealy machines} \label{ssec:mealy}
We use \textit{Mealy machines} to represent the state machine of SSH implementations. A Mealy machine is a a 5-tuple $\mathcal{M} = (Q, q_0, I, O, \rightarrow \rangle)$, where
$I$, $O$ and $Q$ are finite sets of \emph{inputs}, \emph{outputs} and \emph{states}, $q_0 \in Q$ is the initial state, and $\rightarrow \subseteq Q \times I \times O \times Q$
is the \emph{transition relation}. We say $q \xrightarrow{i/o} q'$ if $(q, i, o, q') \in \rightarrow$.
\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}
A Mealy machine $\mathcal{M}$ is \emph{input enabled} if for each state $q$ and input $i$, there is a transition $q \xrightarrow{i/o} q'$, for some $o$ and $q'$. Additionally,
a Mealy machine is said to be \emph{deterministic} if there is at most one such transition defined. In our setting, we restrict our representations of systems to Mealy machines that are both
input enabled and deterministic.
\subsection{Learning state machines} \label{learning}
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.
%\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}
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.
\subsection{MAT Framework} \label{ssec:mat}
The most efficient algorithms for model learning all follow
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Ang87}.
In the MAT framework, learning is viewed as a game in which a learner has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a deterministic Mealy machine $\M$.
Initially, the learner only knows the inputs $I$ and outputs $O$ of $\M$.
The task of the learner is to learn $\M$ through two types of queries:
\begin{itemize}
\item
With a \emph{membership query}, the learner 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 learner 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}
\begin{figure}[h]
\centering
\includegraphics[scale=0.8]{Naamloos.png}
\caption{A learning setup}
\label{learning setup}
\end{figure}
Model learning algorithms have been developed developed for learning deterministic Mealy machines using
a finite number of queries. We point to \cite{Isberner2015} for a recent overview. These algorithms are leveraged
in applications where one wants to learn a model of a black-box reactive system, or System Under Learning (\dsut). The teacher typically
consists of the ~\dsut, which answers 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.
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{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 mapper is a transducer which translates
concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough definition of mappers, we refer to \cite{AJUV15}.
\subsection{Secure Shell} \label{secure shell}
%Perhaps some explanation
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.
%
%
%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}
\ No newline at end of file
specifications.txt 0 → 100644
View file @ 03dbe5e1
Here we add specifications that might be model checked.
SSH_MSG_CHANNEL_CLOSE
Connection Layer:
Upon receiving this message, a party MUST
send back an SSH_MSG_CHANNEL_CLOSE unless it has already sent this
message for the channel. The channel is considered closed for a
party when it has both sent and received SSH_MSG_CHANNEL_CLOSE, and
the party may then reuse the channel number. A party MAY send
SSH_MSG_CHANNEL_CLOSE without having sent or received
SSH_MSG_CHANNEL_EOF.
\ No newline at end of file
the_sut.tex 0 → 100644
View file @ 03dbe5e1
\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. The initial version of the protocol was superseded by a second version (SSHv2), as the former was found to contain design flaws~\cite{FutoranskyAttack} which could not be fixed without losing backwards compatibility. This work focuses on SSHv2.
SSHv2 follows a client-server paradigm consisting of three components (Figure~\ref{fig:sshcomponents}):
\begin{itemize}
\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 processes, such as terminal emulation or file transfer, over a single SSH connection.
\end{itemize}
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers. This means that different layers can interact. Hence, it makes sense to learn SSH as a whole, instead of analyzing its constituent layers independently. We review the happy flow for each layer, outlining the relevant messages which are later used in learning.
%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.
\begin{figure}[!hb]
\centering
\includegraphics[width=0.85\linewidth]{SSH_protocols.png}
\caption{SSH protocol components running on a TCP/IP stack.}
\label{fig:sshcomponents}
\end{figure}
\subsection{Transport layer}\label{ssh-run-trans}
SSH provides end-to-end encryption based on pseudo-random keys which are securely negotiated during key exchange. The negotiation begins with the \textsc{kexinit} message, which exchanges the preferences for negotiable parameters. Subsequently, the actual key exchange using the negotiated algorithm takes place, using \textsc{kex30} and \textsc{kex31} messages using Diffie-Hellman as negotiated key exchange algorithm. The 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. %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.
\begin{figure}[!hb]
\includegraphics[width=0.5\textwidth]{hf-trans.pdf}
\caption{The happy flow for the transport layer.}
\label{fig:sshcomponents}
\end{figure}
\subsection{User authentication layer}\label{ssh-run-auth}
RFC 4252~\cite{rfc4252} defines four authentication methods (password, public-key, host-based and none), which are all sent using the same message number~\cite[p. 8]{rfc4252}. The authentication request includes a user name, service name and authentication data, which includes both the authentication method as well as the data needed to perform the actual authentication, such the password or public key. The happy flow for this layer is defined as the sequence that results in a successful authentication. The messages \textsc{ua\_pw\_ok} and \textsc{ua\_pk\_ok} achieve this for respectively password or public key 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]
\includegraphics[width=0.5\textwidth]{hf-auth.pdf}
\caption{The happy flow for the user authentication layer.}
\label{fig:sshcomponents}
\end{figure}
\subsubsection{Connection protocol}\label{ssh-run-conn}
The connection protocol's requests may opening and closing channels of different types, with each type providing access to specific services. From the various services available, we focus on the remote terminal over a session channel, a standout feature of SSH. A happy flow would involve opening a session channel, \textsc{ch\_open}, requesting a terminal \textsc{ch\_request\_pty}, sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_adj\_win}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}.
%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]
\includegraphics[width=0.5\textwidth]{hf-conn.pdf}
\caption{The happy flow for the connection layer.}
\label{fig:sshcomponents}
\end{figure}
\ No newline at end of file
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