Commit 0748ffda authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated definitions. (Model checking incomplete)

parent b2361dca
......@@ -44,8 +44,7 @@ We then ran an exhaustive test suite with {\dk} of 2 for all implementations.
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing, namely:
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis.
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models along with the specifications checked can be found at~\cite{SSHResults}.
%BitVise: MemQ: 24996 TestQ: 58423
%Dropbear: MemQ: 3561 TestQ: 30629
%OpenSSH: MemQ: 19836 TestQ: 76418
......@@ -75,7 +74,7 @@ is possible . A considerable number of states were also added due to {\dmapper}
Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with various changes applied to improve readability. The happy flow, contoured in green, is fully explored in the model and mostly matches our earlier description of it\footnote{The only exception is in the transport layer, where unlike in our happy flow definition, the server is the first to send the \textsc{newkeys} message. This is also accepted behavior, as the protocol does not specify which side should send \textsc{newkeys} first.}. Also explored is what happens when a rekey sequence is attempted. We notice that rekey is only allowed in states of the Connection layer. Strangely, for these states, rekey is not state preserving, as the generated output on receiving a \textsc{sr\_auth}, \textsc{sr\_conn} or \textsc{kex30} changes from \textsc{unimpl} to \textsc{no\_resp}. This leads to two sub-clusters of states, one before the first rekey, the other afterward. In all other states, the first step of a rekey (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect.
We also found strange how systems reacted to \textsc{sr\_conn}, request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of an explicit service request. That in itself was not strange, because authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
What was strange was that, making this explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of \textsc{BitVise}. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected on requesting this service. Only \textsc{DropBear} seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
What was strange was that, making this explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected on requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
We also notice the intricate authentication behavior, it seems that password authentication is the only form that allows you to authenticate after an unsuccessful attempt. Finally, of all implementations tested, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior.
......
......@@ -43,7 +43,7 @@ the messages \textsc{service\_accept}, \textsc{ua\_accept},
\textsc{ch\_failure} from our alphabet.} Furthermore, from the
Connection layer we only use messages for channel management and the
terminal functionality. Finally, because we will only explore
protocol behaviour after SSH versions have been exchanged, we exclude
protocol behavior after SSH versions have been exchanged, we exclude
these messages for exchanging version numbers.
%\marginpar{\tiny Erik: I
%rephrased all this to make it simpler. Is it still ok?}
......@@ -128,7 +128,7 @@ The restricted alphabet only supports the most general channel management inputs
%table
\subsection{The mapper}
\subsection{The mapper}\label{subsec:mapper}
The {\dmapper} must provide a translation between abstract messages
and well-formed SSH messages: it has to translate abstract inputs
......
\section{Security specifications} \label{sec:specs}
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
%\newfloat{property}{thp}{lop}
%\floatname{property}{Property}
\newtheorem{property}[theorem]{Property}
The size models of the models makes them difficult to manually inspect and verify against specifications. Manual analysis is further complicated by the ambiguity present in textual specifications.
Hence it makes sense to (1) formalize specification so as to eliminate ambiguity and (2) use model checking to verify the specifications automatically. To these ends, we use the NuSMV model checker to verify security properties for the learned models, properties which we formalize using LTL formulas.
......@@ -44,7 +46,7 @@ This function updates the output and state variables for a given valuation of th
\end{tikzpicture}
%\end{subfigure}
\\
\small
\footnotesize
\begin{lstlisting}
MODULE main
VAR state : {q0, q1};
......@@ -87,6 +89,7 @@ A key note is that properties are checked not on the actual concrete model of th
\newcommand{\dopchan}{$hasOpenedChannel$}
Before introducing the properties, we mention some basic predicates and conventions we use in their definition. The happy flow in SSH consists in a series of steps, the user first exchanges keys, then requests for the authentication service, followed up by supplying valid credentials and authentication, concluded by opening of a channel. Whereas the first step is complex, the subsequent steps can be captured by the simple predicates {\dreqauth} , {\dauth} and {\dopchan} respectively. The predicates are defined in terms of the output generated at a given moment, with certain values of this output indicating that the step was performed successfully. For example, \textsc{ch\_open\_success} indicates that a channel has been opened successfully. Sometimes, we also need the input that generated the output, in order to distinguish this step from a different step. In particular, requesting the authentication service is distinguished from requesting the connection service by \textsc{sr\_auth}.
To these predicates, we add predicates for valid, invalid and all. % authentication methods, and a predicate
\begin{center}
\begin{lstlisting}[basicstyle=\footnotesize]
hasReqAuth := inp=SR_AUTH & out=SR_ACCEPT
......@@ -113,7 +116,7 @@ a connection is lost is suggested by generation of the \textsc{no\_conn} output.
G (out=NO_CONN ->
G (out=NO_CONN | out=CH_MAX | out=CH_NONE) )
\end{lstlisting}
\caption{One connection property}
%\caption{One connection property}
\label{prop:noconn}
\end{property}
......@@ -128,7 +131,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
X ( (inp=CH_CLOSE -> out=CH_NONE)
W (inp=CH_OPEN & out!=CH_MAX) ) )
\end{lstlisting}
\caption{Mapper induced channel property}
%\caption{Mapper induced channel property}
\label{prop:channel}
\end{property}
......@@ -143,14 +146,14 @@ Key exchange implies three steps which have to be performed in order but may be
% SR_ACCEPT -> SR_ACCEPT
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasReqAuth ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
\end{lstlisting}
\caption{Transport layer security}
%\caption{Transport layer security}
\label{prop:sec-trans}
\end{property}
......@@ -158,43 +161,42 @@ Apart from a secure connection, Connection layer services also assume that the c
Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$ held in all times $t''$ such that $t' < t'' \leq t$.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasOpenedChannel ->
out!=UA_FAILURE S out=UA_SUCCESS )
\end{lstlisting}
\caption{Authentication layer security}
%\caption{Authentication layer security}
\label{prop:sec-auth}
\end{property}
\subsection{Key re-exchange properties}
Important properties are that re-exchanging keys (or rekey-ing) 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 may map to multiple states in the learned models. For each state, we can specify the properties that rekey-ing (1) should always be possible, and (2) if possible, should always preserve the state, until connection is lost. We can tell each rekey step was successful by the generated response. %There is no feasible way of describing that a state was preserved, but we can again use input and output
These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we note great variance on satisfaction of these properties.
Important properties are that re-exchanging keys (or rekey-ing) is (1) preferably is allowed in all states of the protocol, and (2) its successful execution doesn't affect operation of the higher layers\cite[p. 24]{rfc4254}. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These may map to multiple states in the learned models.
In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request, indicated by the predicate {\dreqauth}. Once here, performing the inputs for rekey in succession should imply success. This is shown in Property~\ref{prop:rpos-pre-auth}.
\begin{property}[h]
(1) can be easily formalized in LTL, (2) cannot, as you cannot express in a general way that two states are equivalent, without pointing to the states in the model, which we want to avoid. We then check this by a simple script which for each state allowing rekey, checks if the state reached after a successful rekey is equivalent when only analyzing higher layer inputs. For (1) we formalize two properties, one for each general state. In the case of the pre-authenticated state, we know we have reached this state following a successful authentication service request, indicated by the predicate {\dreqauth}. Once here, performing the inputs for rekey in succession should imply success. This is shown in Property~\ref{prop:rpos-pre-auth}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasReqAuth ->
X (inp=KEXINIT -> out=KEXINIT &
X (inp=KEX30 -> out=KEX31_NEWKEYS &
X (inp=NEWKEYS -> out=NO_RESP) ) ) )
\end{lstlisting}
\caption{Rekey possible in pre-auth. state}
%\caption{Rekey possible in pre-auth. state}
\label{prop:rpos-pre-auth}
\end{property}
Provided we perform successful finalization of a rekey, we remain in a pre-authenticated state until we exit this state, either by losing the connection (suggested by the \textsc{no\_conn} ) or by successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:rper-pre-auth}. Note that, we can tell we are in a pre-authenticated state if authenticating with a valid public key results in success. W represents the Weak Until operator.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasReqAuth ->
( (inp=NEWKEYS & out=NO_RESP & X inp=UA_PK_OK) ->
X out=UA_SUCCESS)
W (out=NO_CONN | out=UA_SUCCESS) )
\end{lstlisting}
\caption{Key exchange preserves pre-auth. state}
\label{prop:rper-pre-auth}
\end{property}
%Provided we perform successful finalization of a rekey, we remain in a pre-authenticated state until we exit this state, either by losing the connection (suggested by the \textsc{no\_conn} ) or by successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:rper-pre-auth}. Note that, we can tell we are in a pre-authenticated state if authenticating with a valid public key results in success. W represents the Weak Until operator.
%
%\begin{property}[h]
%\begin{lstlisting}[basicstyle=\footnotesize]
% G ( hasReqAuth ->
% ( (inp=NEWKEYS & out=NO_RESP & X inp=UA_PK_OK) ->
% X out=UA_SUCCESS)
% W (out=NO_CONN | out=UA_SUCCESS) )
%\end{lstlisting}
%\caption{Key exchange preserves pre-auth. state}
%\label{prop:rper-pre-auth}
%\end{property}
%\textit{Perhaps this could be merged into one property?}
......@@ -202,12 +204,12 @@ Provided we perform successful finalization of a rekey, we remain in a pre-authe
We have also formalized and checked properties drawn from the RFC specifications. We found parts of the specification unclear, which sometimes meant that we had to give our own interpretation before we could formalize. A first general property can be defined for the \textsc{disconnect} output. The RFC specifies that after sending this message, a party MUST not send or receive any data \cite[p. 24]{rfc4253}. While we cannot tell what the server actually receives, we can check that the server does not generate any output after sending \textsc{disconnect}. After a \textsc{disconnect} message, subsequent outputs should be solely derived by the {\dmapper}. Knowing the {\dmapper} induced outputs are \textsc{no\_conn}, \textsc{ch\_max} and \textsc{ch\_none}, we formulate by Property~\ref{prop:trans-disc} to describe
expected outputs after a \textsc{disconnect}.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=DISCONNECT ->
X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
\caption{No output after DISCONNECT}
%\caption{No output after DISCONNECT}
\label{prop:trans-disc}
\end{property}
......@@ -215,26 +217,26 @@ expected outputs after a \textsc{disconnect}.
The RFC states in~\cite[p. 24]{rfc4254} that after sending a \textsc{kexinit} message, a party MUST not send another \textsc{kexinit}, or a \textsc{sr\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:trans-kexinit}. Note that output \textsc{kex31\_newkeys} means that the {\dsut} sends a \textsc{kex31} followed by a \textsc{newkeys}.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=KEXINIT ->
X ( (out!=SR_ACCEPT & out!=KEXINIT)
W (out=NEWKEYS | out=KEX31_NEWKEYS) ) )
\end{lstlisting}
\caption{Disallowed outputs after KEXINIT}
\captionsetup{font=small}
%\caption{Disallowed outputs after KEXINIT}
%\captionsetup{font=small}
\label{prop:trans-kexinit}
\end{property}
The RFC also states \cite[p. 24]{rfc4254} 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 \textsc{sr\_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 by Property~\ref{prop:trans-sr}. For any service request (\textsc{sr\_auth} or \textsc{sr\_conn}, in case we are not in the initial state, the response will be either an accept (\textsc{sr\_accept}), disconnect (\textsc{disconnect}) which loses the connection in the next step, or \textsc{no\_conn}, the output generated by the {\dmapper} after the connection is lost. We adjusted the property for the initial state since all implementations responded with \textsc{kexinit} which would easily break the property. We cannot yet explain this behavior.
% , with the adjustment that we also allow the mapper induced output \textsc{no\_conn}, which suggests that connection was lost. Additionally, we exclude the initial state from the implication, as it is the only state where a \textsc{kexinit} is generated as a response, which seems to be the default behavior for all implementations.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (inp=SR_AUTH & state!=s0) ->
(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN )))
\end{lstlisting}
\caption{Allowed outputs after SR\_ACCEPT}
%\caption{Allowed outputs after SR\_ACCEPT}
\label{prop:trans-sr}
\end{property}
......@@ -244,50 +246,49 @@ The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service
The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the server rejects the authentication request, it MUST respond with a \textsc{ua\_failure} message. Rejected requests are those using invalid credentials (\textsc{ua\_pk\_nok} and \textsc{ua\_pw\_nok}) or an unacceptable authentication method ( \textsc{ua\_none}). In case the requests succeeds (\textsc{ua\_pk\_ok} and \textsc{ua\_pw\_ok}), a \textsc{ua\_success} MUST be sent only once. While not explicitly stated, we assume this to be in a context where the authentication service had been successfully requested, hence we use the {\dreqauth} predicate. We define two properties, Property~\ref{prop:auth-pre-ua} for behavior before an \textsc{ua\_success}, Property~\ref{prop:auth-post-ua-strong} for behavior afterward.
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasReqAuth ->
X ( (inp=UA_PK_NOK | inp=UA_PW_NOK | inp=UA_NONE)
-> out=UA_FAILURE)
W (out=UA_SUCCESS | output=NO_CONN) )
\end{lstlisting}
\caption{Invalid requests prompt UA\_FAILURE }
%\caption{Invalid requests prompt UA\_FAILURE }
\label{prop:auth-pre-ua}
\end{property}
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (out=UA_SUCCESS) ->
X G (out!=UA_SUCCESS) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
%\caption{UA\_SUCCESS is sent at most once}
\label{prop:auth-post-ua-strong}
\end{property}
In the same paragraph, it is stated that authentication requests received after a \textsc{ua\_success} SHOULD be ignored. This is a weaker statement, and it requires that all authentication messages
after a \textsc{ua\_success} output should prompt no response from the system(\textsc{no\_resp}) until the connection with the system is lost(\textsc{no\_conn}). The formulation of this statement shown in Property~\ref{prop:auth-post-ua}. The property uses $authReq$, a predicate which holds iff the input is an authentication message.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=UA_SUCCESS ->
X ( ( authReq-> out=NO_RESP )
W out=NO_CONN ) )
\end{lstlisting}
\caption{Silence after UA\_SUCCESS}
%\caption{Silence after UA\_SUCCESS}
\label{prop:auth-post-ua}
\end{property}
%\textit{Perhaps this could also be merged into one property?}
The Connection layer RFC states in \cite[p. 9]{rfc4254} that upon receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close} message, unless it had already sent this message for the channel. The channel must have been opened beforehand. Also, this condition no longer applies once the connection is lost (\textsc{no\_conn}) or once the channel was closed. We weaken it,so it also doesn't have to hold once the rekey procedure was initiated (by input \textsc{kexinit}), as all implementations were non-responsive during the rekey procedure. Along these lines we formulate Property~\ref{prop:conn-close}.
\begin{property}[h]
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
G ( ( hasOpenedChannel ->
X (inp=CH_CLOSE -> out=CH_CLOSE &
X ( (out!=CH_CLOSE) W (out=CH_OPEN_SUCCESS) ) )
W (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) )
\end{lstlisting}
\caption{CH\_CLOSE response on CH\_CLOSE request}
%\caption{CH\_CLOSE response on CH\_CLOSE request}
\label{prop:conn-close}
\end{property}
......@@ -297,9 +298,14 @@ The Connection layer RFC states in \cite[p. 9]{rfc4254} that upon receiving a \t
%On the same page, the RFC also states that in case the server rejects a service request, it should send an appropriate \textsc{disconnect} message. Moreover, in case it supports the service request, it MUST sent a \textsc{sr\_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.
\newcommand{\dt}{holds}
\newcommand{\dfce}[1]{#1}
\newcommand{\df}{false}
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the critical security properties hold.
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the critical security properties hold. For the properties that don't hold, we have
accumulated the list of reasons.
%\begin{center}\small
% \centering
\begin{table}
......@@ -308,18 +314,18 @@ Table~\ref{tab:mcresults} presents model checking results. Crucially, all the cr
\begin{tabular}{| r | r | c |c | c |}
\hline
& & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5}
& Property & OpenSSH & Bitvise & Dropbear \\ \hline
Critical & Trans. & & & \\ \cline{2-5}
& Auth. & & & \\ \hline
Rekey & Pre-auth. & & & \\ \cline{2-5}
& Auth. & & & \\ \hline
Functional& Prop.~\ref{prop:trans-disc} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-kexinit} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-sr} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-pre-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua-strong} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:conn-close} & & & \\ \hline
& Property & OpenSSH & Bitvise & Dropbear \\ \hline
Critical & Trans. & \dt & & \\ \cline{2-5}
& Auth. & \dt & & \\ \hline
Rekey & Pre-auth. & \dfce{sends unimpl} & & \\ \cline{2-5}
& Auth. & \dt & & \\ \hline
Functional& Prop.~\ref{prop:trans-disc} & \dt & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-kexinit} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-sr} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-pre-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua-strong} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:conn-close} & & & \\ \hline
\end{tabular}
\caption{Model checking results}
\label{tab:mcresults}
......
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