Commit 0e7220a6 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Figure increased to scale 0.27

parent 7ff080f1
......@@ -11,7 +11,7 @@ We have adapted the setting off timing parameters to each implementation.
\begin{figure*}
\centering
\includegraphics[scale=0.25]{ssh-server_cropped}
\includegraphics[scale=0.27]{ssh-server_cropped}
\caption{Model of the OpenSSH server. {\normalfont States are collected in 3 clusters,
indicated by the rectangles, where each cluster corresponds to
one of the protocol layers.
......@@ -73,8 +73,8 @@ is possible. Many states were also added due to {\dmapper} generated outputs suc
Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with some edits to improve readability. The happy flow, in green, is fully explored in the model and mostly matches our earlier description of it\footnote{The only exception is in the Transport layer, where unlike in our happy flow definition, the server is the first to send the \textsc{newkeys} message. This is also accepted behavior, as the protocol does not specify which side should send \textsc{newkeys} first.}. Also explored is what happens when a rekeying sequence is attempted. We notice that rekeying is only allowed in states of the Connection layer. Strangely, for these states, rekeying is not state preserving, as the generated output on receiving a \textsc{sr\_auth}, \textsc{sr\_conn} or \textsc{kex30} changes from \textsc{unimpl} to \textsc{no\_resp}. This leads to two sub-clusters of states, one before the first rekey, the other afterward. In all other states, the first step of a
rekeying (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect.
We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of an explicit service request. That in itself was not strange, because authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
What was strange was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected on requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
We were puzzled by how systems reacted to \textsc{sr\_conn}, the request for services of the Connection layer. These services can be accessed once the user had authenticated, without the need of a prior service request. That in itself was not strange, as authentication messages already mention that connection services should start after authentication \footnote{This is a technical detail, the message format of authentication messages requires a field which says the service started after authentication. The only option is to start Connection layer services. }.
Unexpected was that an explicit request either lead to \textsc{unimpl}/\textsc{no\_resp} with no state change, as in the case of OpenSSH, or termination of the connection, as in the case of BitVise. The latter was particularly strange, as in theory, once authenticated, the user should always have access to the service, and not be disconnected on requesting this service. Only DropBear seems to respond positively (\textsc{sr\_accept}) to \textsc{sr\_conn} after authentication.
We also notice the intricate authentication behavior:
after an unsuccessful authentication attempt the only authentication method still allowed is password authentication. Finally, only BitVise allowed multiple terminals to be requested over the same channel. As depicted in the model, OpenSSH abruptly terminates on requesting a second terminal. DropBear exhibits a similar behavior.
......
......@@ -175,11 +175,7 @@ the older ones, if such existed.
The {\dmapper} contains a buffer for storing channels opened, 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
(if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially,
the buffer is empty.
Lastly, 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.
(if there was any). The buffer size, or the maximum number of opened channels, is limited to one. Initially the buffer is empty. Lastly, 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
instead of being sent to the {\dsut} to find out its response: (1) on receiving a \textsc{ch\_open} input
......
......@@ -46,7 +46,7 @@ the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~
Here learning is viewed as a game in which a \textit{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a Mealy machine $\M$,
also called the System Under Learning ({\dsut}).
Initially, the {\dlearner} only knows the input alphabet $I$ and output alphabet $O$ of $\M$.
The task of the learner is to learn $\M$ via two types of queries:
The task of the {\dlearner} is to learn $\M$ via two types of queries:
\begin{itemize}
\item
With a \emph{membership query}, the learner asks what the response is to an input sequence $\sigma \in I^{\ast}$.
......
......@@ -80,9 +80,9 @@ This function updates the output and state variables for a given valuation of th
The remainder of this section defines the properties we formalized and verified. We group these properties into four categories:
\begin{enumerate}
\item \textit{basic characterizing properties}, properties which characterize the {\dmapper} and {\dsut} assembly at a basic level. These hold for all systems.
\item \textit{basic characterizing properties}, properties which characterize the {\dmapper} and {\dsut} assembly at a basic level. These hold for all implementations.
\item \textit{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{key re-exchange properties}, or properties regarding the rekey operation (after the initial key exchange was done).
\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}
......@@ -195,7 +195,7 @@ Formula $p S q$ is true at time $t$ if $q$ held at some time $t' \leq t$ and $p$
\end{property}
\subsection{Key re-exchange properties}
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
According to the RFC \cite[p. 24]{rfc4254}, re-exchanging keys (or rekeying) (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.
\begin{property}
\begin{lstlisting}[basicstyle=\footnotesize]
......
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