Commit db65d2d2 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Addressed some comments

parent 6571ae71
......@@ -15,7 +15,7 @@ implementations of other security protocols, notably TLS, with Apple's
'goto fail' bug and the FREAK attack \cite{Beurdouche:2017}. For this
we use model learning (a.k.a.\ active automata learning)
\cite{Angluin1987Learning,Vaa17} to infer state machines of three SSH
implementations, which we then analyse by model checking for
implementations, which we then analyze by model checking for
conformance to both functional and security properties.
The properties we verify for the inferred state machines are based on
......@@ -29,8 +29,7 @@ under-specification in the RFC standards.
Model learning obtains a state machine model of a black-box system by
providing inputs and observing outputs. Since model learning uses a
finite number of observations, we can never be sure that the learned
model is complete\marginpar{\tiny Erik: I prefer 'complete' to
'correct'.} To that end, advanced conformance algorithms are employed
model is correct. To that end, advanced conformance algorithms are employed
\cite{LeeY96}, which yield some confidence that the system inferred is
in fact complete. In the context of testing security protocols, model
learning can be seen as a form of fuzzing, where inputs are sent in
......@@ -52,7 +51,7 @@ options. Our analysis only considers the protocol logic. However,
their rules were tied to routines in the code, so had to be slightly adapted
to fit the different implementations. In contrast, our properties are
defined at an abstract level so do not need such tailoring. Moreover,
our black box approach approach means we can analyse any implemention
our black box approach approach means we can analyze any implementation
of SSH, not just C implementations.
Formal models of SSH in the form of state machines have been used
......@@ -81,7 +80,7 @@ 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
characterisation of normal network traffic, but it cannot uncover
characterization of normal network traffic, but it cannot uncover
implementation flaws that occur in strange message flows, which is our
goal.
......
......@@ -44,8 +44,9 @@ the messages \textsc{service\_accept}, \textsc{ua\_accept},
Connection layer we only use messages for channel management and the
terminal functionality. Finally, because we will only explore
protocol behaviour after SSH versions have been exchanged, we exclude
these messages for exchaning version numbers. \marginpar{\tiny Erik: I
rephrased all this to make it simpler. Is it still ok?}
these messages for exchanging version numbers.
%\marginpar{\tiny Erik: I
%rephrased all this to make it simpler. Is it still ok?}
The resulting lists of inputs for the three protocol layers are given
in tables~\ref{trans-alphabet}-\ref{conn-alphabet}. In some
......@@ -169,26 +170,24 @@ keys. Receipt of the \textsc{newkeys} response from the {\dsut} will
make the {\dmapper} use the new keys earlier negotiated in place of
the older ones, if such existed.
The {\dmapper} contains two other
state variables,
one is a buffer for storing open channels. It is initially empty and
is increased/decreased on \textsc{ch\_open} and \textsc{ch\_close}
inputs respectively. The other is initially set to 0, and stores the
sequence number of the last received message. This is then used when
constructing \textsc{unimpl} inputs. \marginpar{\tiny Erik: I don't get this
bit}
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.
In the following cases, inputs are answered by the {\dmapper} directly
instead of being sent to the {\dsut} fo find out its response:
instead of being sent to the {\dsut} to find out its response:
\begin{enumerate}
\item on receiving a \textsc{ch\_open} input and the buffer has reached the size limit, the {\dmapper} directly responds with \textsc{ch\_max};
\item on receiving any input operating on a channel (all Connection layer inputs other than \textsc{ch\_open}) when the buffer is empty, the
{\dmapper} directly responds with \textsc{ch\_none};
\item if connection with the {\dsut} was terminated, the {\dmapper}
responds with a \textsc{no\_conn} message, as sending furtheer
responds with a \textsc{no\_conn} message, as sending further
messages to the {\dsut} is pointless in that case;
\item if no channel has been opened (the buffer variable is empty) or the maximum number of channels was reached (in our experiments 1), cases which prompt the {\dmapper}
to respond with \textsc{ch\_none}, or \textsc{ch\_max} respectively
\marginpar{\tiny Erik: i don't get this 2nd bullet; something is
missing?}
\end{enumerate}
Overall, we notice that in many ways, the {\dmapper} acts similarly to an SSH client. Hence it is unsurprising that it was built off an existing
......@@ -236,7 +235,7 @@ a warning, which then needs to be manually investigated.
An added benefit of this cache is that is allows the {\dmapper} to
supply answer to some inputs without actually sending them to the
{\dsut}. This speeded up learning a lot when we had to restart
{\dsut}. This sped up learning a lot when we had to restart
experiments: any new experiment on the same {\dsut} could start where
the previous experiment left of, without re-running all inputs. This
was an important benefit, as experiments could take several days.
......@@ -263,7 +262,7 @@ output \textsc{buffered}.
Secondly, buffering happens when opening and closing channels, since a
{\dsut} can close only as many channels as have previously been opened.
Learning this behaviour would lead to an infinite state machine, as we
Learning this behavior would lead to an infinite state machine, as we
would need a state `there are $n$ channels open' for every number $n$.
For this reason, we restrict the number of simultaneously open
channels to one. The {\dmapper} returns a custom response
......
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