Commit 05c3afee by Paul Fiterau Brostean

### Committed definitions

parent 028a7869
 ... ... @@ -3,7 +3,7 @@ %\newfloat{property}{thp}{lop} %\floatname{property}{Property} \newtheorem{property}[theorem]{Property} \newtheorem{property}{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. ... ... @@ -120,7 +120,7 @@ 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$. 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} . $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. %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. ... ... @@ -192,8 +192,8 @@ 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 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. %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. (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. 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 -> ... ... @@ -316,9 +316,9 @@ G ( hasOpenedChannel -> %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} \newcommand{\dt}{\color{green}\checkmark} \newcommand{\dfce}[1]{\color{red}X} \newcommand{\df}{\color{red}X} \subsection{Model checking results} ... ... @@ -328,10 +328,11 @@ In particular, we used {\dvauth} instead of $out=UA\_SUCCESS$ to suggest success 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. Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is acceptable, is up for debate. Definitely the RFC does not suggest it, though the RFC does leave room for interpretation of the \textsc{unimpl} message. 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 problematically, it violates properties of the higher layers. 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}. ... ... @@ -340,21 +341,21 @@ Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be \begin{table} \centering \small \begin{tabular}{| r | r | c | c |c | c |} \begin{tabular}{| l | l | c | c |c | c |} \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} & Auth. & & \dt & \dt & \dt \\ \hline Rekey & Pre-auth. pos. & & \dfce{sends unimpl} & \dt & \dt \\ \cline{3-6} & Auth. pos. & & \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 & Prop.~\ref{prop:auth-post-ua} & SHOULD & \dfce{sends unimpl}* & \dfce{sends unimpl}* & \df \\ \cline{3-6} & Prop.~\ref{prop:conn-close} & MUST & \dt & \dt & \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!