the_sut.tex 8.23 KB
 Paul Fiterau Brostean committed Jan 20, 2017 1 2 \section{The Secure Shell Protocol} \label{sec:ssh}  Joeri committed Feb 16, 2017 3 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.  Paul Fiterau Brostean committed Jan 20, 2017 4   Erik Poll committed Feb 15, 2017 5 6 SSHv2 follows a client-server paradigm. The protocol consists of three layers (Figure~\ref{fig:sshcomponents}): \begin{enumerate}  7 \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.  Paul Fiterau Brostean committed Jan 20, 2017 8 \item The \textit{user authentication protocol} (RFC 4252~\cite{rfc4252}) is used to authenticate the client to the server.  Joeri committed Feb 16, 2017 9 \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.  Erik Poll committed Feb 15, 2017 10 \end{enumerate}  Paul Fiterau Brostean committed Jan 20, 2017 11   Erik Poll committed Feb 17, 2017 12 13 \begin{figure}[t] % was !hb \centering  Paul Fiterau Brostean committed Feb 17, 2017 14  \includegraphics[scale=0.20]{SSH_protocols.png}  Erik Poll committed Feb 17, 2017 15 16  \caption{SSH protocol layers} \label{fig:sshcomponents}  Paul Fiterau Brostean committed Feb 17, 2017 17  \vspace{-3mm}  Erik Poll committed Feb 17, 2017 18 19 20 \end{figure}  Erik Poll committed Feb 17, 2017 21 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 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 characterising the so-called \textit{happy flow} that a normal protocol  Erik Poll committed Feb 15, 2017 22 run follows.  23   Paul Fiterau Brostean committed Feb 18, 2017 24 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.  Paul Fiterau Brostean committed Feb 08, 2017 25   Paul Fiterau Brostean committed Jan 20, 2017 26 27 28 %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}  Joeri committed Feb 16, 2017 29 30 31 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}.  Paul Fiterau Brostean committed Jan 20, 2017 32   Erik Poll committed Feb 17, 2017 33 \begin{figure}[!hb]  Paul Fiterau Brostean committed Feb 17, 2017 34 35 %\vspace{-1cm} \includegraphics[scale=0.285]{hf-trans_cropped.pdf}  Paul Fiterau Brostean committed Feb 18, 2017 36  \caption{The happy flow for the Transport layer.}  37  \label{fig:hf-trans}  Paul Fiterau Brostean committed Feb 17, 2017 38  \vspace{-3mm}  Paul Fiterau Brostean committed Jan 20, 2017 39 40 \end{figure}  Erik Poll committed Feb 17, 2017 41 \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  Erik Poll committed Feb 15, 2017 42 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.  Paul Fiterau Brostean committed Feb 08, 2017 43 44 45 46 47  %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}  Erik Poll committed Feb 15, 2017 48   Paul Fiterau Brostean committed Feb 18, 2017 49 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.  Joeri committed Feb 16, 2017 50 %Figure~\ref{fig:hf-auth} presents the case for password authentication.  Paul Fiterau Brostean committed Jan 20, 2017 51 52 53 %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]  Paul Fiterau Brostean committed Feb 17, 2017 54 55 %\vspace{-1cm} \includegraphics[scale=0.45]{hf-auth_cropped.pdf}  Paul Fiterau Brostean committed Feb 18, 2017 56  \caption{The happy flow for the user Authentication layer.}  57  \label{fig:hf-auth}  Paul Fiterau Brostean committed Feb 17, 2017 58  \vspace{-3mm}  Paul Fiterau Brostean committed Jan 20, 2017 59 60 \end{figure}  Paul Fiterau Brostean committed Jan 29, 2017 61 62   Paul Fiterau Brostean committed Feb 08, 2017 63 \subsection{Connection layer}\label{ssh-run-conn}  Paul Fiterau Brostean committed Feb 18, 2017 64 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}.  Paul Fiterau Brostean committed Feb 16, 2017 65 66 %\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}??}  Paul Fiterau Brostean committed Jan 20, 2017 67 68 69 70 71 72 73  %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]  Paul Fiterau Brostean committed Feb 17, 2017 74 75 %\vspace{-1cm} \includegraphics[scale=0.35]{hf-conn_cropped.pdf}  Paul Fiterau Brostean committed Feb 18, 2017 76  \caption{The happy flow for the Connection layer.}  77  \label{fig:hf-conn}  Paul Fiterau Brostean committed Feb 17, 2017 78  \vspace{-3mm}  Erik Poll committed Feb 15, 2017 79 \end{figure}