the_sut.tex 5.46 KB
 Paul Fiterau Brostean committed Jan 20, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 \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  Paul Fiterau Brostean committed Feb 01, 2017 17  \includegraphics[width=0.65\linewidth]{SSH_protocols.png}  Paul Fiterau Brostean committed Jan 20, 2017 18 19 20 21 22 23 24 25 26 27 28 29 30 31  \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}  Paul Fiterau Brostean committed Jan 29, 2017 32 RFC 4252~\cite{rfc4252} defines four authentication methods (password, public-key, host-based and none). 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.  Paul Fiterau Brostean committed Jan 20, 2017 33 34 35 36 37 38 39 40 %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}  Paul Fiterau Brostean committed Jan 29, 2017 41 42 43  \subsection{Connection protocol}\label{ssh-run-conn}  Paul Fiterau Brostean committed Jan 20, 2017 44 45 46 47 48 49 50 51 52 53 54 55 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}