Commit 7145da0a authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

More updates

parent 929d2cc4
......@@ -22,10 +22,8 @@ We have adapted the setting of timing parameters to each implementation.
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-size, 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
\textsc{ua\_pw\_nok}) as it they would take the system 2-3 seconds to respond to. By contrast, public key authentication resulted in quick responses. For a similar reason we excluded
\textsc{disconnect}.
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
\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
%challenges, as it would take a varying amount of time before the system responded.
......@@ -42,8 +40,9 @@ For the test queries we used random and exhaustive variants of the testing algor
distinguishing sequence. The exhaustive variant generates tests for all possible middle sections of length {\dk} 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 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. %We have additionally included in our suit suite counterexamples to the formalized specification generated by the model checker. 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.
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.
%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:
......
......@@ -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 can not be re-established. The moment
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
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]
......@@ -162,7 +162,7 @@ Outputs \textsc{ch\_max} and \textsc{ch\_none} are still generated because of a
\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.
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 were 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 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$.
% SR_AUTH_AUTH -> SR_AUTH
......
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