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

Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
3
4
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
5

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
6
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
7
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.  
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
8

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
9
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
10
11
12


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


Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
15
\begin{enumerate}
16
17
18
\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 re-exchange operation (after the initial key exchange was done).
\item \textit{basic 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
19
\end{enumerate}
20

21
22
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}. 
 %cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
23

24
Since we are checking the model of a {\dsut} and {\dmapper} assemble, we had to account for the {\dmapper} induced behavior when formalizing specifications. In particular, once connection with the server is lost, it cannot be recovered and the {\dmapper} will itself respond with \textsc{no\_conn} to any subsequent inputs sent by the {\dlearner}. For this reason, several formulas follow a pattern where a property should hold until the connection is lost, captured by the predicate \textsc{out} = \textsc{no\_conn} .
25

26
27
\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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
28

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
29
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.
30
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. 
31

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
32
33
34
35
36
37

% SERVICE_REQUEST_AUTH -> SR_AUTH
% SERVICE_REQUEST_CONN -> SR_CONN
% SERVICE_REQUEST_CONN -> SR_CONN


Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
38
\begin{property}[h]
39
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
40
41
42
43
44
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) ) ) )
45
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
46
\caption{Transport layer security.}
Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
47
48
\label{prop:prop1}
\end{property}
49

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
50
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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
51

52

Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
53
\begin{property}[h]
54
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
55
56
G ( (in=CH_OPEN & out=CH_OPEN_SUCCESS) ->
	(!(out=UA_FAILURE) S out=UA_SUCCESS) )
57
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
58
\caption{Authentication layer security.}
Paul Fiterau Brostean's avatar
updates    
Paul Fiterau Brostean committed
59
60
\label{prop:prop2}
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
61

62
\subsection{Key re-exchange properties}
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
63
Important properties are that re-exchanging keys (or rekey-ing) is allowed in all states of the protocol, and its successful execution doesn't change the protocol state\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. For each state, we specify the properties that rekey-ing (1) should always be allowed from that state, and (2) when allowed, should always preserve the state, until connection is lost. We can tell we are in one of these states from the input/output transition leading up to it. These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we note great variance on satisfaction of these properties. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
64

Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
65
66
67
68

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]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
69
70
71
72
G ( (in=SR_AUTH & out=SERVICE_ACCEPT) -> 
	X (in=KEXINIT -> out=KEXINIT & 
		X (in=KEX30 -> out=KEX31_NEWKEYS & 
			X (in=NEWKEYS -> out=NO_RESP) ) ) ) 
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
73
74
75
76
77
78
\end{lstlisting}
\caption{Key exchange possible in pre-auth. state}
\label{prop:prop25}
\end{property}

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 via successful authentication (\textsc{ua\_success}). The latter is described in Property~\ref{prop:prop3}. 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.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
79
80
81

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
82
83
84
85
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) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
86
\end{lstlisting}
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
87
\caption{Key exchange preserves pre-auth. state}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
88
89
\label{prop:prop3}
\end{property}
90

Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
91
\textit{Perhaps this could be merged into one property?}
92

93
94
\subsection{Basic functional properties}
We have also formalized and checked properties drawn from the RFC specifications. We found parts of the specification vague, which sometimes meant that we had to give our own interpretation before we could formalize. 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{service\_accept} message, until it has sent a \textsc{newkeys} message. This is translated to Property~\ref{prop:prop4}. Note that \textsc{kex31\_newkeys} suggests that the {\dsut} sends a \textsc{kex31}, followed by a \textsc{newkeys}, so it depicts a case where \textsc{newkeys} was sent.
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
95
96
97
98


