Commit b35932f3 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Minor additions

parent 1cc821bd
......@@ -29,8 +29,7 @@ tabsize=2
%\acmISBN{123-4567-24-567/08/06}
%Conference
\acmConference[SPIN'17]{SPIN Symposium}{July 1997}{El
Paso, Texas USA}
\acmConference[SPIN'17]{SPIN Symposium}{July 2017}{California, USA}
\acmYear{2017}
\copyrightyear{2017}
......@@ -39,6 +38,7 @@ tabsize=2
\begin{document}
\graphicspath{{images/}}
\title{Leveraging Model Learning and Model Checking to Infer and Verify SSH Implementations}
\renewcommand{\shorttitle}{Inference and Verification of SSH Implementations}
......
......@@ -4,9 +4,9 @@
\floatname{property}{Property}
The learned models are too big for thorough manual inspection and verification of specifications. Manual analysis is further complicated by the ambiguity 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 to LTL.
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.
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.
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 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. 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.
The remainder of this section defines the properties we formalized and verified. We group these properties into three categories:
......@@ -26,30 +26,36 @@ Since we are checking the model of a {\dsut} and {\dmapper} assemble, we had to
\subsection{Layer-critical 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, authentication and connection services should only become available after exchanging and employing of kryptographic keys (key exchange) was done in the Transport layer, otherwise these services would be running over an unencrypted channel. Requests for these services 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 or connection service requests should necessarily imply successful execution of the key exchange steps. We can tell a service request or a key exchange step were successful from the values of the input and output variables. For example, an authentication service request is successful if for the input \textsc{service\_request\_auth}, the output \textsc{service\_accept} was received. One would expect that a connection service request would in a similar way be successful if on sending \textsc{service\_request\_conn}, we would also receive the output \textsc{service\_accept}. Unfortunately, as discussed in the previous section, this is never the case, so we choose successfully opening a channel as way to signal that connection services were engaged. This is suggested by receiving a \textsc{ch\_open\_success} output to a \textsc{ch\_open} input.
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication or connection service requests should necessarily imply successful execution of the key exchange steps. We can tell a service request or a key exchange step were successful from the values of the input and output variables. For example, an authentication service request is successful if for the input \textsc{sr\_auth}, the output \textsc{service\_accept} was received. One would expect that a connection service request would in a similar way be successful if on sending \textsc{sr\_conn}, we would also receive the output \textsc{service\_accept}. Unfortunately, as discussed in the previous section, this is never the case, so we choose successfully opening a channel as way to signal that connection services were engaged. This is suggested by receiving a \textsc{ch\_open\_success} output to a \textsc{ch\_open} input.
Following these principles, we define the LTL specification in Property~\ref{prop:prop1}, where O stands for the Once-operator. This operator is a past time LTL operator which holds if its argument holds in a past time instant.
% SERVICE_REQUEST_AUTH -> SR_AUTH
% SERVICE_REQUEST_CONN -> SR_CONN
% SERVICE_REQUEST_CONN -> SR_CONN
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in =SERVICE_REQUEST_AUTH & out =SERVICE_ACCEPT) |
(in= CH_OPEN & out= CH_OPEN_SUCCESS) ->
O ( (in =NEWKEYS & out = NO_RESP) &
O ( (in =KEX30 & out =KEX31_NEWKEYS) &
O (out =KEXINIT) ) ) )
G ( (in=SR_AUTH & out=SERVICE_ACCEPT) |
(in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
O ( (in=NEWKEYS & out=NO_RESP) &
O ( (in=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
\end{lstlisting}
\caption{Transport layer security property.}
\caption{Transport layer security.}
\label{prop:prop1}
\end{property}
Apart from a secure connection, the 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. Provision of valid/invalid credentials is suggested by the outputs \textsl{ua\_success} and \textsl{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:prop2}, where S stands for the Since-operator. This operator holds if its first argument holds up to the moment its second argument holds, with the mention that the second argument has to hold somewhere along the path.
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. Provision of valid/invalid credentials is suggested by the outputs \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:prop2}, where S stands for the Since-operator. This operator holds if its first argument holds up to the moment its second argument holds, with the mention that the second argument has to hold somewhere along the path.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in= CH_OPEN & out= CH_OPEN_SUCCESS) ->
(!(out=UA_FAILURE) S out= UA_SUCCESS) )
G ( (in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
(!(out=UA_FAILURE) S out=UA_SUCCESS) )
\end{lstlisting}
\caption{Authentication layer security property.}
\caption{Authentication layer security.}
\label{prop:prop2}
\end{property}
......@@ -60,10 +66,10 @@ Important properties are that re-exchanging keys (or rekey-ing) is allowed in al
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 rekey in succession should imply success. This is shown in Property~\ref{prop:prop25}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SERVICE_REQUEST_AUTH & out=SERVICE_ACCEPT) ->
X (in = KEXINIT -> out = KEXINIT &
X ( in = KEX30 -> out= KEX31_NEWKEYS &
X (in = NEWKEYS -> out=NO_RESP ) ) ) )
G ( (in=SR_AUTH & out=SERVICE_ACCEPT) ->
X (in=KEXINIT -> out=KEXINIT &
X (in=KEX30 -> out=KEX31_NEWKEYS &
X (in=NEWKEYS -> out=NO_RESP) ) ) )
\end{lstlisting}
\caption{Key exchange possible in pre-auth. state}
\label{prop:prop25}
......@@ -73,10 +79,10 @@ Provided we perform successful finalization of a rekey, we remain in a pre-authe
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in = SERVICE_REQUEST & out = SERVICE_ACCEPT) ->
( ( in = NEWKEYS & out = NO_RESP
& X ( in = UA_PK_OK ) ) -> X ( out =UA_SUCCESS) )
W (out = NO_CONN | out = UA_SUCCESS)
G ( (in=SERVICE_REQUEST & out=SERVICE_ACCEPT) ->
( (in=NEWKEYS & out=NO_RESP & X in=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:prop3}
......@@ -90,9 +96,9 @@ We have also formalized and checked properties drawn from the RFC specifications
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (out = KEXINIT) ->
X ( (out != SERVICE_ACCEPT & out != KEXINIT)
W (out = NEWKEYS | out = KEX31_NEWKEYS ) ) )
G ( (out=KEXINIT) ->
X ( (out!=SERVICE_ACCEPT & out!=KEXINIT)
W (out=NEWKEYS | out=KEX31_NEWKEYS) ) )
\end{lstlisting}
\caption{Disallowed outputs after KEXINIT}
\captionsetup{font=small}
......@@ -105,11 +111,9 @@ an accept(\textsc{service\_accept}) or a disconnect(\textsc{disconnect}) which
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in = SERVICE_REQUEST_AUTH
& out != NO_CONN
& state != s0)
-> (out = SERVICE_ACCEPT | (out = DISCONNECT &
X G (in = SERVICE_REQUEST -> out = NO_CONN) ) ) )
G ( (in=SR_AUTH & out!=NO_CONN & state!=s0)
-> (out=SERVICE_ACCEPT | (out=DISCONNECT &
X G (in=SERVICE_REQUEST -> out=NO_CONN) ) ) )
\end{lstlisting}
\caption{Allowed outputs after SERVICE\_ACCEPT}
\label{prop:prop5}
......@@ -121,10 +125,10 @@ The RFC for the Authentication Layer states in~\cite[p. 6]{rfc4252} that if the
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SERVICE_REQUEST_AUTH & out=SERVICE_ACCEPT) ->
X ( (in = UA_PK_NOK -> out = UA_FAILURE) &
(in = UA_PK_OK -> out = UA_SUCCESS) )
W ( out = UA_SUCCESS | output = NO_CONN) )
G ( (in=SR_AUTH & out=SERVICE_ACCEPT) ->
X ( (in=UA_PK_NOK -> out=UA_FAILURE) &
(in=UA_PK_OK -> out=UA_SUCCESS) )
W (out=UA_SUCCESS | output=NO_CONN) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
\label{prop:prop6}
......@@ -132,9 +136,9 @@ The RFC for the Authentication Layer states in~\cite[p. 6]{rfc4252} that if the
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (out = UA_SUCCESS ->
X ( ( ( in =UA_PK_OK | in =UA_PK_NOK) -> out =NO_RESP )
W out = NO_CONN ) )
G (out=UA_SUCCESS ->
X ( ( (in =UA_PK_OK | in=UA_PK_NOK) -> out=NO_RESP )
W out=NO_CONN ) )
\end{lstlisting}
\caption{Silently ignore auth. requests after UA\_SUCCESS}
\label{prop:prop7}
......@@ -145,10 +149,10 @@ The Connection Layer RFC states that upon receiving a \textsc{ch\_close} message
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( ( (in = CH_OPEN & out = CH_OPEN_SUCCESS) ->
X (in = CH_CLOSE -> out = CH_CLOSE &
X ( (out != CH_CLOSE) W (out = CH_OPEN_SUCCESS) ) )
W (out = NO_CONN | in = KEXINIT | out = CH_CLOSE) )
G ( ( (in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
X (in=CH_CLOSE -> out=CH_CLOSE &
X ( (out!=CH_CLOSE) W (out=CH_OPEN_SUCCESS) ) )
W (out=NO_CONN | in=KEXINIT | out=CH_CLOSE) )
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\label{prop:prop8}
......@@ -168,7 +172,7 @@ Table~\ref{tab:mcresults} presents model checking results. Crucially, all the cr
\begin{table}
\centering
\small
\begin{tabular}{| r | r | ccc |}
\begin{tabular}{| r | r | c |c | c |}
\hline
& & \multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5}
& Property & OpenSSH & Bitvise & Dropbear \\ \hline
......
......@@ -18,7 +18,7 @@ the common case of a successful operation. The SSH protocol happy flow at a high
\begin{figure}[!hb]
\centering
\includegraphics[width=0.65\linewidth]{SSH_protocols.png}
\includegraphics[scale=0.35]{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