Commit 17072e7a authored by Frits Vaandrager's avatar Frits Vaandrager

pass over property section

parent 8e5245cb
......@@ -5,10 +5,10 @@
\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.
%The size 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 \cite{NuSMV2} to verify security properties for the %learned models, properties which we formalize using LTL formulas.
NuSMV is a model checker where 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 given 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.
A NuSMV model is specified via a set of finite variables together with a transition-function that describes 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 given specification is not true. We generate NuSMV models automatically from the learned models. Generation proceeds by first defining a NuSMV file with three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to this file.
This function updates the output and state variables for a given valuation of the input variable and the current state. Figure~\ref{fig:nusmvex} gives an example of a Mealy machine and it's associated NuSMV model.
%\parbox{\columnwidth}{
......@@ -35,18 +35,18 @@ This function updates the output and state variables for a given valuation of th
\begin{figure}[h]
\centering
%\begin{subfigure}
\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
\begin{tikzpicture}[scale=0.1,>=stealth',shorten >=1pt,auto,node distance=2.5cm]
\node[initial,state] (q0) {$q_0$};
\node[state] (q1) [right of=q0] {$q_1$};
\path[->] (q0) edge node {INIT/OK} (q1);
\path[->] (q0) edge node {BEGIN/OK} (q1);
\path[->] (q0) edge [loop above] node {MSG/NOK} (q0);
\path[->] (q1) edge [loop above] node {INIT/OK} (q1);
\path[->] (q1) edge [loop above] node {BEGIN/OK} (q1);
\path[->] (q1) edge [loop right] node {MSG/ACK} (q1);
\end{tikzpicture}
%\end{subfigure}
\\
\footnotesize
\tiny
\begin{lstlisting}
MODULE main
VAR state : {q0, q1};
......@@ -68,7 +68,7 @@ This function updates the output and state variables for a given valuation of th
esac;
\end{lstlisting}
\caption{A Mealy Machine and its associated NuSMV model}
\caption{Mealy machine + associated NuSMV code}
\label{fig:nusmvex}
\end{figure}
......@@ -128,8 +128,8 @@ $p\,W\,q\, =\, p \,U\, q\, | \, G\, p$. Many of the higher layer properties we
\subsection{Basic characterizing properties}
%cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met.
In our setting, one TCP connection with the system is made and once the connection is lost (because the system disconnects for example), it can no longer be re-established. The moment
a connection is lost is suggested by generation of the \textsc{no\_conn} output. From this moment onwards, the only outputs encountered are the \textsc{no\_conn} output (the {\dmapper} tried but failed to communicate with the {\dsut}), or outputs generated by the {\dmapper} directly, without querying the system . The latter are \textsc{ch\_max} (channel buffer is full) and \textsc{ch\_none} (channel buffer is empty). With these outputs we define Property~\ref{prop:noconn} which describes the ``one connection'' property of our setup.
In our setting, a single TCP connection with the system is made and once this connection is lost (e.g.\ because the system disconnects), it can not be re-established. The moment
a connection is lost is marked by generation of the \textsc{no\_conn} output. From this moment onwards, the only outputs encountered are the \textsc{no\_conn} output (the {\dmapper} tried but failed to communicate with the {\dsut}), or outputs generated by the {\dmapper} directly, without querying the system. The latter are \textsc{ch\_max} (channel buffer is full) and \textsc{ch\_none} (channel buffer is empty). With these outputs we define Property~\ref{prop:noconn} which describes the ``one connection'' property of our setup.
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -191,9 +191,8 @@ Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$
\end{property}
\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.
%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.
According to the RFC \cite[p. 24]{rfc4254}, re-exchanging keys (or rekey-ing) (1) is preferably allowed in all states of the protocol, and (2) its successful execution does not affect operation of the higher layers. We consider two general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These may map to multiple states in the learned models. We formalized requirement (1) by
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 asserted in Property~\ref{prop:rpos-pre-auth}. A similar property is defined for the authenticated state.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
G ( hasReqAuth ->
......@@ -205,6 +204,8 @@ Important properties are that re-exchanging keys (or rekey-ing) is (1) preferabl
%\caption{Rekey possible in pre-auth. state}
\label{prop:rpos-pre-auth}
\end{property}
Requirement (2) cannot be expressed in LTL, since in LTL we cannot specify that two states are equivalent.
We therefore checked this requirement directly, by writing a simple script which, for each state $q$ that allows rekeying, checks if the state $q'$ reached after a successful rekey is equivalent to $q$ in the subautomaton that only contains the higher layer inputs.
%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.
%
......@@ -222,7 +223,7 @@ Important properties are that re-exchanging keys (or rekey-ing) is (1) preferabl
%\textit{Perhaps this could be merged into one property?}
\subsection{Functional properties}
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
We have formalized and checked several other properties drawn from the RFCs. 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}
......@@ -322,36 +323,26 @@ G ( hasOpenedChannel ->
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the security properties hold. For BitVise,
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. 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. 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 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}.
%\begin{center}\small
% \centering
\begin{table}
\begin{table}[h!]
\centering
\small
\begin{tabular}{| l | l | c | c |c | c |}
\hline
& & & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6}
& Property & Requirement &OpenSSH & Bitvise & DropBear \\ \hline
& Property & Key word &\tiny{OpenSSH} & \tiny{Bitvise} & \tiny{DropBear} \\ \hline
Security & Trans. & & \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}
Rekey & Pre-auth. & & \dfce{sends unimpl} & \dt & \dt \\ \cline{3-6}
& Auth. & & \dt & \dfce{disc for kex} & \dt \\ \hline
Funct.& 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}
......@@ -362,6 +353,14 @@ Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be
\end{table}
%\end{center}
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. 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 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}.
%, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.
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