Commit 88acfa77 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Updated security definition

parent 3eab78af
......@@ -77,7 +77,7 @@ The remainder of this section defines the properties we formalized and verified.
\begin{enumerate}
\item \textit{basic characterizing properties}, properties which characterize the {\dmapper} and {\dsut} assembly at a basic level. These hold for all systems.
\item \textit{layer-critical security properties}, these are properties fundamental to achieving the main security goal of the respective layer.
\item \textit{security properties}, these are properties fundamental to achieving the main security goal of the respective layer.
\item \textit{key re-exchange properties}, that is properties regarding the key re-exchange operation (after the initial key exchange was done).
\item \textit{functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications. They may have a security impact.
\end{enumerate}
......@@ -85,24 +85,44 @@ The remainder of this section defines the properties we formalized and verified.
A key note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstract model, which represents an over-approximation of the {\dsut} induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model, concretization obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Performing model checking on an abstract model means we cannot fully translate model checking results to the concrete (unknown) model of the implementation. In particular, properties which hold for the abstract model do not necessarily hold for the implementation. Properties that don't hold however, also don't hold for the {\dsut}.
\newcommand{\dreqauth}{$hasReqAuth$}
\newcommand{\dauth}{$hasAuth$}
\newcommand{\dvauth}{$validAuthReq$}
\newcommand{\dauthreq}{$authReq$}
\newcommand{\diauth}{$invAuthReq$}
\newcommand{\dopchan}{$hasOpenedChannel$}
\newcommand{\drnewkeys}{$receivedNewKeys$}
\newcommand{\drkex}{$kexStarted$}
\newcommand{\dconnlost}{$connLost$}
\newcommand{\dend}{$endCondition$}
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
\lstset{%
escapeinside={(*}{*)},%
}
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} , {\dvauth} 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, a predicate for the receipt of \textsc{newkeys} from the server, and receipt of \textsc{kexinit}, which can also be seen as initiation of key (re-) exchange. These latter predicates have to be tweaked in accordance with the input alphabet used and with the output the {\dsut} generated (\textsc{kexinit} could be sent in different packaging, either alone, or joined by a different message). Their formulations correspond to the OpenSSH setting. Finally, by {\dconnlost} we define a predicate suggesting that connection was lost, and by {\dend}, the end condition for most higher layer properties.
\begin{center}
\begin{lstlisting}[basicstyle=\footnotesize]
hasReqAuth := inp=SR_AUTH & out=SR_ACCEPT
hasAuth := out=UA_PK_OK | out=UA_PW_OK
hasOpenedChannel := out=CH_OPEN_SUCCESS
(*{\dreqauth}*) := inp=SR_AUTH & out=SR_ACCEPT;
(*{\dvauth}*) := out=UA_PK_OK | out=UA_PW_OK;
(*{\dopchan}*) := out=CH_OPEN_SUCCESS;
(*{\dvauth}*) := inp=UA_PK_OK | inp=UA_PW_OK;
(*{\diauth}*) := inp=UA_PK_NOK|inp=UA_PW_NOK|inp=UA_NONE;
(*{\dauthreq}*) := validAuthReq | invalidAuthReq;
(*{\drnewkeys}*) := out=NEWKEYS | out=KEX31_NEWKEYS;
(*{\drkex}*) := out=KEXINIT;
(*{\dconnlost}*) := out=NO_CONN | out=DISCONNECT;
(*{\dend}*) := kexStarted | connLost;
\end{lstlisting}
\end{center}
Our formulation uses NuSMV syntax.
%We occasionally rely on past modalities operators such Once (O) and Since (S), which are uncommon, but are supported by NuSMV.
We also use the weak until operator W, which is not supported by NuSMV, but can be easily defined in terms of the until operator
U and globally operator G that are supported:
$p\,W\,q\, =\, p \,U\, q\, | \, G\, p$.
$p\,W\,q\, =\, p \,U\, q\, | \, G\, p$. Many of the higher layer properties we formulate should hold only until a disconnect or a key (re-)exchange happens, hence the definition of the {\dend} predicate. This is because the RFC's don't specify what should happen when no connection exists. Moreover, higher layer properties in the RFC's only apply outside of rekey sequences, as inside a rekey sequence, the RFC's suggest implementations to reject all higher layer inputs, regardless of the state before the rekey. We will frequently refer to $connLost | kexStarted$ as the \textit{end condition} .
%In the actual specification, W was replaced by this re-formulation. %Finally, we may define properties which we later use when defining other properties. This feature again isn't supported by NuSMV, hence the properties appear in expanded form in the run specification.
\subsection{Basic characterizing properties}
......@@ -135,7 +155,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\label{prop:channel}
\end{property}
\subsection{Layer-critical security properties}
\subsection{Security properties}
In SSH, upper layer services assume some notions of security, notions which are ensured by mechanisms in the lower layers. These mechanisms should have to be first engaged for the respective upper layer services to become available. As an example, the authentication service should only become available after exchanging and employing of kryptographic keys (key exchange) was done in the Transport layer, otherwise the service would be running over an unencrypted channel. Requests for this service should therefore not succeed unless key exchange was performed successfully.
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication should necessarily imply successful execution of the key exchange steps. We can tell each key exchange step were successful from the values of the input and output variables. Successful authentication request is indicated by the predicate defined earlier, {\dreqauth}. Following these principles, we define the LTL specification in Property~\ref{prop:sec-trans}, where O is the once operator. Formula $O p$ is true at time $t$ if $p$ held in at least one of the previous time steps $t' \leq t$.
......@@ -157,7 +177,7 @@ Key exchange implies three steps which have to be performed in order but may be
\label{prop:sec-trans}
\end{property}
Apart from a secure connection, Connection layer services also assume that the client behind the connection was authenticated. This is ensured by the Authentication layer by means of an authentication mechanism, which only succeeds, and thus authenticates the client, if valid credentials are provided. For the implementation to be secure, there should be no path from an unauthenticated to an authenticated state without the provision of valid credentials. We consider an authenticated state, a state where a channel can be opened successfully, captured by the predicate {\dopchan}. Provision of valid/invalid credentials is indicated by the outputs \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:sec-auth}, where S stands for the since operator.
Apart from a secure connection, Connection layer services also assume that the client behind the connection was authenticated. This is ensured by the Authentication layer by means of an authentication mechanism, which only succeeds, and thus authenticates the client, if valid credentials are provided. For the implementation to be secure, there should be no path from an unauthenticated to an authenticated state without the provision of valid credentials. We consider an authenticated state, a state where a channel has been opened successfully, captured by the predicate {\dopchan}. Provision of valid/invalid credentials is indicated by the outputs \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:sec-auth}, where S stands for the since operator.
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$.
......@@ -173,13 +193,14 @@ Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$
\subsection{Key re-exchange 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.
(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}.
(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 until one of two things happen, the connection is lost(\dconnlost) or we have authenticated. This is shown in Property~\ref{prop:rpos-pre-auth}. A similar property is defined for the authenticated state.
\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) ) ) )
X ( inp=KEX30 -> out=KEX31_NEWKEYS &
X (inp=NEWKEYS -> out=NO_RESP) ) ) W
(connLost | hasAuth ) )
\end{lstlisting}
%\caption{Rekey possible in pre-auth. state}
\label{prop:rpos-pre-auth}
......@@ -214,14 +235,14 @@ expected outputs after a \textsc{disconnect}.
\end{property}
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}.
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(\drnewkeys). This is translated to Property~\ref{prop:trans-kexinit}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=KEXINIT ->
X ( (out!=SR_ACCEPT & out!=KEXINIT)
W (out=NEWKEYS | out=KEX31_NEWKEYS) ) )
W receivedNewKeys ) )
\end{lstlisting}
%\caption{Disallowed outputs after KEXINIT}
%\captionsetup{font=small}
......@@ -244,14 +265,13 @@ The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service
%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}
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.
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 suggested by the predicate {\diauth}. In case of requests with valid credentials (\dvauth), 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. For the first property, note that (\dreqauth) may hold even after successful authentication, but we are only interested in behavior between the first time (\dreqauth) holds and the first time authentication is successful (out=\textsc{ua\_success}), hence the use of the O operator. As is the case with most higher layer properties, the first property only has to hold until the end condition holds(\dend), that is the connection is lost(\dconnlost) or rekey was started by the {\dsut} (\drkex).
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\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) )
G ( (hasReqAuth & !O out=UA_SUCCESS) ->
(invalidAuthReq -> (out=UA_FAILURE) )
W (out=UA_SUCCESS | endCondition ) )
\end{lstlisting}
%\caption{Invalid requests prompt UA\_FAILURE }
\label{prop:auth-pre-ua}
......@@ -266,27 +286,25 @@ The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the
\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.
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 (suggested by {\dauthreq}) after a \textsc{ua\_success} output should prompt no response from the system(\textsc{no\_resp}) until the end condition is true. The formulation of this statement shown in Property~\ref{prop:auth-post-ua}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=UA_SUCCESS ->
X ( ( authReq-> out=NO_RESP )
W out=NO_CONN ) )
W endCondition ) )
\end{lstlisting}
%\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}.
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 (\dopchan) and the property only has to hold up to when the end condition holds or the channel was closed(\textsc{ch\_close}). Along these lines we formulate Property~\ref{prop:conn-close}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
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) )
G ( hasOpenedChannel ->
( (inp=CH_CLOSE) -> (out=CH_CLOSE) )
W ( endCondition | out=CH_CLOSE) )
\end{lstlisting}
%\caption{CH\_CLOSE response on CH\_CLOSE request}
\label{prop:conn-close}
......@@ -304,28 +322,39 @@ The Connection layer RFC states in \cite[p. 9]{rfc4254} that upon receiving a \t
\subsection{Model checking results}
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.
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the security properties hold. For BitVise,
because it buffered all responses during rekey (including \textsc{UA\_SUCCESS}) we had to adapt our properties slightly.
In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest successful authentication.
Properties marked with '*' did not hold because implementations chose to send \textsc{unimpl}, instead of the output suggested by the RFC. As an example,
after successful authentication, both BitVise and OpenSSH respond with \textsc{unimpl} to further authentication requests, instead of being silent, violating
Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is acceptable, is up for debate.
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all transport layer specifications, however,
problematically, it violates important MUST properties. Firstly, upon receiving \text{ch\_close}, it responds by \textsc{ch\_eof} instead of \text{ch\_close}, not respecting
Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be generated multiple times, violating both Properties ~\ref{prop:auth-post-ua-strong} and
(implicitly) ~\ref{prop:auth-post-ua}.
%\begin{center}\small
% \centering
\begin{table}
\centering
\small
\begin{tabular}{| r | r | c |c | c |}
\begin{tabular}{| r | r | c | c |c | c |}
\hline
& & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5}
& 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
& & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
& Property & Requirement &OpenSSH & Bitvise & DropBear \\ \hline
Security & Trans. & & \dt & \dt & \dt \\ \cline{3-6}
& Auth. & & \dt & \dt * & \dt \\ \hline
Rekey & Pre-auth. possible & & \dfce{sends unimpl} & \dt & \dt \\ \cline{3-6}
& Auth. possible & & \dt & \dfce{disc for kex} & \dt \\ \hline
Functional& Prop.~\ref{prop:trans-disc} & MUST & \dt & \dt & \dt \\ \cline{3-6}
& Prop.~\ref{prop:trans-kexinit} & MUST & \dt & \dt & \dt \\ \cline{3-6}
& Prop.~\ref{prop:trans-sr} & MUST & \dfce{sends unimpl} & \dfce{kex no resp} & \dt \\ \cline{3-6}
& Prop.~\ref{prop:auth-pre-ua} & MUST & \dt & \dt * & \dt \\ \cline{3-6}
& Prop.~\ref{prop:auth-post-ua-strong} & MUST & \dt & \dt & \dfce{can recon after rekey} \\ \cline{3-6}
& Prop.~\ref{prop:auth-post-ua} & SHOULD & \dfce{sends unimpl} & \dfce{sends unimpl} & \df \\ \cline{3-6}
& Prop.~\ref{prop:conn-close} & MUST & \dt & \dfce{sends unimpl} & \dfce{sends CH\_EOF} \\ \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