Adding the LaTex sources of Patrick Verleg's master thesis

masterthesis_Patrick_Verleg/0-title.tex

+\title{Inferring SSH state machines using protocol state fuzzing}
+\date{}
+\author{Erik Poll\\ Radboud University \and Joeri de Ruiter\\ University of Birmingham \and Patrick Verleg\\ Radboud University}
+\maketitle

masterthesis_Patrick_Verleg/1-abstract.tex

+\begin{abstract}
+We describe the results of a technique called protocol state fuzzing, which is used to infer state machines for six SSH servers. Our results show that all tested SSH servers implement a secure state machine. However, implemented state machines differ significantly. These variances allow anyone to effectively fingerprint the tested servers.
+
+Various shortcomings whit 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. 
+
+If the SSH RFC authors would have sketched a state machine, we would expect the standards to be less ambiguous and implemented state machines to have fewer differences. In general, protocols in RFCs would benefit from added state information. We would generally encourage RFC authors to append a reference state machines to protocol specifications.
+\end{abstract}

masterthesis_Patrick_Verleg/2-introduction.tex

+\section{Introduction}\label{introduction}
+
+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 analyses found no serious issues~\cite{Williams2011Analysis}\cite{Paterson2010PlaintextDependent}. Academic researchers have so far focussed more on the theoretical aspects than on implementations of the protocol. 
+
+We have used fuzzing
+
+
+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. Results ranged from interesting insights to more serious implementational flaws.
+
+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}.

masterthesis_Patrick_Verleg/3-ssh.tex

+\section{Secure shell}\label{ssh} 
+The development of SSHv1 started in 1995 when Finnish researcher Tatu Ylönen drafted the first version of the software and its protocol at the Helsinki University of Technology. It was later standardized by the Internet Engineering Task Force, but quickly succeeded by SSHv2 because it contained design flaws~\cite{FutoranskyAttack} that could not be fixed without losing backwards compatibility. 
+
+SSH 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}
+
+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]{imgs/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]{imgs/hf-trans.pdf}
+  \caption{The happy flow for the transport layer.}
+  \label{fig:sshcomponents}
+\end{figure}
+
+\subsection{User authentication layer}\label{ssh-run-auth} 
+The RFC 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 queries \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]{imgs/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 involve opening and closing channels, requesting a process over that channel and sending data to a requested process. Because the connection protocol offers a wide range of functionalities, 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}. 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.
+
+\begin{figure}[!ht]
+  \includegraphics[width=0.5\textwidth]{imgs/hf-conn.pdf}
+  \caption{The happy flow for the connection layer.}
+  \label{fig:sshcomponents}
+\end{figure}
+

masterthesis_Patrick_Verleg/4-preliminaries.tex

