Commit 8e5245cb authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Processed first round of comments

parent 25f61056
......@@ -57,7 +57,7 @@ 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 means we can analyze any implementation
of SSH, not just C implementations.
of SSH, not just open source C implementations.
Formal models of SSH in the form of state machines have been used
......
......@@ -7,7 +7,7 @@ systems. BitVise is a well-known proprietary Windows-only SSH implementation.
In our experimental setup, {\dlearner} and {\dmapper} ran inside a Linux Virtual Machine. OpenSSH and DropBear were
learned over a localhost connection, whereas BitVise was learned over a virtual connection with the Windows host machine.
Certain arrangements had to be made including the setting of timing parameters to fit each implementation.
We have adapted the setting off timing parameters to each implementation.
\begin{figure*}
\centering
......@@ -36,7 +36,7 @@ challenges, as it would take a varying amount of time until the system responded
For the test queries we used random and exhaustive variants of the testing algorithm described in
\cite{SMJV15}, which generate efficient test suites. Tests generated comprise an access sequence, a middle section of length {\dk} and a
distinguishing sequence. The exhaustive variant for a set {\dk} generates tests for all possible middle sections and all states. Passing all tests then provides some notion of confidence,
namely, that the learned model is correct unless the (unknown) model of the implementation has at least {\dk} more states. The random variant produces tests
namely, that the learned model is correct unless the (unknown) model of the implementation has at least {\dk} more states than the learned hypothesis. The random variant produces tests
with randomly generated middle sections. No formal confidence is provided, but past experience shows this to be more effective at finding counterexamples since {\dk}
can be set to higher values. We executed a random test suite with {\dk} of 4 comprising 40000 tests for OpenSSH, and 20000 tests for BitVise and DropBear.
We then ran an exhaustive test suite with {\dk} of 2 for all implementations.
......
......@@ -100,7 +100,7 @@ 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 manage channels and to request/run services over them. In accordance with our learning goal,
The Connection layer allows the client to manage channels and to request/run 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.
......@@ -152,7 +152,7 @@ logic with one dictated by messages received from the {\dlearner}.
The {\dmapper} maintains a set of state variables to record parameters
of the ongoing session, including for example the server's preferences
for key exchange and encryption algorithm, parameters of these
protocols, and -- once is has been established -- the session key.
protocols, and -- once it has been established -- the session key.
These parameters are updated when receiving messages from the server,
and are used to concretize inputs to actual SSH messages to the server.
......@@ -209,7 +209,7 @@ There are a few sources of non-determinism in SSH:
\begin{enumerate}
\item Underspecification in the SSH specification (for example, by not
specifying the order of certain messages) allows some
non-deterministic behavior. And even if client
non-deterministic behavior. Even if client
and server do implement a fixed order for messages they sent, the
asynchronous nature of communication means that the
interleaving of sent and received messages may vary. Moreover,
......@@ -218,12 +218,17 @@ There are a few sources of non-determinism in SSH:
messages are aimed to thwart traffic analysis.}
\item Timing is another source of non-deterministic behavior. For
example, the {\dmapper} might time-out before the {\dsut} had
sent its response.
In our experiments we tried to set time-out periods so that this
did not occur. However, other timing-related quirks can still
cause non-determinism. For example, some {\dsuts} behave
sent its response. Some {\dsuts} also behave
unexpectedly when a new query is received too shortly after the
previous one.
previous one. Hence in our experiments we adjusted time-out
periods accordingly so that neither of these events occur, and the {\dsut}
behaves deterministically all the time.
%did not occur.
%However, other timing-related quirks can still
%cause non-determinism. For example, some {\dsuts} behave
%unexpectedly when a new query is received too shortly after the
%previous one.
%For example, a trace in which a valid user authentication is performed within five milliseconds after an authentication request on DropBear can cause the authentication to (wrongly) fail.
\end{enumerate}
%
......
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