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

Updated definitions

parent 1a18b770
\section{Checking security specifications} \label{sec:specs}
\section{Security specifications} \label{sec:specs}
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
We use the NuSMV model checker to verify security properties. 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.
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.
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.
The remainder of this section defines the properties we formalized and verified. We group these properties into three categories:
\begin{enumerate}
\item \textit{general security properties}, that is properties which must hold if the implementation is to be deemed secure
\item \textit{key exchange properties}, that is properties regarding the key exchange operation
\item \textit{other functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications
\item \textit{layer-critical 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 exchange operation
\item \textit{other 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}
A key note is that the properties describe not only the {\dsut}, but the {\dsut} and {\dmapper} assemble. Properties had to be adjusted so they with consideration of the {\dmapper}'s behavior. In particular, once connection with the server is lost it cannot be recovered and the {\dmapper} will itself respond with \textsc{no\_conn} responses. These have to be accounted for in the properties specified.
\subsection{General security properties}
Both the Transport and the Authentication Layers can be said to provide notions of security, which secure access to services of the Connection Layer. For each of these layers, we define general security properties that reflect successful implementation of these notions.
%Each upper SSH layer assumes a notion of security is provided by the layer bellow. The Authentication Layer assumes integrity and confidentiality is provided by the Transport Layer, the Connection Layer the same assumptions, plus it also assumes authentication was successful. We define a general property for each upper layer on the basis of successful implementation of these security notions.
\subsection{Layer-critical security properties}
The security property for the Transport layer is defined as follows: ``We consider a transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell an authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input \textsc{service\_request\_auth}, the output \textsc{service\_accept} was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
%Both the Transport and the Authentication Layers can be said to provide notions of security, which secure access to services of the Connection Layer. For each of these layers, we define general security properties that reflect successful implementation of these notions.
Each upper SSH layer assumes a notion of security is provided by the layer bellow. The means whereby these notions are achieved form the basis for defining these properties. The Authentication Layer
assumes integrity and confidentiality is provided. The Transport layer provides this, by first exchanging and employing kryptographic keys, before invoking the authentication service at the client's request. Hence, it should not be possible to summon authentication service before some form of key exchange is done, otherwise authentication would be done over a un-encrypted channel. In other words, authentication request should not succeed if key exchange wasn't performed successfully.
Key exchange implies performing three steps which have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell an authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input \textsc{service\_request\_auth}, the output \textsc{service\_accept} was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -31,13 +35,16 @@ G ( (input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT) ->
O ( (input=KEX30 & output=KEX31_NEWKEYS) &
O (output=KEXINIT) ) ) )
\end{lstlisting}
\caption{Transport layer security property.}
\caption{Transport layer-critical security property.}
\label{prop:prop1}
\end{property}
In a similar way, we say that the Authentication Layer is secure ``if there is no path from the unauthenticated state to the authenticated state without providing the correct credentials.''\cite{Verleg2016}
Since we have no method to directly determine if the model is in an authenticated state, we consider the authenticated state to be a state where opening a channel can be done successfully.
Since opening a channel should only be possible after user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the \textsc{ua\_failure} or \textsc{ua\_success} packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Property~\ref{prop:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
In a similar way, the Connection layer not only assumes an encrypted channel, but also that the user is authorized. The Authentication layer ensures this by
employing authentication methods, which successfully authenticate the user only if provided correct credentials. Once authenticated, access to services of the Connection layer is granted.
Authentication can only be ensured if, there should be no path from the unauthenticated state to the authenticated state without the correct credentials, otherwise illegitimate users might gain
access to the system.
Since we have no method to directly determine if the we are in an authenticated state, we consider the authenticated state to be a state where opening a channel can be done successfully. Since opening a channel should only be possible after successful user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the \textsc{ua\_failure} or \textsc{ua\_success} packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Property~\ref{prop:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -76,7 +83,8 @@ G ( (output = KEXINIT) ->
X (output != SERVICE_ACCEPT & output != KEXINIT)
W X (output = NEWKEYS | output = KEX31_NEWKEYS ) )
\end{lstlisting}
\caption{Allowed outputs after KEXINIT}
\caption{Disallowed outputs after KEXINIT}
\captionsetup{font=small}
\label{prop:prop4}
\end{property}
......@@ -99,7 +107,7 @@ G ( X (output = UA_SUCCESS) ->
((output!=UA_SUCCESS & (input=UA_PK_NOK -> output=UA_FAILURE))
S (input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT) ) )
\end{lstlisting}
\caption{Implementation should send UA\_SUCCESS at most once}
\caption{UA\_SUCCESS is sent at most once}
\label{prop:prop6}
\end{property}
......@@ -109,7 +117,7 @@ G (output = UA_SUCCESS ->
X ( (input=UA_PK_OK | input=UA_PK_NOK) -> output=NO_RESP )
W X X(output= NO_CONN) )
\end{lstlisting}
\caption{After UA\_SUCCESS, silently ignore auth. requests}
\caption{Silently ignore auth. requests post UA\_SUCCESS}
\label{prop:prop7}
\end{property}
......
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