+\chapter{Preliminaries}\label{preliminaries}
+This chapter covers background information about techniques, algorithms and formalisms relevant to this thesis. Different methods of state machine inference will be discussed in Section~\ref{prelim-infer}. Inferred state machines are represented as Mealy machines. The basic properties of Mealy machines are the subject of Section~\ref{mealymachines}. Section ~\ref{lstar} will cover the L* learning algorithm, the off-the-self algorithm used for inferring state machines. 
+
+\section{Inferring state machines}\label{prelim-infer}
+There are two fundamentally different ways in which state information can be derived for a certain protocol. In a passive approach, messages originating from two or more communicating systems are analysed to derive information. Since most protocols communicate over a network, these messages usually originate from network traffic. On the other hand, an active approach injects or alters messages to reveal protocol information. Both techniques can use learning algorithms to infer information, but the former has a focus on statistical methods to categorize messages, while the latter uses fuzzing.
+
+Both techniques have successfully been applied. The passive approach was used to extract state machines from real-world network traffic by making use of both package heads and body in~\cite{Wang2011Inferring}. This information was fed to a clustering algorithm, and its output was used to construct a state machine. The authors specifically mention that their inferred state machine might not include all transitions of the actual protocol's state machine. This is an observation that is true for any passive technique, since a clustering algorithm can only learn from traces that occur in the observed network traffic. Transitions that are not part of the collected traces can thus never be predicted. Another fundamental restriction to passively inferring state machines is the inability to learn protocols that communicate over an encrypted channel, at least without having access to the security keys. Encryption will mask the information needed to infer the state machine.
+
+These restrictions do not apply to active learning systems. Active learning approaches are less generic than passive learning systems. Since they need to take part in the protocol communication, some knowledge of the protocol is a prerequisite and therefore a tailor-made protocol participant has to be created. Encryption stresses the need for tailor-made systems even more. Firstly, because encryption prevents any automatic deduction of message format to use later on. Secondly, because encrypted systems have a natural protection against fuzzing, since the encryption-handling outer layers of a protocol will discard any message that is damaged or malformed~\cite{WheelerHow}. 
+
+In general, the more extensive the protocol, the more custom logic needs to be added to the fuzzer to successfully participate in the protocol's execution. In fact, it has been suggested that one of the reasons that the Heartbleed bug in OpenSSL's TLS implementation remained undiscovered for so long is due to the fact that only tailor-made fuzzers could be used~\cite{WheelerHow}. In this thesis, we will use a tailor-made fuzzer to actively participate in the protocol's execution. By fuzzing on the order of otherwise correctly-formed messages we will deduct a state machine, which will be represented as a Mealy machine.
+
+\section{Mealy machines}~\label{mealymachines}
+Mealy machines provide a representation for the internal state machine of an SSH implementation. We will refrain from covering all the available literature on Mealy machines, and instead discuss the necessary information needed for understanding the relevant representation restrictions and interpreting this thesis' results. For further reading, please refer to~\cite{Aarts2010Generating}, in which the relation between Mealy machines and inferring state machines is more thoroughly discussed and from which we will adopt terminology. 
+
+A Mealy machine can be represented as a tuple $\mathcal{M} = (I, O, Q, q_{0}, \delta, \lambda)$ in which $I$ and $O$ represent the input and output symbols, $Q$ is the set of states, with $q_{0}$ being the starting state. The two transition functions denoted by $\delta$ and $\lambda$ represent respectively the edges ($Q \times I \rightarrow Q$) and output ($Q \times I \rightarrow O$) with respect to a certain state and input. To spot logical flaws, a graphical representation is usually better-suited. Such a graphical representation typically depicts states as nodes and state transitions as edges. A Mealy machine for which $\lambda(q_{0}, i')=o'$ and $\delta(q_{0}, i')=q_{0}$ will therefore show an edge from $q_{0}$ to $q_{0}$ with label $i'/o'$, meaning that input $i'$ results in output $o'$ without changing the state. An example of a graphical representation for a simple Mealy machine is shown in Figure~\ref{fig:mealymachine}.
+
+
+\begin{figure}[!htb]
+  \noindent\makebox[\textwidth]{\includegraphics[width=0.6\textwidth]{imgs/example-mealy.pdf}}
+  \caption{A Mealy machine with three different states.}
+  \label{fig:mealymachine}
+\end{figure}
+
+A Mealy machine is a deterministic finite state transducer, implying it is both deterministic and finite. The transition functions therefore allow only a single output for a given state and input, and the number of input symbols and states is finite. Therefore, Mealy machines do not allow effective representation of infinitely large buffers in a protocol. Consider a state $q$ in which an input $i'$ always results in $o'$, but as soon as $i''$ is processed the SUT sends $o''$ once for each $i'$ that has been processed so far. A Mealy machine representation of this behaviour would need at least as many states as the (infinitely large) buffer. We will observe buffer-like behaviour in some SUTs. The adaptations made to still be able to model these SUTs as Mealy machines are described in Section~\ref{setup-handling}. 
+
+\section{L* learning algorithm}\label{lstar}
+The L* algorithm is used to build a model of the state machines and decide which queries need to be sent to a SUT. The usage of L* to infer state machines has first been demonstrated in~\cite{Pasareanu2008Learning}. In this thesis, we will use L* as an off-the-self algorithm and thus only briefly cover its properties. 
+
+Given a certain input alphabet, L* dictates which input to send to the SUT. The resulting output is used to infer states and decide which subsequent input symbols to send. Between the different traces, the SUT is reset to the initial state. In case of SSH, this is effectively done by terminating the connection and initiating a new one. 
+
+If the SUT's state machine is deterministic and finite, the algorithm produces a state machine hypothesis in a finite number of queries. The number of needed queries depend on the complexity of the state machine that is to be inferred. Unfortunately, neither the state machine's complexity nor its deterministic or finite properties are known beforehand. Running the algorithm on non-terminating or non-deterministic SUTs might result in non-termination of the L* implementation. In our testing setup, we automatically detect such cases (Section~\ref{challenging-nontermination}).
+
+As soon as a first hypothesis has been formed, it is passed to a testing oracle. This oracle will search for a counterexample. Since our testing-approach is black-box, no oracle algorithm can guarantee that existing counterexamples will be found in finite time. Section~\ref{components} describes the considerations for the selection of our oracle algorithm. 
+
+If the testing oracle finds a counterexample, the counterexample and hypothesis are used as a starting point for further learning. This process repeats until no more counterexamples are found. The final hypothesis is assumed to correctly define the SUT's minimal state machine~\cite[p. 12]{Pasareanu2008Learning}. 
\ No newline at end of file

masterthesis_Patrick_Verleg/7-conclusions.tex

+\chapter{Conclusions}\label{conclusions}
+In this thesis protocol state fuzzing was used to infer state machines for six SSH servers. Our setup (Chapter~\ref{setup}) uses a mapper to translate abstract queries from the learner to actual network packets that could be understood by an SSH server. Message numbers were used to convert response messages back to abstract representations. 
+
+Creating the mapper proved to be non-trivial. Handling non-determinism, non-termination and multiple responses were challenging (Section~\ref{setup-handling}). The mapper was extended with a trance and response log to detect non-determinism and improve performance. Delays were added to the mapper, as well as means to handle multiple responses to a single query and detect buffers within those responses. 
+
+All of the tested SUTs implement secure state machines (Chapter~\ref{results}). PowerShell and CiscoSSH do not support multiple channels (Section~\ref{results-conn}). Besides that, no incompatibilities were found. This does not mean that the inferred state machines show little difference. On the contrary: unresponsive and superfluous states, different interpretation of the RFCs, and unexplained quirks are the rule rather than the exception. In fact, only in the authentication layer did we find two identical state machines. These variances allow anyone to fingerprint the tested SUTs. 
+
+OpenSSH and Tectia implement a liberal message acceptance policy (Section~\ref{results-trans}). OpenSSH does not require a \textsc{kexinit} message from the client, and makes a guess on the used parameters. Tectia allows the three rekeying messages to arrive in arbitrary order. These liberal acceptance policies are unwise from a security perspective, since which they allow for state machine-related bugs which are easily introduced and hard to detect. CiscoSSH's state machines is the most restrictive, and closes the connection on any unexpected message.
+
+OpenSSH seems to contain a bug which leads to a terminated connection when closing a channel if a rekey has been performed earlier. Besides this bug, our results do not show that different protocol layers interact unexpectedly.
+
+The RFC for the connection layer provides relatively little state-related information (Section~\ref{results-rfcs}). Developers used this freedom of interpretation to implement state-machines which differ significantly. If the SSH RFC authors would had sketched a state machine, we would expect the standards to be less ambiguous and implemented state machines with fewer differences. Adding a reference state machine to the standards would definitely have added value for SSH. Most RFCs would benefit from added state information, and we would generally encourage authors to append a reference state machines to protocol specifications.
+
+\section{Future work}
+We had to make strict decisions on which messages we implemented to keep the learning times feasible. Although we aimed to pick messages that are most likely to produce interesting state-changing behaviour\footnote{An ``outgoing only'' message policy was used, as described in Section~\ref{trans-alphabet}.}, the alphabet could be further extended. Testing key exchange algorithms other than Diffie-Hellman is especially interesting in this regard. 
+
+The input alphabet can also be extended by fuzzing on message parameters. Some parameters were included (for example, the \textsc{guessinit} message is a \textsc{kexinit} with slightly altered parameters), but further extending parameter fuzzing might result in interesting behaviour. Extending the mapper to implement the wrong-guess procedure\footnote{Section~\ref{alphabet} provides more information on the \textsc{guessinit} message.} would also provide more information. 
+
+We limited the number of SUTs to six. Other frequently-used servers could be investigated as well. 
+
+Finally, a practical limitation of our setup is that it infers SSH's protocol layers individually. As a result, we cannot prove that there is no undetected, unwanted interaction between different layers. Trying more transport layer messages in higher layer could reveal unwanted interaction. A combined state machine for all three layers could also reveal more interesting interaction, although learning a combined machine would most likely need another experimental setup\footnote{The grounds for inferring the layers indivudally are covered in Section~\ref{layers-individual}.}.
\ No newline at end of file

masterthesis_Patrick_Verleg/MasterThesis.tex

+\documentclass[11pt,twocolumn,a4paper]{article}
+
+\usepackage{url}
+\usepackage[hidelinks]{hyperref}
+\usepackage[a4paper]{geometry}
+\usepackage[utf8]{inputenc}
+\usepackage{graphicx}
+
+% Table of content depth
+\setcounter{tocdepth}{1}
+
+\begin{document}
+\input{0-title}
+\input{1-abstract}
+\input{2-introduction}
+\input{3-ssh}
+%\input{4-preliminaries}
+%\input{5-setup}
+%\input{6-results}
+%\input{7-conclusions}
+
+\bibliographystyle{ieeetr}
+\bibliography{bibliography}
+
+%\appendix
+%\input{appendixa}
+%\input{appendixb}
+\end{document}
\ No newline at end of file

masterthesis_Patrick_Verleg/appendixa.tex

+\chapter{Message abbreviations}\label{appendixa}
+
+\begin{table}[!ht]
+\begin{tabular}{lll}
+\textbf{Abbreviation} & \textbf{RFC-defined name} & \textbf{Reference} \\
+\textsc{discon} & \textsc{ssh\_msg\_disconnect} & \cite[p. 23]{rfc4253} \\
+\textsc{ignore} & \textsc{ssh\_msg\_ignore} & \cite[p. 24]{rfc4253} \\
+\textsc{unimpl} & \textsc{ssh\_msg\_unimplemented} & \cite[p. 25]{rfc4253} \\
+\textsc{debug} & \textsc{ssh\_msg\_debug} & \cite[p. 25]{rfc4253} \\
+\textsc{kexinit} & \textsc{ssh\_msg\_kexinit} & \cite[p. 17]{rfc4253} \\
+\textsc{guessinit} & \textsc{ssh\_msg\_kexinit} & \cite[p. 19]{rfc4253} \\
+\textsc{kex30} & \textsc{ssh\_msg\_kexdh\_init} & \cite[p. 21]{rfc4253} \\
+\textsc{kex31} & \textsc{ssh\_msg\_kexdh\_reply} & \cite[p. 22]{rfc4253} \\
+\textsc{newkeys} & \textsc{ssh\_msg\_newkeys} & \cite[p. 21]{rfc4253} \\
+\textsc{sr\_auth} & \textsc{ssh\_msg\_service\_request} & \cite[p. 23]{rfc4253} \\
+\textsc{sr\_conn} & \textsc{ssh\_msg\_service\_request} & \cite[p. 23]{rfc4253} \\
+\textsc{accept} & \textsc{ssh\_msg\_service\_accept} & \cite[p. 25]{rfc4253} \\
+\end{tabular}
+\caption{Message abbreviations for the transport layer.}
+\label{apendix-alphabet-trans}
+\end{table}
+
+\begin{table}[!th]
+\begin{tabular}{lll}
+\textbf{Abbreviation} & \textbf{RFC-defined name} & \textbf{Reference} \\
+\textsc{ua\_none} & \textsc{ssh\_msg\_userauth\_request} & \cite[p. 7]{rfc4252} \\
+\textsc{ua\_pk\_ok} & \textsc{ssh\_msg\_userauth\_request} & \cite[p. 8]{rfc4252} \\
+\textsc{ua\_pk\_nok} & \textsc{ssh\_msg\_userauth\_request} & \cite[p. 8]{rfc4252} \\
+\textsc{ua\_pw\_ok} & \textsc{ssh\_msg\_userauth\_request} & \cite[p. 10]{rfc4252} \\
+\textsc{ua\_pw\_nok} & \textsc{ssh\_msg\_userauth\_request} & \cite[p. 10]{rfc4252} \\
+\textsc{ua\_success} & \textsc{ssh\_msg\_userauth\_success} & \cite[p. 6]{rfc4252} \\
+\textsc{ua\_failure} & \textsc{ssh\_msg\_userauth\_failure} & \cite[p. 5]{rfc4252} \\
+\end{tabular}
+\caption{Message abbreviations for the user authentication layer.}
+\label{apendix-alphabet-auth}
+\end{table}
+
+\begin{table}[!ht]
+\begin{tabular}{lll}
+\textbf{Abbreviation} & \textbf{RFC-defined name} & \textbf{Reference} \\
+\textsc{ch\_open} & \textsc{ssh\_msg\_channel\_open} & \cite[p. 5]{rfc4254} \\
+\textsc{ch\_close} & \textsc{ssh\_msg\_channel\_close} & \cite[p. 9]{rfc4254} \\
+\textsc{ch\_eof} & \textsc{ssh\_msg\_channel\_eof} & \cite[p. 9]{rfc4254} \\
+\textsc{ch\_data} & \textsc{ssh\_msg\_channel\_data} & \cite[p. 7]{rfc4254} \\
+\textsc{ch\_edata} & \textsc{ssh\_msg\_channel\_extended\_data} & \cite[p. 8]{rfc4254} \\
+\textsc{ch\_window\_adjust} & \textsc{ssh\_msg\_channel\_window\_adjust} & \cite[p. 7]{rfc4254} \\
+\textsc{ch\_request\_pty} & \textsc{ssh\_msg\_channel\_request\_pty} & \cite[p. 11]{rfc4254} \\
+\textsc{ch\_success} & \textsc{ssh\_msg\_channel\_success} & \cite[p. 4]{rfc4254} \\
+\end{tabular}
+\caption{Message abbreviations for the connection layer.}
+\label{apendix-alphabet}
+\end{table}
\ No newline at end of file

masterthesis_Patrick_Verleg/appendixb.tex

+\chapter{State machine formatting}\label{appendixb}
+This appendix shows the formatting process applied to CiscoSSH's transport layer state machine. \\
+
+\begin{figure}[!ht]
+  \noindent\makebox[\textwidth]{\includegraphics[width=1.25\textwidth]{imgs/appendixb_unformatted.pdf}}
+  \caption{Unformatted state machine.}
+  \label{fig:appendixb-unformatted}
+\end{figure}
+
+\begin{figure}[!ht]
+  \noindent\makebox[\textwidth]{\includegraphics[width=0.8\textwidth]{imgs/appendixb_auto.pdf}}
+  \caption{State machine after merging edges between same nodes.}
+  \label{fig:appendixb-auto}
+\end{figure}
+
+\begin{figure}[!ht]
+  \noindent\makebox[\textwidth]{\includegraphics[width=0.6\textwidth]{imgs/appendixb_manual.pdf}}
+  \caption{State machine after manually applying conventions from Section~\ref{visualisation}.}
+  \label{fig:appendixb-manual}
+\end{figure}
\ No newline at end of file