security_definitions.tex 27.4 KB
Newer Older
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
1
\section{Security specifications} \label{sec:specs}
2

3 4 5
%\newfloat{property}{thp}{lop}
%\floatname{property}{Property}

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
6
  \newtheorem{property}{Property}
7

Frits Vaandrager's avatar
Frits Vaandrager committed
8 9
%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.  
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
10

Frits Vaandrager's avatar
Frits Vaandrager committed
11
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. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
12
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
13

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
%\parbox{\columnwidth}{
%  \parbox{0.5\columnwidth}{
%\begin{tikzpicture}[>=stealth',shorten >=1pt,auto,node distance=2.8cm]
%  \node[initial,state] (q0)      {$q_0$};
%  \node[state]         (q1) [right of=q0]  {$q_1$};
%
%  \path[->]          (q0)  	edge  						   node {INIT/OK} (q1);
%	\path[->]          (q0)  	edge  [loop above]   node {MSG/NOK} (q0);
%	\path[->]          (q1)  	edge  [loop above]   node {INIT/OK} (q1);
%  \path[->]          (q1)  	edge  [loop right] 	 node {MSG/ACK} (q1);
%\end{tikzpicture}	
%}
%\parbox{0.5\columnwidth}{
%\begin{verbatim}
%
%\end{verbatim}
%}
%}

%\lstset{showspaces=true}

Erik Poll's avatar
shit  
Erik Poll committed
35
\begin{figure}[h]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
36 37
\centering
%\begin{subfigure}
Frits Vaandrager's avatar
Frits Vaandrager committed
38
\begin{tikzpicture}[scale=0.1,>=stealth',shorten >=1pt,auto,node distance=2.5cm]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
39 40 41
  \node[initial,state] (q0)      {$q_0$};
  \node[state]         (q1) [right of=q0]  {$q_1$};

Frits Vaandrager's avatar
Frits Vaandrager committed
42
  \path[->]          (q0)  	edge  						   node {BEGIN/OK} (q1);
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
43
	\path[->]          (q0)  	edge  [loop above]   node {MSG/NOK} (q0);
Frits Vaandrager's avatar
Frits Vaandrager committed
44
	\path[->]          (q1)  	edge  [loop above]   node {BEGIN/OK} (q1);
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
45 46 47 48
  \path[->]          (q1)  	edge  [loop right] 	 node {MSG/ACK} (q1);
\end{tikzpicture}
%\end{subfigure}
\\
Frits Vaandrager's avatar
Frits Vaandrager committed
49
\tiny
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
50
\begin{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
51 52
	MODULE main 
		VAR state : {q0, q1};
Frits Vaandrager's avatar
Frits Vaandrager committed
53
		inp : {BEGIN, MSG};
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
54 55 56
		out : {OK, NOK, ACK};
		ASSIGN
		init(state) := q0;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
57
		next(state) := case
Frits Vaandrager's avatar
Frits Vaandrager committed
58
			state = q0 & inp = BEGIN: q1;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
59
			state = q0 & inp = MSG: q0; 
Frits Vaandrager's avatar
Frits Vaandrager committed
60
			state = q1 & inp = BEGIN: q1;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
61
			state = q1 & inp = MSG: q1; 
Frits Vaandrager's avatar
Frits Vaandrager committed
62 63 64 65 66
	    esac;
		out := case
			state = q0 & inp = BEGIN: OK;
			state = q0 & inp = MSG: NOK;
			state = q1 & inp = BEGIN: OK;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
67 68
			state = q1 & inp = MSG: ACK;
		esac;
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
69 70
\end{lstlisting}

Frits Vaandrager's avatar
Frits Vaandrager committed
71
\caption{Mealy machine + associated NuSMV code}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
72 73
\label{fig:nusmvex}
\end{figure}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
74

Erik Poll's avatar
shit  
Erik Poll committed
75

76
The remainder of this section defines the properties we formalized and verified. We group these properties into four categories: 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
77

Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
78
\begin{enumerate}
79
\item \textit{basic characterizing properties}, properties which characterize the {\dmapper} and {\dsut} assembly at a basic level. These hold for all systems.
80
\item \textit{security properties}, these are properties fundamental to achieving the main security goal of the respective layer.
81
\item \textit{key re-exchange properties}, that is properties regarding the key re-exchange operation (after the initial key exchange was done).
82
\item \textit{functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications. They may have a security impact.
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
83
\end{enumerate}
84

85
A key note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstract model, which represents an over-approximation of the {\dsut} induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model, concretization obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Performing model checking on an abstract model means we cannot fully translate model checking results to the concrete (unknown) model of the implementation. In particular, properties which hold for the abstract model do not necessarily hold for the implementation. Properties that don't hold however, also don't hold for the {\dsut}. 
86 87

\newcommand{\dreqauth}{$hasReqAuth$}
88 89 90
\newcommand{\dvauth}{$validAuthReq$}
\newcommand{\dauthreq}{$authReq$}
\newcommand{\diauth}{$invAuthReq$}
91
\newcommand{\dopchan}{$hasOpenedChannel$}
92 93 94 95
\newcommand{\drnewkeys}{$receivedNewKeys$}
\newcommand{\drkex}{$kexStarted$}
\newcommand{\dconnlost}{$connLost$}
\newcommand{\dend}{$endCondition$}
96

97 98 99 100 101 102
\lstset{%
  escapeinside={(*}{*)},%
}

Before introducing the properties, we mention some basic predicates and conventions we use in their definition. The happy flow in SSH consists in a series of steps, the user first exchanges keys, then  requests for the authentication service, followed up by supplying valid credentials and authentication, concluded by opening of a channel. Whereas the first step is complex, the subsequent steps can be captured by the simple predicates {\dreqauth} , {\dvauth} and {\dopchan} respectively. The predicates are defined in terms of the output generated at a given moment, with certain values of this output indicating that the step was performed successfully. For example, \textsc{ch\_open\_success} indicates that a channel has been opened successfully. Sometimes, we also need the input that generated the output, in order to distinguish this step from a different step. In particular, requesting the authentication service is distinguished from requesting the connection service by \textsc{sr\_auth}. 
To these predicates, we add predicates for valid, invalid and all authentication methods, a predicate for the receipt of \textsc{newkeys} from the server, and receipt of \textsc{kexinit}, which can also be seen as initiation of key (re-) exchange. These latter predicates have to be tweaked in accordance with the input alphabet used and with the output the {\dsut} generated (\textsc{kexinit} could be sent in different packaging, either alone, or joined by a different message). Their formulations correspond to the OpenSSH setting. Finally, by {\dconnlost} we define a predicate suggesting that connection was lost, and by {\dend}, the end condition for most higher layer properties.
103
\begin{center}
104
\begin{lstlisting}[basicstyle=\footnotesize]
105 106 107 108 109 110 111 112 113 114
	(*{\dreqauth}*) := inp=SR_AUTH & out=SR_ACCEPT;
	(*{\dvauth}*) := out=UA_PK_OK | out=UA_PW_OK;
	(*{\dopchan}*) := out=CH_OPEN_SUCCESS;
	(*{\dvauth}*) := inp=UA_PK_OK | inp=UA_PW_OK;
	(*{\diauth}*) := inp=UA_PK_NOK|inp=UA_PW_NOK|inp=UA_NONE;
	(*{\dauthreq}*) := validAuthReq | invalidAuthReq;
	(*{\drnewkeys}*) := out=NEWKEYS | out=KEX31_NEWKEYS;
	(*{\drkex}*) := out=KEXINIT;
	(*{\dconnlost}*) := out=NO_CONN | out=DISCONNECT;
	(*{\dend}*) := kexStarted | connLost;
115 116 117
\end{lstlisting}
\end{center}

118

119 120 121 122
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:
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
123
$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. 
124 125


126
%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.
127

128
\subsection{Basic characterizing properties}
129

130
 %cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met. 
Frits Vaandrager's avatar
Frits Vaandrager committed
131 132
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.
133 134 135

\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
136 137
	G (out=NO_CONN -> 
		G (out=NO_CONN | out=CH_MAX | out=CH_NONE) )
138
\end{lstlisting}
139
%\caption{One connection property}
140 141
\label{prop:noconn}
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
142

143
Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a characteristic we touched on in Subsection~\ref{subsec:mapper}. The {\dmapper} maintains a buffer of opened channels and limits its size to 1. From the perspective of the {\dmapper}, a channel is open, and thus added to the buffer, whenever \textsc{ch\_open} is received from the learner, regardless if a channel was actually opened on the {\dsut}. In particular, if after opening a channel via \textsc{ch\_open} an additional attempt to open a channel is made, the {\dmapper} itself responds by \textsc{ch\_max} without querying the {\dsut}. This continues until the {\dlearner} closes the channel by \textsc{ch\_close}, prompting removal of the channel and the sending on an actual CLOSE message to the {\dsut} (hence out!=\textsc{ch\_none}). A converse property can be formulated in a similar way for when the buffer is empty after a \textsc{ch\_close}, in which case subsequent \textsc{ch\_close} messages prompt the {\dmapper} generated \textsc{ch\_none}, until a channel is opened via \textsc{ch\_open} and an actual OPEN message is sent to the {\dsut}. Conjunction of these two behaviors forms Property~\ref{prop:channel}.
144

145 146
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
147 148 149 150 151 152
	(G (inp=CH_OPEN) ->
			X ( (inp=CH_OPEN -> out=CH_MAX)  
				W (inp=CH_CLOSE & out!=CH_NONE) ) ) &
	(G (inp=CH_CLOSE) ->
			X ( (inp=CH_CLOSE -> out=CH_NONE)  
				W (inp=CH_OPEN & out!=CH_MAX) ) ) 
153
\end{lstlisting}
154
%\caption{Mapper induced channel property}
155 156
\label{prop:channel}
\end{property}
157

158
\subsection{Security properties} 
159
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, the authentication service should only become available after exchanging and employing of kryptographic keys (key exchange) was done in the Transport layer, otherwise the service would be running over an unencrypted channel. Requests for this service should therefore not succeed unless key exchange was performed successfully.
160

161
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication necessarily imply successful execution of the key exchange steps. We can tell each key exchange step were successful from the values of the input and output variables. Successful authentication request is indicated by the predicate defined earlier, {\dreqauth}. Following these principles, we define the LTL specification in Property~\ref{prop:sec-trans}, where O is the once operator. Formula $O p$ is true at time $t$ if $p$ held in at least one of the previous time steps $t' \leq t$.
162

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
163

164 165 166
% SR_AUTH_AUTH -> SR_AUTH
% SR_AUTH_CONN -> SR_CONN
% SR_ACCEPT -> SR_ACCEPT
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
167 168


169
\begin{property}
170
\begin{lstlisting}[basicstyle=\footnotesize]
171 172 173 174
	G ( hasReqAuth -> 
			O ( (inp=NEWKEYS & out=NO_RESP) & 
				O ( (inp=KEX30 & out=KEX31_NEWKEYS) & 
					O (out=KEXINIT) ) ) )
175
\end{lstlisting}
176
%\caption{Transport layer security}
177
\label{prop:sec-trans}
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
178
\end{property}
179

180
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 has been opened successfully, captured by the predicate {\dopchan}. Provision of valid/invalid credentials is indicated by the outputs \textsc{ua\_success} and \textsc{ua\_failure} respectively. Along these lines, we formulate this specification by Property~\ref{prop:sec-auth}, where S stands for the since operator. 
181
Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$ held in all times $t''$ such that $t' < t'' \leq t$.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
182

183

184
\begin{property}
185
\begin{lstlisting}[basicstyle=\footnotesize]
186 187
	G ( hasOpenedChannel ->
		out!=UA_FAILURE S out=UA_SUCCESS )
188
\end{lstlisting}
189
%\caption{Authentication layer security}
190
\label{prop:sec-auth}
Paul Fiterau Brostean's avatar
updates  
Paul Fiterau Brostean committed
191
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
192

193
\subsection{Key re-exchange properties}
Frits Vaandrager's avatar
Frits Vaandrager committed
194 195
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.
196
\begin{property}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
197
\begin{lstlisting}[basicstyle=\footnotesize]
198 199
	G ( hasReqAuth -> 
		X (inp=KEXINIT -> out=KEXINIT & 
200 201 202
			X ( inp=KEX30 -> out=KEX31_NEWKEYS & 
				X (inp=NEWKEYS -> out=NO_RESP) ) ) W 
         (connLost | hasAuth ) ) 
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
203
\end{lstlisting}
204
%\caption{Rekey possible in pre-auth. state}
205
\label{prop:rpos-pre-auth}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
206
\end{property}
Frits Vaandrager's avatar
Frits Vaandrager committed
207 208
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.
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
209

210 211 212 213 214 215 216 217 218 219 220 221
%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.
%
%\begin{property}[h]
%\begin{lstlisting}[basicstyle=\footnotesize]
%	G ( hasReqAuth ->
%		( (inp=NEWKEYS & out=NO_RESP & X inp=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:rper-pre-auth}
%\end{property}
222

223
%\textit{Perhaps this could be merged into one property?}
224

225
\subsection{Functional properties}
Frits Vaandrager's avatar
Frits Vaandrager committed
226
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
227 228
expected outputs after a \textsc{disconnect}.

229
\begin{property}
230 231 232 233
\begin{lstlisting}[basicstyle=\footnotesize]
	G ( out=DISCONNECT -> 
		X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
234
%\caption{No output after DISCONNECT}
235 236 237 238
\label{prop:trans-disc}
\end{property}


239
The RFC states in~\cite[p. 24]{rfc4254} that after sending a \textsc{kexinit} message, a party MUST not send another \textsc{kexinit}, or a \textsc{sr\_accept} message, until it has sent a \textsc{newkeys} message(\drnewkeys). This is translated to Property~\ref{prop:trans-kexinit}.  
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
240 241


242
\begin{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
243
\begin{lstlisting}[basicstyle=\footnotesize]
244 245
	G ( out=KEXINIT -> 
		X ( (out!=SR_ACCEPT & out!=KEXINIT) 
246
			W receivedNewKeys )	)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
247
\end{lstlisting}
248 249
%\caption{Disallowed outputs after KEXINIT}
%\captionsetup{font=small}
250
\label{prop:trans-kexinit}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
251 252
\end{property}

253
The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service request, ``it SHOULD send an appropriate SSH\_MSG\_DISCONNECT message and MUST disconnect''. Moreover, in case it supports the service request, it MUST send a \textsc{sr\_accept} message. Unfortunately, it is not evident from the specification if rejection and support are the only allowed outcomes. We assume that is the case, and formalize an LTL formula accordingly by Property~\ref{prop:trans-sr}. For any service request (\textsc{sr\_auth} or \textsc{sr\_conn}, in case we are not in the initial state, the response will be either an accept (\textsc{sr\_accept}), disconnect (\textsc{disconnect}) which loses the connection in the next step, or \textsc{no\_conn}, the output generated by the {\dmapper} after the connection is lost. We adjusted the property for the initial state since all implementations responded with \textsc{kexinit} which would easily break the property. We cannot yet explain this behavior.
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
254
% , with the adjustment that we also allow the mapper induced output \textsc{no\_conn}, which suggests that connection was lost. Additionally, we exclude the initial state from the implication, as it is the only state where a \textsc{kexinit} is generated as a response, which seems to be the default behavior for all implementations.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
255

256
\begin{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
257
\begin{lstlisting}[basicstyle=\footnotesize]
258
	G ( (inp=SR_AUTH & state!=s0) ->
259
	(out=SR_ACCEPT | out=DISCONNECT | out=NO_CONN )))
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
260
\end{lstlisting}
261
%\caption{Allowed outputs after SR\_ACCEPT}
262
\label{prop:trans-sr}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
263 264
\end{property}

265

266 267 268

%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}

269
The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the server rejects the authentication request, it MUST respond with a \textsc{ua\_failure} message. Rejected requests are suggested by the predicate {\diauth}. In case of requests with valid credentials (\dvauth), a \textsc{ua\_success} MUST be sent only once. While not explicitly stated, we assume this to be in a context where the authentication service had been successfully requested, hence we use the {\dreqauth} predicate. We define two properties, Property~\ref{prop:auth-pre-ua} for behavior before an \textsc{ua\_success}, Property~\ref{prop:auth-post-ua-strong} for behavior afterward. For the first property, note that (\dreqauth) may hold even after successful authentication, but we are only interested in behavior between the first time (\dreqauth) holds and the first time authentication is successful (out=\textsc{ua\_success}), hence the use of the O operator. As is the case with most higher layer properties, the first property only has to hold until the end condition holds(\dend), that is the connection is lost(\dconnlost) or rekey was started by the {\dsut} (\drkex).
270
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}. 
271
\begin{property}
272
\begin{lstlisting}[basicstyle=\footnotesize]
273 274 275
G ( (hasReqAuth & !O out=UA_SUCCESS) ->
    (invalidAuthReq -> (out=UA_FAILURE) ) 
		W (out=UA_SUCCESS | endCondition ) )
276
\end{lstlisting}
277
%\caption{Invalid requests prompt UA\_FAILURE }
278
\label{prop:auth-pre-ua}
279 280
\end{property}

281
\begin{property}
282
\vspace{-4mm}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
283
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
284
G ( out=UA_SUCCESS -> X G out!=UA_SUCCESS)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
285
\end{lstlisting}
286
%\caption{UA\_SUCCESS is sent at most once}
287
\label{prop:auth-post-ua-strong}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
288 289
\end{property}

290
In the same paragraph, it is stated that authentication requests received after a \textsc{ua\_success} SHOULD be ignored. This is a weaker statement, and it requires that all authentication messages (suggested by {\dauthreq}) after a \textsc{ua\_success} output should prompt no response from the system(\textsc{no\_resp}) until the end condition is true. The formulation of this statement shown in Property~\ref{prop:auth-post-ua}. 
291
\begin{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
292
\begin{lstlisting}[basicstyle=\footnotesize]
293
	G ( out=UA_SUCCESS -> 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
294
		X ( ( authReq-> out=NO_RESP ) W endCondition ) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
295
\end{lstlisting}
296
%\caption{Silence after UA\_SUCCESS}
297
\label{prop:auth-post-ua}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
298
\end{property}
299
%\textit{Perhaps this could also be merged into one property?}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
300

301
The Connection layer RFC states in \cite[p. 9]{rfc4254} that upon receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close} message, unless it had already sent this message for the channel. The channel must have been opened beforehand (\dopchan) and the property only has to hold up to when the end condition holds or the channel was closed(\textsc{ch\_close}). Along these lines we formulate Property~\ref{prop:conn-close}. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
302

303
\begin{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
304
\begin{lstlisting}[basicstyle=\footnotesize]
305 306 307
G ( hasOpenedChannel -> 
	( (inp=CH_CLOSE) -> (out=CH_CLOSE) ) 
	W ( endCondition | out=CH_CLOSE) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
308
\end{lstlisting}
309
%\caption{CH\_CLOSE response on CH\_CLOSE request}
310
\label{prop:conn-close}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
311
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
312 313


314
%A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a \textsc{kexinit} message, a party MUST not send \textsc{service\_request} or \textsc{sr\_accept} messages, until it has sent a \textsc{newkeys} message. This is translated to the LTL.
315

316
%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
317

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
318
%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. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
319 320 321
\newcommand{\dt}{\color{green}\checkmark}
\newcommand{\dfce}[1]{\color{red}X}
\newcommand{\df}{\color{red}X}
322

323 324

\subsection{Model checking results}
Frits Vaandrager's avatar
Frits Vaandrager committed
325
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. For BitVise,
326 327 328
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. 

329
%\begin{center}\small
330
%	\centering
Frits Vaandrager's avatar
Frits Vaandrager committed
331
\begin{table}[h!]
332 333
	\centering
	\small
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
334
	\begin{tabular}{| l | l | c | c |c | c |}
335
		\hline 
336
		          &   					 																	&		          & 		\multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{4-6} 					
Frits Vaandrager's avatar
Frits Vaandrager committed
337
							&   Property 	 																	&	Key word &\tiny{OpenSSH}	                 		& \tiny{Bitvise}              & \tiny{DropBear} \\ \hline 
338
		Security  &   Trans. 		 																	&		          & \dt  		                 		& \dt                  & \dt                					  \\ \cline{3-6} 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
339
		    			&   Auth.      																	&		          & \dt	 		                 		& \dt                  & \dt                					  \\ \hline 
Frits Vaandrager's avatar
Frits Vaandrager committed
340 341 342 343 344
		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}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
345 346 347 348
		    			&   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		                 			& \dt                  & \dfce{sends CH\_EOF}						\\ \hline 		
349
	\end{tabular}
Paul Fiterau Brostean's avatar
updated  
Paul Fiterau Brostean committed
350
	\caption{Model checking results}
351
	\label{tab:mcresults}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
352
	\vspace{-5mm}
353 354
\end{table}
%\end{center}
355

Frits Vaandrager's avatar
Frits Vaandrager committed
356 357 358 359
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.
360

Frits Vaandrager's avatar
Frits Vaandrager committed
361 362 363 364
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}.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
365 366

%, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.