\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
99
100
101
G ( (out=KEXINIT) -> 
	X ( (out!=SERVICE_ACCEPT & out!=KEXINIT) 
		W (out=NEWKEYS | out=KEX31_NEWKEYS) )	)
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
102
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
103
104
\caption{Disallowed outputs after KEXINIT}
\captionsetup{font=small}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
105
106
107
\label{prop:prop4}
\end{property}

Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
108
109
110
On the same page, it is stated 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{service\_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:prop5}. For any service request, in case connection wasn't lost (\textsc{no\_conn}) or we are not in the initial state, the response will either be
an accept(\textsc{service\_accept}) or a disconnect(\textsc{disconnect})  which loses the connection. 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.
% , 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
111
112
113

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
114
115
116
G ( (in=SR_AUTH & out!=NO_CONN & state!=s0) 
-> (out=SERVICE_ACCEPT | (out=DISCONNECT & 
		X G (in=SERVICE_REQUEST -> out=NO_CONN) ) ) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
117
118
119
120
121
\end{lstlisting}
\caption{Allowed outputs after SERVICE\_ACCEPT}
\label{prop:prop5}
\end{property}

Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
122
%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
123

124
125
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. Conversely, if the requests succeeds, a \textsc{ua\_success} MUST be sent only once. Authentication requests received thereafter SHOULD be ignored. While not explicitly stated, we assume this to be in a context where the authentication service had been successfully requested. We define two properties, Property~\ref{prop:prop6} for behavior before an \textsc{ua\_success}, Property~\ref{prop:prop7} for behavior afterward, until the connection is lost.
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
126
127
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
128
129
130
131
 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) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
132
\end{lstlisting}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
133
\caption{UA\_SUCCESS is sent at most once}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
134
135
136
137
138
\label{prop:prop6}
\end{property}

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
139
140
141
G (out=UA_SUCCESS -> 
	X ( ( (in =UA_PK_OK | in=UA_PK_NOK) -> out=NO_RESP ) 
		W out=NO_CONN ) )
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
142
\end{lstlisting}
143
\caption{Silently ignore auth. requests after UA\_SUCCESS}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
144
145
\label{prop:prop7}
\end{property}
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
146
\textit{Perhaps this could also be merged into one property?}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
147

Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
148
The Connection Layer RFC states that upon receiving a \textsc{ch\_close} message, a side SHOULD send back a \textsc{ch\_close} message, unless it had already sent this message for the channel. The channel must have been opened beforehand. Also, this condition no longer applies once the connection is lost (\textsc{no\_conn}), once a re-key procedure was initiated (by input \textsc{kexinit}) or once the channel was closed. Along those lines we formulate Property~\ref{prop:prop8}. 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
149
150
151

\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
152
153
154
155
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) ) 
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
156
157
158
159
\end{lstlisting}
\caption{CH\_CLOSE request is followed by CH\_CLOSE response}
\label{prop:prop8}
\end{property}
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
160
161


Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
162
%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{service\_accept} messages, until it has sent a \textsc{newkeys} message. This is translated to the LTL.
163

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
164
%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{service\_accept} message. If
165

Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
166
%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. 
167
168

\subsection{Model checking results}
169
170
Table~\ref{tab:mcresults} presents model checking results. Crucially, all the critical security properties hold. 
%\begin{center}\small
171
%	\centering
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
172
\begin{table}
173
174
	\centering
	\small
Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
175
	\begin{tabular}{| r | r | c |c | c |}
176
		\hline 
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
177
		          &   					 & 		\multicolumn{3}{c|}{\emph{SSH Implementation}}\\ \cline{3-5} 					
178
179
180
181
182
183
184
185
186
187
							&   Property 	 & OpenSSH	& Bitvise	& Dropbear \\ \hline 
		Critical  &   Trans. 		 &          & 				& 				 \\ \cline{2-5}
		    			&   Auth.      &  				& 				& 				 \\ \hline 
		Rekey 		&   Pre-auth.  &  				&         &          \\ \cline{2-5}
		    			&   Auth.      &  				&         &          \\ \hline 
		Functional&   Prop. 5    &  				&         &          \\ \cline{2-5} 
		    			&   Prop. 6    &  				&         &          \\ \cline{2-5}
		    			&   Prop. 7    &  				&         &          \\ \cline{2-5}
		    			&   Prop. 8    &  				&         &          \\ \hline 		
	\end{tabular}
Paul Fiterau Brostean's avatar
updated    
Paul Fiterau Brostean committed
188
	\caption{Model checking results}
189
190
191
	\label{tab:mcresults}
\end{table}
%\end{center}
192
193


Paul Fiterau Brostean's avatar
Paul Fiterau Brostean committed
194
195

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