We have combined model learning with abstraction techniques to infer models of the OpenSSH, Bitvise and DropBear SSH server implementations. We have also
formalized several security and functional properties drawn from the SSH RFC specifications. We have verified these
properties on the learned models using model checking and have uncovered several minor inconsistencies, though crucially, the security critical properties were met
by all implementations.
properties on the learned models using model checking and have uncovered several minor standard violations.
The security critical properties were met by all implementations.
Abstraction was provided by a {\dmapper} component placed between the
{\dlearner} and the {\dsut}. The {\dmapper} was constructed from an
...
...
@@ -15,15 +15,15 @@ full version for OpenSSH, and a restricted version for the other
implementations. The restricted alphabet was still sufficient to
explore most aforementioned behavior.
There were several challenges encountered. Firstly, building a {\dmapper} presented a considerable technical challenge, as it required re-structuring of an actual
We encountered several challenges. Firstly, building a {\dmapper} presented a considerable technical challenge, as it required re-structuring of an actual
SSH implementation. Secondly, because we used classical learning algorithms, we had to ensure that the abstracted implementation behaved
like a deterministic Mealy Machine. Here time-induced non-determinism was difficult to eliminate. Buffering also presented problems,
like a (deterministic) Mealy Machine. Here time-induced non-determinism was difficult to eliminate. Buffering also presented problems,
leading to a considerable increase in the number of states. Moreover, the systems analyzed were relatively slow, which meant learning took
several days\marginpar{\tiny Erik: For a single server, right??}. 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, hence possibilities 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. Formal definition
of the mapper and concretization of the learned models would tackle this. The {\dmapper} also caused considerable 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 facilitate learning using expanded alphabets instead of resorting to restricted alphabets.
of the mapper and concretization of the learned models (as defined in \cite{AJUV15}) would tackle this. The {\dmapper} also caused considerable 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 facilitate learning using expanded alphabets instead of resorting to restricted alphabets.
Furthermore, the {\dmapper} abstraction could be refined, to give more
insight into the implementations. In particular, parameters,
such as the session identifier or data sent over channels, could be extracted from the {\dmapper} and potentially handled by existing Register Automata learners\cite{ralib2015,tomte2015}. These learners
\authornote{Supported by NWO project 612.001.216, Active Learning of Security Protocols (ALSEP).}
\affiliation{%
\institution{Radboud University Nijmegen}
}
...
...
@@ -87,17 +85,14 @@ tabsize=2
\affiliation{%
\institution{Radboud University Nijmegen}
}
\email{patrick.verleg@student.ru.nl}
\email{patrickverleg@gmail.com}
\renewcommand{\shortauthors}{Fiter\u{a}u-Bro\c{s}tean et al.}
\begin{abstract}
We apply model learning on three SSH implementations to infer state machine models, which
are then verified by a model checker for functional and security properties. Our results show that
all tested SSH servers satisfy the security properties, but
satisfy the functional properties
only to a varying degree. Moreover, the state machines of the
implementations differ significantly, allowing them to be
are then verified by a model checker for functional and security properties. Our analysis showed that
all tested SSH server models satisfy the security properties. Nevertheless, we uncovered several minor standard violations.
The state machines of the implementations differ significantly, allowing them to be
effectively fingerprinted.
%Various shortcomings with regards to the RFCs were found. Opening multiple channels is not properly implemented on CiscoSSH and PowerShell. OpenSSH contains a bug which can result in connection closure after rekeying in some circumstances. Both Tectia and OpenSSH implement a liberal message acceptance policy in the first phase of the protocol. Such a liberal policy is unwise in this error-prone stage.
...
...
@@ -154,6 +149,7 @@ effectively fingerprinted.
\maketitle
\renewcommand{\shortauthors}{Fiter\u{a}u-Bro\c{s}tean et al.}
abstract={The problem of identifying an unknown regular set from examples of its members and nonmembers is addressed. It is assumed that the regular set is presented by a minimally adequate Teacher, which can answer membership queries about the set and can also test a conjecture and indicate whether it is equal to the unknown set and provide a counterexample if not. (A counterexample is a string in the symmetric difference of the correct set and the conjectured set.) A learning algorithm L∗ is described that correctly learns any regular set from any minimally adequate Teacher in time polynomial in the number of states of the minimum dfa for the set and the maximum length of any counterexample provided by the Teacher. It is shown that in a stochastic setting the ability of the Teacher to test conjectures may be replaced by a random sampling oracle, {EX}( ). A polynomial-time learning algorithm is shown for a particular problem of context-free language identification.},
address={Duluth, MN, USA},
author={Angluin, Dana},
journal={Information and Computation},
author={Angluin, D.},
journal={Inf.\ and Comp.},
month=nov,
number={2},
pages={87--106},
publisher={Academic Press, Inc.},
title={Learning regular sets from queries and counterexamples},
volume={75},
year={1987}
}
@incollection{Aarts2010Generating,
author={Aarts, Fides and Jonsson, Bengt and Uijen, Johan},
author={Chalupar, Georg and Peherstorfer, Stefan and Poll, Erik and de Ruiter, Joeri},
citeulike-article-id={13837720},
booktitle={Proceedings of the 8th USENIX workshop on
Offensive Technologies (WOOT'14)},
author={Chalupar, G. and Peherstorfer, S. and Poll, E. and Ruiter, J. {de}},
booktitle={Proc.\ USENIX workshop on Offensive Technologies (WOOT'14)},
pages={1--10},
posted-at={2015-11-13 14:58:54},
priority={2},
title={Automated Reverse Engineering using {LEGO}},
year={2014}
}
@incollection{Aarts2010Inference,
author={Aarts, Fides and Schmaltz, Julien and Vaandrager, Frits},
author={Aarts, F. and Schmaltz, J. and Vaandrager, F.},
booktitle={Leveraging Applications of Formal Methods, Verification, and Validation},
editor={Margaria, Tiziana and Steffen, Bernhard},
pages={673--686},
publisher={Springer},
series={LNCS},
...
...
@@ -268,8 +248,7 @@ machine learning algorithms},
@article{Bellare2004Breaking,
abstract={The secure shell ({SSH}) protocol is one of the most popular cryptographic protocols on the Internet. Unfortunately, the current {SSH} authenticated encryption mechanism is insecure. In this paper, we propose several fixes to the {SSH} protocol and, using techniques from modern cryptography, we prove that our modified versions of {SSH} meet strong new chosen-ciphertext privacy and integrity requirements. Furthermore, our proposed fixes will require relatively little modification to the {SSH} protocol and to {SSH} implementations. We believe that our new notions of privacy and integrity for encryption schemes with stateful decryption algorithms will be of independent interest.},
address={New York, NY, USA},
author={Bellare, Mihir and Kohno, Tadayoshi and Namprempre, Chanathip},
author={Bellare, M. and Kohno, T. and Namprempre, C.},
abstract={This paper presents a variety of plaintext-recovering attacks against SSH. We implemented a proof of concept of our attacks against OpenSSH, where we can verifiably recover 14 bits of plaintext from an arbitrary block of ciphertext with probability \$2^{-14}\$ and 32 bits of plaintext from an arbitrary block of ciphertext with probability \$2^{-18}\$. These attacks assume the default configuration of a 128-bit block cipher operating in CBC mode. The paper explains why a combination of flaws in the basic design of SSH leads implementations such as OpenSSH to be open to our attacks, why current provable security results for SSH do not cover our attacks, and how the attacks can be prevented in practice.},
address={Washington, DC, USA},
author={Albrecht, Martin R. and Paterson, Kenneth G. and Watson, Gaven J.},
booktitle={Security and Privacy, 2009 30th IEEE Symposium on},
institution={Inf. Security Group, Univ. of London, Egham, UK},
month=may,
author={Albrecht, M.R. and Paterson, K.G. and Watson, G.J.},
author={Beurdouche, B. and Bhargavan, K. and Delignat-Lavaud, A. and Fournet, C. and Kohlweiss, M. and Pironti, A. and Strub, P.-Y. and Zinzindohoue, J. K.},
title={A Messy State of the Union: Taming the Composite State Machines of TLS},
