Commit a7a9048f authored by Erik Poll's avatar Erik Poll
Browse files

fixed some times & condensed

parent 7145da0a
......@@ -9,10 +9,10 @@ Abstraction was provided by a {\dmapper} component placed between the
{\dlearner} and the {\dsut}. The {\dmapper} was constructed from an
existing SSH implementation. The input alphabet of the {\dmapper}
explored key exchange, setting up a secure connection, several
authentication methods and opening and closing channels over which the
authentication methods, and opening and closing channels over which the
terminal service could be requested. We used two input alphabets, a
full version for OpenSSH, and a restricted version for the other
implementations. The restricted alphabet was still sufficient to
full version for OpenSSH, and a restricted version for Bitvise and
DropBear. The restricted alphabet was still sufficient to
explore most aforementioned behavior.
We encountered several challenges. Firstly, building a {\dmapper} presented a considerable technical challenge, as it required re-structuring of an actual
......
......@@ -86,7 +86,7 @@ also used model checkers \cite{TCP2016,Chalupar2014Automated}.
Instead of using active learning as we do, it is also possible to use
passive learning to obtain protocol state machines
\cite{Wang2011Inferring}. Here network traffic is observed, and not
actively generated. This can then also provide a probabilistic
actively generated. This can then provide a probabilistic
characterization of normal network traffic, but it cannot uncover
implementation flaws that occur in strange message flows, which is our
goal.
......
......@@ -21,8 +21,9 @@ We have adapted the setting of timing parameters to each implementation.
\end{figure*}
OpenSSH was learned using a full alphabet, whereas DropBear and BitVise were learned using a restricted alphabet (as defined in Subsection~\ref{subsec:alphabet}).
The main reason for using a restricted alphabet reduce learning times. Based on the model learned for OpenSSH (the first implementation analyzed) and the specification, we excluded
inputs that seemed unlikely to produce state change (like \textsc{debug} or \textsc{unimpl}). We also excluded inputs that proved costly time-wise (like \textsc{disconnect}), yet were not were not needed to visit all states in our happy flow. We excluded, for example, the user/password based authentication inputs (\textsc{ua\_pw\_ok} and
The reason for using a restricted alphabet was to reduce learning times. Based on the model learned for OpenSSH (the first implementation analyzed) and the specification, we excluded
inputs that seemed unlikely to produce state change (such as
\textsc{debug} or \textsc{unimpl}). We also excluded inputs that proved costly time-wise (such as \textsc{disconnect}) but were not were not needed to visit all states in the happy flow. We excluded, for example, the user/password based authentication inputs (\textsc{ua\_pw\_ok} and
\textsc{ua\_pw\_nok}) as they would take the system 2-3 seconds to respond to. By contrast, public key authentication resulted in quick responses.
%The \textsc{disconnect} input presented similar
......@@ -45,8 +46,8 @@ can be set to higher values. We executed a random test suite with {\dk} of 4 com
%To that end, we built a java adapter that would automatically run the model checker on the hypothesis, and transform any counterexamples into tests. This proved essential in learning DropBear, as the last counterexample was generated by the model checker.
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing, namely:
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models plus the specifications checked can be found at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}. The statistics
Table~\ref{tab:experiments} describes the exact versions of the systems analyzed together with statistics on learning and testing:
(1) the number of states in the learned model, (2) the number of hypotheses built during the learning process and (3) the total number of learning and test queries run. For test queries, we only consider those run on the last hypothesis. All learned models and the properties checked are at \url{https://gitlab.science.ru.nl/pfiteraubrostean/Learning-SSH-Paper/tree/master/models}. The statistics
give a glimpse into the issue of scalability. Assuming each input took 0.5 seconds to process, and an average query length of 10, to perform 40000 queries would have taken roughly 55 hours. This is consistent with the time experiments took, which span several days. The long duration compelled us to resort to restricted alphabets, which lead to reduction in the number of queries needed. Our work could have benefited from parallel execution.
%BitVise: MemQ: 24996 TestQ: 58423
%Dropbear: MemQ: 3561 TestQ: 30629
......
......@@ -100,7 +100,7 @@ convey its own parameter preferences before key exchange can proceed. Also inclu
\label{trans-alphabet}
\end{table}
The Authentication layer defines one single client message type in the form of the authentication request~\cite[p. 4]{rfc4252}. Its parameters contain all information needed for authentication. Four authentication methods exist: none, password, public key and host-based. Our mapper supports all methods except the host-based authentication because some SUTs don't support this feature. Both the public key and password methods have \textsc{ok} and \textsc{nok} variants, which provide respectively correct and incorrect credentials. Our restricted alphabet supports only public key authentication, as the implementations processed this faster than the other authentication methods.
The Authentication layer defines a single client message type for the authentication requests~\cite[p. 4]{rfc4252}. Its parameters contain all information needed for authentication. Four authentication methods exist: none, password, public key and host-based. Our mapper supports all methods except host-based authentication because some SUTs don't support this feature. Both the public key and password methods have \textsc{ok} and \textsc{nok} variants, which provide respectively correct and incorrect credentials. Our restricted alphabet supports only public key authentication, as the implementations processed this faster than the other authentication methods.
\begin{table}[!ht]
\centering
......@@ -118,9 +118,9 @@ The Authentication layer defines one single client message type in the form of t
\label{auth-alphabet}
\end{table}
The Connection layer allows the client to manage channels and to request/run services over them. In accordance with our learning goal,
The Connection layer allows clients to manage channels and request services over them. In accordance with our learning goal,
our mapper only supports inputs for requesting terminal emulation, plus inputs for channel management as shown in Table~\ref{conn-alphabet}.
The restricted alphabet only supports the most general channel management inputs. Those excluded are not expected to produce state change.
The restricted alphabet only supports the most general channel management inputs, and excludes those not expected to produce state change.
\begin{table}[!ht]
......@@ -141,7 +141,7 @@ The restricted alphabet only supports the most general channel management inputs
\label{conn-alphabet}
\end{table}
\emph{The output alphabet} subsumes all messages an SSH server generates, which may include, with identical meaning, any of the messages defined as inputs. They also include responses to various requests: \textsc{kex31}~\cite[p. 21]{rfc4253} as reply to \textsc{kex30}, \textsc{sr\_succes} in response to service requests (\textsc{sr\_auth} and \textsc{sr\_conn}), \textsc{ua\_success} and \textsc{ua\_failure}~\cite[p. 5,6]{rfc4252} in response to authentication requests, and \textsc{ch\_open\_success}~\cite[p. 6]{rfc4254} and \textsc{ch\_success}~\cite[p. 10]{rfc4254} , in positive response to \textsc{ch\_open} and \textsc{ch\_request\_pty} respectively. To these outputs, we add \textsc{no\_resp} for when the {\dsut} generates no output, and the special outputs \textsc{ch\_none}, \textsc{ch\_max} and \textsc{no\_conn}, and \textsc{buffered}, which we discuss in the next Subsections.
\emph{The output alphabet} includes all messages an SSH server generates, which may include, with identical meaning, any of the messages defined as inputs. This also includes responses to various requests: \textsc{kex31}~\cite[p. 21]{rfc4253} as reply to \textsc{kex30}, \textsc{sr\_succes} in response to service requests (\textsc{sr\_auth} and \textsc{sr\_conn}), \textsc{ua\_success} and \textsc{ua\_failure}~\cite[p. 5,6]{rfc4252} in response to authentication requests, and \textsc{ch\_open\_success}~\cite[p. 6]{rfc4254} and \textsc{ch\_success}~\cite[p. 10]{rfc4254} , in positive response to \textsc{ch\_open} and \textsc{ch\_request\_pty} respectively. To these outputs, we add \textsc{no\_resp} for when the {\dsut} generates no output, and the special outputs \textsc{ch\_none}, \textsc{ch\_max} and \textsc{no\_conn}, and \textsc{buffered}, which we discuss in the next subsections.
%The learning alphabet comprises of input/output messages by which the {\dlearner} interfaces with the {\dmapper}. Section~\ref{sec:ssh} outlines essential inputs, while Table X provides a summary
%of all messages available at each layer. \textit{\textit{}}
......@@ -160,7 +160,9 @@ is the \textsc{no\_resp} message.
The sheer complexity of the {\dmapper} meant that it was easier to
adapt an existing SSH implementation, rather than construct the
{\dmapper} from scratch. Paramiko already provides mechanisms for
{\dmapper} from scratch.
After all, in many ways the {\dmapper} acts similar to an SSH client.
Paramiko already provides mechanisms for
encryption/decryption, as well as routines for constructing and
sending the different types of packets, and for receiving them. These
routines are called by control logic dictated by Paramiko's own state
......@@ -186,7 +188,7 @@ negotiated earlier in place of the older ones, if such existed.
The {\dmapper} also contains a buffer for storing opened channels, which is initially empty.
On a \textsc{ch\_open} from the learner, the {\dmapper} adds a channel to the buffer
with a randomly generated channel identifier, on a \textsc{ch\_close}, it removes the channel
with a randomly generated channel identifier; on a \textsc{ch\_close}, it removes the channel
(if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. The {\dmapper} also stores the sequence number of the last received message from the {\dsut}. This number is then used when constructing \textsc{unimpl} inputs.
In the following cases, inputs are answered by the {\dmapper} directly
......@@ -204,8 +206,6 @@ responds with a \textsc{no\_conn} message, as sending further messages to the {\
% messages to the {\dsut} is pointless in that case;
%\end{enumerate}
%
In many ways, the {\dmapper} acts similar to an SSH client, hence the
decision to built it by adapting an existing client implementation.
\subsection{Practical complications}
......@@ -278,7 +278,7 @@ complete are all these messages processed. This leads to a
\textsc{newkeys} response (indicating rekeying has completed),
directly followed by all the responses to the buffered requests. This
would lead to non-termination of the learning algorithm, as for every
sequence of buffered messages the response is different. To
sequence of buffered messages the response differs. To
prevent this, we treat the sequence of queued responses as the single
output \textsc{buffered}.
......
......@@ -92,8 +92,8 @@ tabsize=2
\begin{abstract}
We apply model learning on three SSH implementations to infer state machine models, and then use model checking
to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that
all tested SSH server models satisfy the stated security properties.
However, our analysis uncovered several violations of the standard.
all tested SSH server models satisfy the stated security properties,
but uncovered several violations of the standard.
%Frits: I would say the fingerprinting is a detail, standard violations much more important.
%The state machines of the implementations differ significantly, allowing them to be
%effectively fingerprinted.
......
......@@ -8,7 +8,7 @@
%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.
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.
A NuSMV model is specified by 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.
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 its associated NuSMV model.
%\parbox{\columnwidth}{
......@@ -86,7 +86,7 @@ The remainder of this section defines the properties we formalized and verified.
\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.
\end{enumerate}
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}.
A key point to 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 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}.
\newcommand{\dreqauth}{$hasReqAuth$}
\newcommand{\dvauth}{$validAuthReq$}
......@@ -102,8 +102,8 @@ A key note is that properties are checked not on the actual concrete model of th
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 (1) exchanges keys, (2) requests for the authentication service, (3) supplies valid credentials to authenticate and finally (4) opens a channel. Whereas step (1) 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, so as 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 condition after which higher layer properties no longer have to hold.
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 (1) exchanges keys, (2) requests for the authentication service, (3) supplies valid credentials to authenticate and finally (4) opens a channel. Whereas step (1) 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, so as to distinguish this step from other steps. 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 last 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 below are for the OpenSSH server. Finally, {\dconnlost} indicates that connection was lost, and {\dend} is the condition after which higher layer properties no longer have to hold.
\begin{center}
\begin{lstlisting}[basicstyle=\footnotesize]
(*{\dreqauth}*) := inp=SR_AUTH & out=SR_ACCEPT;
......@@ -124,7 +124,7 @@ 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:
$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 advise implementations to reject all higher layer inputs, regardless of the state before the rekey.
$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 RFCs don't specify what should happen when no connection exists. Moreover, higher layer properties in the RFCs only apply outside of rekey sequences, as inside a rekey sequence the RFCs advise implementations to reject all higher layer inputs, regardless of the state before the rekey.
%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.
......@@ -132,7 +132,7 @@ $p\,W\,q\, =\, p \,U\, q\, | \, G\, p$. Many of the higher layer properties we
\subsection{Basic characterizing properties}
%cannot be translated. %Though in practical terms, these results are still translatable, in particular for cases where properties are not met.
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 cannot be re-established. The moment
In our setting, a single TCP connection is made and once this connection is lost (e.g.\ because the system disconnects) it cannot 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.
\begin{property}%[h]
......@@ -144,7 +144,7 @@ a connection is lost is marked by generation of the \textsc{no\_conn} output. F
\label{prop:noconn}
\end{property}
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 open 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}.
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 open 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 of 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}.
\begin{property}%[h]
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -160,9 +160,9 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\end{property}
\subsection{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, 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.
In SSH, upper layer services rely on security guarantees ensured by lower layers. So these services should not be available before the lower layers have completed. For example, the authentication service should only become available \emph{after} a successful key exchange and the seting up of a secure tunnel by 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.
Key exchange implies three steps which have to be performed in order but may be interleaved by other actions. Successful authentication necessarily implies successful execution of the key exchange steps. We can tell each key exchange step was 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$.
Key exchange involves three steps that have to be performed in order but may be interleaved by other actions. Successful authentication necessarily implies successful execution of the key exchange steps. We can tell each key exchange step was 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$.
% SR_AUTH_AUTH -> SR_AUTH
......@@ -181,7 +181,7 @@ Key exchange implies three steps which have to be performed in order but may be
\label{prop:sec-trans}
\end{property}
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 as 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.
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 as a state where a channel has been opened successfully, described 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.
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$.
......@@ -227,7 +227,7 @@ We therefore checked this requirement directly, by writing a simple script which
%\textit{Perhaps this could be merged into one property?}
\subsection{Functional properties}
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
We 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. 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
expected outputs after a \textsc{disconnect}.
\begin{property}
......@@ -270,7 +270,7 @@ The RFC also states \cite[p. 24]{rfc4254} that if the server rejects the service
%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}
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).
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).
%Indeed, before reaching this state, implementations replied with \textsc{unimplemented}.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -302,7 +302,7 @@ In the same paragraph, it is stated that authentication requests received after
\end{property}
%\textit{Perhaps this could also be merged into one property?}
The Connection layer RFC states in \cite[p. 9]{rfc4254} that on receiving a \textsc{ch\_close} message, a side MUST send back a \textsc{ch\_close}, 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 until the end condition holds or the channel was closed(\textit{out=CH\_CLOSE}). We formulate Property~\ref{prop:conn-close} accordingly.
The Connection layer RFC states in \cite[p. 9]{rfc4254} that on receiving a \textsc{ch\_close} message, a party MUST send back a \textsc{ch\_close}, 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 until the end condition holds or the channel was closed (\textit{out=CH\_CLOSE}). We formulate Property~\ref{prop:conn-close} accordingly.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
......@@ -328,7 +328,7 @@ G ( hasOpenedChannel ->
\subsection{Model checking results}
Table~\ref{tab:mcresults} presents model checking results. Crucially, the security properties hold for all three implementations. We had to slightly adapt our properties for BitVise
as it buffered all responses during rekey (incl. \textsc{UA\_SUCCESS}).
In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} to suggest successful authentication.
In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} as sign of successful authentication.
%\begin{center}\small
% \centering
......@@ -359,10 +359,10 @@ In particular, we used {\dvauth} instead of \textit{out=UA\_SUCCESS} to suggest
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.
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.
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all Transport and Authentication layer specifications, however,
DropBear is the only implementation that allows rekeying in both general states of the protocol. DropBear also satisfies all Transport and Authentication layer specifications, however,
problematically, it violates the property of the Connection layer. Upon receiving \textsc{ch\_close}, it responds by \textsc{ch\_eof} instead of \textsc{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
%~\ref{prop:auth-post-ua}.
......
......@@ -251,7 +251,6 @@ machine learning algorithms},
abstract = {The secure shell ({SSH}) protocol is one of the most popular cryptographic protocols on the Internet. Unfortunately, the current {SSH} authenticated encryption mechanism is insecure. In this paper, we propose several fixes to the {SSH} protocol and, using techniques from modern cryptography, we prove that our modified versions of {SSH} meet strong new chosen-ciphertext privacy and integrity requirements. Furthermore, our proposed fixes will require relatively little modification to the {SSH} protocol and to {SSH} implementations. We believe that our new notions of privacy and integrity for encryption schemes with stateful decryption algorithms will be of independent interest.},
author = {Bellare, M. and Kohno, T. and Namprempre, C.},
journal = {ACM Trans. Inf. Syst. Secur.},
month = may,
number = {2},
pages = {206--241},
publisher = {ACM},
......@@ -357,7 +356,7 @@ machine learning algorithms},
author = {Aarts, F. and Ruiter, J. {de} and Poll, E.},
booktitle = {Software Testing, Verification and Validation Workshops (ICSTW)},
pages = {461--468},
publisher = {IEEE CS},
publisher = {IEEE},
title = {Formal Models of Bank Cards for Free},
year = {2013}
}
......
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