Commit 51fc5a5b authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Pushed updated files

parent 18c8f0fb
......@@ -8,7 +8,7 @@ Having obtained models, we use model checking to automatically verify their conf
Our work is borne out of 2 recent theses \cite{Verleg2016}, \cite{Toon2016}. It 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{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.
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.
......
......@@ -3,8 +3,11 @@
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
We use the NuSMV model checker to verify security properties. NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function, which can then be defined to change these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a certain specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
We use the NuSMV model checker to verify security properties. NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function which makes changes on these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a certain specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
In this section, we define the properties that we formalized and verified with the NuSMV model checker. We group these properties into three categories:
\begin{enumerate}
\item \textit{general security properties}, that is properties which must hold if the implementation is to be deemed secure
\item \textit{key exchange properties}, that is properties regarding the key exchange operation
......@@ -15,7 +18,7 @@ In this section, we define the properties that we formalized and verified with t
Both the Transport and the Authentication Layers can be said to provide notions of security, which secure access to services of the Connection Layer. For each of these layers, we define general security properties that reflect successful implementation of these notions.
%Each upper SSH layer assumes a notion of security is provided by the layer bellow. The Authentication Layer assumes integrity and confidentiality is provided by the Transport Layer, the Connection Layer the same assumptions, plus it also assumes authentication was successful. We define a general property for each upper layer on the basis of successful implementation of these security notions.
The security property for the Transport layer is defined as follows: ``We consider a 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.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell a authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input SERVICE\_REQUEST\_AUTH, the output SERVICE\_ACCEPT was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
The security property for the Transport layer is defined as follows: ``We consider a 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.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell an authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input SERVICE\_REQUEST\_AUTH, the output SERVICE\_ACCEPT was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -42,15 +45,46 @@ G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS) ->
\end{property}
\subsection{Key exchange properties}
Important properties are that (re-)exchanging keys is allowed in all states of the protocol, and its successful execution doesn't change the protocol state. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These map to multiple states in the learned models. For each state, we specify the properties that performing key exchange (1) should always be allowed from that state, and (2) if allowed, should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a \emph{disconnect} action from either side. These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we noted great variance on satisfaction of these properties.
Important properties are that re-exchanging keys is allowed in all states of the protocol, and its successful execution doesn't change the protocol state\cite[p. 24]{rfc4254}. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These map to multiple states in the learned models. For each state, we specify the properties that performing key exchange (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a \emph{disconnect} action from either side. We can tell we are in one of these states from the input/output transition leading up to it.
These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we note great variance on satisfaction of these properties.
In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request. Once here, performing the inputs for key re-exchange in succession should imply success. Provided we perform successful finalization of a re-key, we remain in a pre-authenticated state until we exit this state on a \textsc{disconnect} from either side, or via a successful authentication (\textsc{ua\_success}. The latter is described in Property~\ref{prop:prop3}. Note that, we can tell of being in a pre-authenticated state, if authenticating with a valid public key implies success. WU represents the Weak Until operator.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (input= SERVICE_REQUEST & output= SERVICE_ACCEPT) ->
( ( input = NEWKEYS & output = NO_RESP & X ( input = UA_PK_OK ) ) ->
X ( output=UA_SUCCESS) ) WU (input = DISCONNECT | output= DISCONNECT | output= UA_SUCCESS)
\end{lstlisting}
\caption{Key exchange preserves pre-authenticated state}
\label{prop:prop3}
\end{property}
\subsection{Other functional properties}
We have also formalized and checked properties drawn from the RFC specifications. A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a KEXINIT message, a party MUST not send SERVICE\_REQUEST or SERVICE\_ACCEPT messages, until it has sent a NEWKEYS message. This is translated to the LTL.
We have also formalized and checked properties drawn from the RFC specifications. We found the specification vague, which sometimes meant we had to make certain assumptions in order to formalize properly.
The RFC states in~\ref[p. 24]{rfc4254} that after sending a \textsc{kexinit} message, a party MUST not send another \textsc{kexinit}, or a \textsc{service\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:prop4}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (output = KEXINIT) ->
X (output != SERVICE_ACCEPT & output != KEXINIT)
WU X (output = NEWKEYS | output = KEX31_NEWKEYS ) )
\end{lstlisting}
\caption{Allowed outputs after KEXINIT}
\label{prop:prop4}
\end{property}
On the same page, it is stated that if ``the server rejects the service request, it SHOULD send an appropriate SSH_MSG_DISCONNECT message and MUST disconnect''. Moreover, in case it supports the service request, it MUST send a \textsl{service\_accept} message. Unfortunately, it is not evident from the specification if rejection and support are the only allowed outcomes. We assume that is the case, and formalize an LTL formula accordingly, with the adjustment that we also allow the output \textsl{no\_conn}, suggesting there is no connection. Of course, if there is no connection, the server cannot possibly reply.
The RFC for the Authentication Layer states that if the server rejects the authentication request, it MUST respond with a \textsl{ua\_failure} message. Conversely, if the requests succeeds, an \textsl{ua\_success} MUST be sent only once. Further authentication requests received thereafter SHOULD be ignored. While not explicitly stated, we assume this to be in a context where the authentication service had been requested. Indeed, outside of this state, implementations replied with \textsl{unimplemented}.
A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a \textsl{kexinit} message, a party MUST not send \textsl{service\_request} or \textsl{service\_accept} messages, until it has sent a \textsl{newkeys} message. This is translated to the LTL.
The RFC also states that in case the server rejects a service request, it should send an appropriate DISCONNECT message.
On the same page, the RFC also states that in case the server rejects a service request, it should send an appropriate \textsl{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsl{service\_accept} message. If
The Connection Layer RFC states that upon receiving a CH\_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH\_CLOSE would no longer have to be issued.
%The Connection Layer RFC states that upon receiving a CH_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH_CLOSE would no longer have to be issued.
\subsection{Model checking results}
Table presents the model checking results. Crucially, all general security properties are met, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.
......@@ -14,7 +14,7 @@ Each layer has its own specific messages. The SSH protocol is interesting in th
\begin{figure}[!hb]
\centering
\includegraphics[width=0.85\linewidth]{SSH_protocols.png}
\includegraphics[width=0.65\linewidth]{SSH_protocols.png}
\caption{SSH protocol components running on a TCP/IP stack.}
\label{fig:sshcomponents}
\end{figure}
......
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