Commit a30030d7 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Removed a kexinit input, relabelling in learned models

parent 6209b4aa
......@@ -16,12 +16,12 @@ like a deterministic Mealy Machine. Herein, time induced non-determinism was di
leading to a considerable increase in the number of states. Moreover, the systems analyzed were relatively slow, which meant learning and testing took
several days. This was compounded by the size of the learning alphabet, and it forced us into using a reduced alphabet for two of the analyzed implementations.
Limitations of the work, thus elements for future work, are several. First of all, the {\dmapper} was not formalized, unlike in~\cite{TCP2016}, thus we did not
Limitations of the work, hence elements for future work, are several. First of all, the {\dmapper} was not formalized, unlike in~\cite{TCP2016}, thus we did not
produce a concretization of the abstract models. Consequently, model checking results cannot be fully transferred to the actual implementations. Moreover,
abstraction produced by the {\dmapper} could be made less coarse, so more insight into the implementation is gained. Parameters which are now abstracted,
such as the channel identifier or data sent over channels, could be extracted and potentially handled by Register Automata learners. The {\dmapper} also caused
redundancy in the learned model, re-tweaking the abstractions used, in particular those for managing channels, could alleviate this problem while also
improving learning times, which in turn would make facilitate learning using full alphabets for all systems. Another thing which
redundancy in the learned models, re-tweaking the abstractions used, in particular those for managing channels, could alleviate this problem while also
improving learning times. This in turn would ease the task of using expanded alphabets in learning instead of resorting to restricted alphabets. Another thing which
warrants improvement is the handling of buffering behavior. Buffering leads to many uninteresting states and greatly lengthens the learning process.
Despite these limitations, our work provides a compelling application of learning and model checking in a security setting, on a widely used protocol. We hope this lays
......
......@@ -9,5 +9,5 @@ prekex -> kexed[color=green style=bold label="KEX30/
kexed -> keyed[color=green style=bold label="NEWKEYS/
NEWKEYS"]
keyed -> preauth[color=green style=bold label="SR_AUTH/
SR_SUCCESS"]
SR_ACCEPT"]
}
No preview for this file type
......@@ -68,7 +68,7 @@ responses for higher layer inputs sent during key re-exchange, and would deliver
a major contributor to the number of states. In states permitting rekey, following the sequence of transitions comprising the rekey should lead back to the starting state. This
leads to 2 additional rekey states for every state permitting rekey. A considerable number of states were also added due to {\dmapper} generated outputs such as \textsc{ch\_none} or \textsc{ch\_max}, outputs which signal that no channel is open or that the maximum number of channels have been opened.
Figure~{fig:sshserver} shows the model learned for OpenSSH, with various changes applied to improve readability. The happy flow, contoured 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 the \textsc{newkeys} first.}. Also explored is what happens when a rekey sequence is attempted. We notice that rekey is only allowed in states of the Connection layer. Strangely, for these states, rekey 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 rekey (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect. We also notice the intricate authentication behavior, it seems that password authentication is the only form that allows you to authenticate after an unsuccessful attempt.
Figure~\ref{fig:sshserver} shows the model learned for OpenSSH, with various changes applied to improve readability. The happy flow, contoured 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 the \textsc{newkeys} first.}. Also explored is what happens when a rekey sequence is attempted. We notice that rekey is only allowed in states of the Connection layer. Strangely, for these states, rekey 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 rekey (\textsc{kexinit}) yields (\textsc{unimpl}), while the last step (\textsc{newkeys}) causes the system to disconnect. We also notice the intricate authentication behavior, it seems that password authentication is the only form that allows you to authenticate after an unsuccessful attempt.
......
......@@ -39,7 +39,11 @@ in exploring SSH's behavior once the initial exchange took place. From the input
%be sent by both client and server at the start of every connection. The exchange of these inputs is made implicit.
Table~\ref{trans-alphabet} introduces the Transport layer inputs. We include two versions of the \textsc{kexinit} message, one where \texttt{first\_kex\_packet\_follows} is disabled, the other when it is enabled, in which case, the message would make a guess on the security parameters~\cite[p. 17]{rfc4253}. Our mapper can only handle correct key guesses, so the wrong-guess procedure as described in ~\cite[p. 19]{rfc4253} was not supported. \textsc{ignore}, \textsc{unimpl} and \textsc{debug} are not expected to alter behavior so excluded from our restricted alphabet. \textsc{discon} proved costly time wise, so was also excluded.
Table~\ref{trans-alphabet} introduces the Transport layer inputs. We include a version of the \textsc{kexinit} message with \texttt{first\_kex\_packet\_follows} disabled.
This means no guess~\cite[p. 17]{rfc4253} is attempted on the {\dsut}'s parameter preferences. Consequently, the {\dsut} will have to send its own \textsc{kexinit} in order to
convey its own parameter preferences before key exchange can proceed. Also included are inputs for establishing new keys (\textsc{kex30}, \textsc{newkeys}), disconnecting (\textsc{disconnect}), as well as the special inputs \textsc{ignore}, \textsc{unimpl} and \textsc{debug}. The latter are not expected to alter behavior so are excluded from our restricted alphabet. \textsc{disconnect} proved costly time wise, so was also excluded.
%We include two versions of the \textsc{kexinit} message, one where \texttt{first\_kex\_packet\_follows} is disabled, the other when it is enabled, in which case, the message would make a guess on the security parameters~\cite[p. 17]{rfc4253}. Our mapper can only handle correct key guesses, so the wrong-guess procedure as described in ~\cite[p. 19]{rfc4253} was not supported.
%\textsc{ignore}, \textsc{unimpl} and \textsc{debug}
%When needed, SUTs were configured to make this guess work by altering their cipher preferences. The SSH version and comment string (described in Section~\ref{ssh-run-trans}) was not queried because it does not follow the binary packet protocol.
\begin{table}[!ht]
......@@ -47,12 +51,12 @@ Table~\ref{trans-alphabet} introduces the Transport layer inputs. We include two
\small
\begin{tabular}{ll}
\textbf{Message} & \textbf{Description} \\
\textsc{discon} & Terminates the current connection~\cite[p. 23]{rfc4253} \\
\textsc{disconnect} & Terminates the current connection~\cite[p. 23]{rfc4253} \\
\textsc{ignore} & Has no intended effect~\cite[p. 24]{rfc4253} \\
\textsc{unimpl} & Intended response to an unimplemented message~\cite[p. 25]{rfc4253} \\
\textsc{debug} & Provides other party with debug information~\cite[p. 25]{rfc4253} \\
\textsc{kexinit}* & Sends parameter preferences~\cite[p. 17]{rfc4253} \\
\textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\
%\textsc{guessinit}* & A \textsc{kexinit} after which a guessed \textsc{kex30} follows~\cite[p. 19]{rfc4253} \\
\textsc{kex30}* & Initializes the Diffie-Hellman key exchange~\cite[p. 21]{rfc4253} \\
\textsc{newkeys}* & Requests to take new keys into use~\cite[p. 21]{rfc4253} \\
\textsc{sr\_auth}* & Requests the authentication protocol~\cite[p. 23]{rfc4253} \\
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -56,7 +56,7 @@ This function updates the output and state variable for a given valuation of the
state = q0 & in = MSG: q0
state = q1 & in = INIT: q1
state = q1 & in = MSG: q1
next(out)
next(out) := case
state = q0 & in = INIT: OK
state = q0 & in = MSG: ONOK
state = q1 & in = INIT: OK
......
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