Commit 1b243f09 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated definitions

parent 3fba3655
\section{Conclusions}\label{sec:conclusions}
We have combined model learning with abstraction techniques to infer models of the OpenSSH, Bitvise and Dropbear SSH server implementations. We have also
We have combined model learning with abstraction techniques to infer models of the OpenSSH, Bitvise and DropBear SSH server implementations. We have also
formalized several security and functional properties drawn from the SSH RFC specifications. We have verified these
properties on the learned models using model checking and have uncovered several minor inconsistencies, though crucially, the main security goals were met
by all implementation.
......
-- Security Properties
-- Transport Layer Security
-- Authentication Layer Security
-- Rekey Properties
-- Authenticated rekey is possible
LTLSPEC NAME auth_rekey_pos := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | ( out=UA_SUCCESS) ) ->
( X (inp=KEXINIT -> out=KEXINIT & X (inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
-- Authenticated state is preserved
LTLSPEC NAME auth_rekey_pres := G ( ( ( inp=CH_CLOSE & out=CH_CLOSE) | (inp=CH_OPEN & out=CH_OPEN_SUCCESS) | (inp=SR_AUTH & out=SR_ACCEPT) ) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) ) U (out=NO_CONN) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=CH_OPEN ) ) -> X ( out=CH_OPEN_SUCCESS | out=CH_MAX) )
& G ! (out=NO_CONN) ) )
-- Pre-auth rekey is possible
LTLSPEC NAME pre-auth_rekey_pos := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( X (inp=KEXINIT -> out=KEXINIT & X ( inp=KEX30 -> out=KEX31_NEWKEYS & X (inp=NEWKEYS -> out=NO_RESP) ) ) ) )
---- Preauth state is preserved
--LTLSPEC G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
-- ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
-- ( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
-- & G ! (out=DISCONNECT | out=UA_SUCCESS) ) )
-- Pre-auth state is preserved
LTLSPEC NAME pre-auth_rekey_pres := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) ) U (out=NO_CONN | out=UA_SUCCESS) |
( G ( ( inp=NEWKEYS & out=NO_RESP & X ( inp=UA_PK_OK ) ) -> X ( out=UA_SUCCESS) )
& G ! (out=NO_CONN | out=UA_SUCCESS) ) )
-- Functional Properties
---- After sending a KEXINIT, the other side should not send another KEXINIT or SR_ACCEPT until it has sent NEWKEYS
LTLSPEC NAME trans_kexinit := G ( (out=KEXINIT) ->
X ( ( (out!=SR_ACCEPT & out!=KEXINIT) U (out=NEWKEYS | out=KEX31_NEWKEYS ) |
G (out!=SR_ACCEPT & out!=KEXINIT) & G ! (out=NEWKEYS | out=KEX31_NEWKEYS ) ) ) )
-- If the server rejects the service request, it SHOULD send an
-- appropriate SSH_MSG_DISCONNECT message and MUST disconnect.
LTLSPEC NAME trans_sr := G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
(out=SR_ACCEPT | (out=DISCONNECT & X G(inp=SR_AUTH -> out=NO_CONN) ) ) )
-- If the server rejects the authentication request, it MUST respond
-- with the following: SSH_MSG_USERAUTH_FAILURE. *It may also disconnect on failed unauth attempts
LTLSPEC NAME auth_ua_pre := G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) U (out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) |
(G ( (inp=UA_PK_NOK -> out=UA_FAILURE) & (inp=UA_PK_OK -> out=UA_SUCCESS) ) & G !(out=UA_SUCCESS | out=NO_CONN | out=DISCONNECT) ) )
-- SSH_MSG_USERAUTH_SUCCESS MUST be sent only once. When
-- SSH_MSG_USERAUTH_SUCCESS has been sent, any further authentication
-- requests received after that SHOULD be silently ignored. *openssh sends UNIMPL, is that bad?
LTLSPEC NAME auth_ua_post := G ( (out=UA_SUCCESS) ->
X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) U (out=NO_CONN) |
(G X ( (inp=UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP) & G !(out=NO_CONN) ) )
-- Upon receiving this message, a party MUST
-- send back an SSH_MSG_CHANNEL_CLOSE unless it has already sent this
-- message for the channel. The channel is considered closed for a
-- party when it has both sent and received SSH_MSG_CHANNEL_CLOSE, and
-- the party may then reuse the channel number.
-- Had to add NEWKEYS and KEXINIT ins, strangely KEXINIT closes
LTLSPEC NAME conn_close := G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
( ( ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) U (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) |
( G ( (inp=CH_CLOSE) -> (out=CH_CLOSE)) & G ! (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) ) ) )
\ No newline at end of file
......@@ -46,21 +46,24 @@ This function updates the output and state variable for a given valuation of the
\\
\small
\begin{lstlisting}
MODULE example
VAR state : {q0, q1}
out : {OK, NOK, ACK}
in : {INIT, MSG}
init(state) := q0
MODULE main
VAR state : {q0, q1};
out : {OK, NOK, ACK};
inp : {INIT, MSG};
ASSIGN
init(state) := q0;
next(state) := case
state = q0 & in = INIT: q1
state = q0 & in = MSG: q0
state = q1 & in = INIT: q1
state = q1 & in = MSG: q1
next(out) := case
state = q0 & in = INIT: OK
state = q0 & in = MSG: ONOK
state = q1 & in = INIT: OK
state = q1 & in = MSG: ACK
state = q0 & inp = INIT: q1;
state = q0 & inp = MSG: q0;
state = q1 & inp = INIT: q1;
state = q1 & inp = MSG: q1;
esac;
next(out) := case
state = q0 & inp = INIT: OK;
state = q0 & inp = MSG: ONOK;
state = q1 & inp = INIT: OK;
state = q1 & inp = MSG: ACK;
esac;
\end{lstlisting}
\caption{A Mealy Machine and its associated NuSMV model}
......@@ -94,10 +97,10 @@ G (out=NO_CONN ->
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (in=CH_OPEN & out!=CH_MAX -> (in=CH_OPEN -> out=CH_MAX)
W (in=CH_CLOSE & out!=CH_NONE &
G (inp=CH_OPEN & out!=CH_MAX -> (inp=CH_OPEN -> out=CH_MAX)
W (inp=CH_CLOSE & out!=CH_NONE &
(isConnectionInput(in) -> out=CH_NONE)
W (in=CH_OPEN) ) )
W (inp=CH_OPEN) ) )
\end{lstlisting}
\caption{Mapper induced property.}
\label{prop:channel}
......@@ -117,10 +120,10 @@ Following these principles, we define the LTL specification in Property~\ref{pro
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SR_AUTH & out=SR_ACCEPT) |
(in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
O ( (in=NEWKEYS & out=NO_RESP) &
O ( (in=KEX30 & out=KEX31_NEWKEYS) &
G ( (inp=SR_AUTH & out=SR_ACCEPT) |
(inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
O ( (inp=NEWKEYS & out=NO_RESP) &
O ( (inp=KEX30 & out=KEX31_NEWKEYS) &
O (out=KEXINIT) ) ) )
\end{lstlisting}
\caption{Transport layer security.}
......@@ -132,7 +135,7 @@ Apart from a secure connection, Connection layer services also assume that the c
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
G ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
(!(out=UA_FAILURE) S out=UA_SUCCESS) )
\end{lstlisting}
\caption{Authentication layer security.}
......@@ -146,10 +149,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:rpos-pre-auth}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SR_AUTH & out=SR_ACCEPT) ->
X (in=KEXINIT -> out=KEXINIT &
X (in=KEX30 -> out=KEX31_NEWKEYS &
X (in=NEWKEYS -> out=NO_RESP) ) ) )
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
X (inp=KEXINIT -> out=KEXINIT &
X (inp=KEX30 -> out=KEX31_NEWKEYS &
X (inp=NEWKEYS -> out=NO_RESP) ) ) )
\end{lstlisting}
\caption{Rekey possible in pre-auth. state}
\label{prop:rpos-pre-auth}
......@@ -159,8 +162,8 @@ Provided we perform successful finalization of a rekey, we remain in a pre-authe
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SR_AUTH & out=SR_ACCEPT) ->
( (in=NEWKEYS & out=NO_RESP & X in=UA_PK_OK) ->
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
( (inp=NEWKEYS & out=NO_RESP & X inp=UA_PK_OK) ->
X out=UA_SUCCESS)
W (out=NO_CONN | out=UA_SUCCESS) )
\end{lstlisting}
......@@ -191,11 +194,11 @@ an accept(\textsc{sr\_accept}) or a disconnect(\textsc{disconnect}) which loses
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (in=SR_AUTH & out!=NO_CONN & state!=s0)
-> (out=SR_ACCEPT | (out=DISCONNECT &
X G (in=SR_AUTH -> out=NO_CONN) ) ) )
G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
(out=SR_ACCEPT | (out=DISCONNECT &
X G (inp=SR_AUTH -> out=NO_CONN) ) ) )
\end{lstlisting}
\caption{Allowed outputs after sr\_accept}
\caption{Allowed outputs after SR\_ACCEPT}
\label{prop:trans-sr}
\end{property}
......@@ -205,9 +208,9 @@ 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=SR_AUTH & out=SR_ACCEPT) ->
X ( (in=UA_PK_NOK -> out=UA_FAILURE) &
(in=UA_PK_OK -> out=UA_SUCCESS) )
G ( (inp=SR_AUTH & out=SR_ACCEPT) ->
X ( (inp=UA_PK_NOK -> out=UA_FAILURE) &
(inp=UA_PK_OK -> out=UA_SUCCESS) )
W (out=UA_SUCCESS | output=NO_CONN) )
\end{lstlisting}
\caption{UA\_SUCCESS is sent at most once}
......@@ -217,7 +220,7 @@ 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 )
X ( ( (in =UA_PK_OK | inp=UA_PK_NOK) -> out=NO_RESP )
W out=NO_CONN ) )
\end{lstlisting}
\caption{Silently ignore auth. requests after UA\_SUCCESS}
......@@ -229,10 +232,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 &
G ( ( (inp=CH_OPEN & out=CH_OPEN_SUCCESS) ->
X (inp=CH_CLOSE -> out=CH_CLOSE &
X ( (out!=CH_CLOSE) W (out=CH_OPEN_SUCCESS) ) )
W (out=NO_CONN | in=KEXINIT | out=CH_CLOSE) )
W (out=NO_CONN | inp=KEXINIT | out=CH_CLOSE) )
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\label{prop:conn-close}
......@@ -263,7 +266,7 @@ Table~\ref{tab:mcresults} presents model checking results. Crucially, all the cr
Functional& 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-pre-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:conn-close} & & & \\ \hline
\end{tabular}
\caption{Model checking results}
......
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