Commit 18c8f0fb authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

updates

parent 97388517
......@@ -2,13 +2,11 @@
The SSH protocol is used interact securely with remote machines. Alongside TLS and IPSec, SSH is amongst the most frequently used security suites~\cite{Albrecht2009Plaintext}. Due to its significant user base and sensitive nature, flaws in the protocol or its implementation could have major impact. It therefore comes as no surprise that SSH has attracted scrutiny from the security community. Problems with information leakage via unencrypted MACs were identified~\cite{Bellare2004Breaking}, as well as possibilities for plain text recovery when a block cipher in cipher block chaining mode was used~\cite{Albrecht2009Plaintext}. Other analysis found no serious issues~\cite{Williams2011Analysis}\cite{Paterson2010PlaintextDependent}. Academic researchers have so far focused more on the theoretical aspects than on implementations of the protocol.
In this work, we use classical active automata learning, which we refer to as model learning, to infer state machines of 2 SSH implementations. Model learning has previously been applied to infer state machines of EMV bank cards~\cite{Aarts2013Formal}, electronic passports~\cite{Aarts2010Inference} and hand-held readers for online banking~\cite{Chalupar2014Automated}. More recently, it was used to learn implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol}. Model learning's goal is obtaining a state model of a black-box system by providing inputs and observing outputs. The learned state model corresponds to the observed behavior, and can be used in system analysis. Since model learning builds from a finite number of observations, we can never be sure that the learned model is correct. To that end, advanced conformance algorithms are employed, which yield some confidence that the system inferred is in fact correct. In the context of testing protocols, model learning can be seen as a form of protocol state fuzzing, whereby unexpected inputs are sent to a system under test in the hope of exposing hidden anomalies. In model learning, inputs are sent with no regard to the order imposed by the protocol.
Inputs can therefore be sent disorderly. Any anomalies are then exposed in the learned model.
In this work, we use classical active automata learning, which we refer to as model learning, to infer state machines of 2 SSH implementations. Model learning has previously been applied to infer state machines of EMV bank cards~\cite{Aarts2013Formal}, electronic passports~\cite{Aarts2010Inference} and hand-held readers for online banking~\cite{Chalupar2014Automated}. More recently, it was used to learn implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol}. Model learning's goal is obtaining a state model of a black-box system by providing inputs and observing outputs. The learned state model corresponds to the observed behavior, and can be used in system analysis. Since model learning builds from a finite number of observations, we can never be sure that the learned model is correct. To that end, advanced conformance algorithms are employed, which yield some confidence that the system inferred is in fact correct. In the context of testing protocols, model learning can be seen as a form of protocol state fuzzing, whereby unexpected inputs are sent to a system under test in the hope of exposing hidden anomalies. In model learning, inputs are sent with no regard to the order imposed by the protocol. Inputs can therefore be sent disorderly. Any anomalies are then exposed in the learned model.
Having obtained models, we use model checkers to automatically verify their conformance to security properties. Such verification would be difficult manually, as the learned models are large. Moreover, the very satisfaction of properties can be used to refine the learned model. In cases where the learned model does not satisfy a security property, the proving sequence of inputs can either signal non-conformance of the system, or can be used to further refine the learned model.
Having obtained models, we use model checking to automatically verify their conformance to security properties. Such verification would be difficult manually, as the learned models are large. Moreover, the very satisfaction of properties can be used to refine the learned model. In cases where the learned model does not satisfy a security property, the proving sequence of inputs can either signal non-conformance of the system, or can be used to further refine the learned model. The security properties are drawn out of the RFC specifications\cite{rfc4251}\cite{rfc4252}\cite{rfc4253}\cite{rfc4254} and formalized in LTL. They are then checked for truth on the learned model using NuSMV~\cite{NuSMV}.
Our work is borne out of 3 recent theses. It most closely resembles work on TCP~\cite{Janssen2015Learning}, where they also combine classical learning and model checking to analyze
various TCP implementations, with our work being more focused on security properties. Other case studies rely on
Our work is borne out of 2 recent theses \cite{Verleg2016}, \cite{Toon2016}. It most closely resembles work on TCP~\cite{Janssen2015Learning}, where they also combine classical learning and model checking to analyze various TCP implementations, with our work being more focused on security properties. Other case studies rely on
manual analysis of the learned models ~\cite{Aarts2013Formal},\cite{Chalupar2014Automated}, \cite{RuiterProtocol}. Our work differs,
since we use a model checker to automatically check specifications. Moreover, the model checker is also used as means of testing the learned model.
Inference of protocols has also been done from observing network traffic ~\cite{Wang2011Inferring}. Such inference is limited to the traces that
......
\section{Learning setup} \label{sec:setup}
\section{The learning setup} \label{sec:setup}
%This chapter will cover the setup used to infer the state machines. We provide a general setup outline in Section~\ref{components}. The tested SSH servers are described in Section~\ref{suts}, which were queried with the alphabet described in Section~\ref{alphabet}. Section~\ref{setup-handling} will cover the challenging SUT behaviour faced when implementing the mapper, and the adaptations that were made to overcome these challenges. Section~\ref{layers-individual} will discuss the relation between state machines for individual layers and the state machine of the complete SSH protocol. The conventions on visualisation of the inferred state machines are described in Section~\ref{visualisation}.
%Throughout this chapter, an individual SSH message to a SUT is denoted as a \textit{query}. A \textit{trace} is a sequence of multiple queries, starting from a SUT's initial state. Message names in this chapter are usually self-explanatory, but a mapping to the official RFC names is provided in Appendix~\ref{appendixa}.
......@@ -12,7 +12,7 @@ The learner uses LearnLib ~\cite{LearnLib2009}, a Java library implementing $L^{
\begin{figure}
\centering
\includegraphics[scale=0.35]{example-components.pdf}
\caption{The setup consists of a learner, mapper and SUT.}
\caption{The SSH learning setup.}
\label{fig:components}
\end{figure}
......@@ -82,15 +82,30 @@ The connection protocol allows the client to request different processes over a
\label{conn-alphabet}
\end{table}
%The learning alphabet comprises of input/output messages by which the {\dlearner} interfaces with the {\dmapper}. Section~\ref{sec:ssh} outlines essential inputs, while Table X provides a summary
%of all messages available at each layer.
%of all messages available at each layer. \textit{\textit{}}
%table
\subsection{The mapper}
The {\dmapper} must provide translation between abstract message representations and well-formed SSH messages. A special case is for when no output is received from the {\dsut}, in which case the {\dmapper} gives back to the learner a {\dtimeout} message, concluding a timeout occurred. The sheer complexity of the {\dmapper}, meant that it was easier to adapt an existing SSH implementation, rather than construct the {\dmapper} from scratch. Paramiko had already provided routines for sending the different types of packets, and for receiving them. These routines were called by control logic dictated by Paramiko's own state machine. The {\dmapper} was constructed by replacing this control logic with one dictated by messages received from the {\dlearner}. %over a socket connection
The {\dmapper} must provide translation between abstract message representations and well-formed SSH messages. A special case is for when no output is received from the {\dsut}, in which case the {\dmapper} gives back to the learner a {\dtimeout} message, concluding a timeout occurred. The sheer complexity of the {\dmapper}, meant that it was easier to adapt an existing SSH implementation, rather than construct the {\dmapper} from scratch. Paramiko already provides routines for sending the different types of packets, and for receiving them. These routines are called by control logic dictated by Paramiko's own state machine. The {\dmapper} was constructed by replacing this control logic with one dictated by messages received from the {\dlearner}. %over a socket connection
The {\dmapper} mapper maintains a set of state variables which are used in this abstract to concrete translation. It most notably, (1) saves the parameter preferences, (2)
it uses to craft concrete messages corresponding the learning abstractions.
%textbf{Message} & \textbf{Influence on mapper state} \\
%\textsc{kexinit} & Saves SUT's parameter preferences\tablefootnote{The parameters that must be supported according to the RFCs to ensure interoperability are used if no \textsc{kexinit} has been received.}. \\
%\textsc{kex31} & Saves the exchange hash resulting from key exchange. \\
%\textsc{newkeys} & Takes in use new keys for all outgoing messages\tablefootnote{Silently ignored when key exchange has not yet been completed.}. \\
%\textsc{ch\_accept} & Saves the channel identifier, used in some queries\tablefootnote{Zero is used if no \textsc{ch\_accept} has been received.}. \\
%\textit{any} & Saves the sequence number, used for the \textsc{unimpl} query\tablefootnote{Zero is used if no message has been received.}. \\
%\end{tabular}
%\caption{State-changing responses implemented by the mapper. These combinedly result in the mapper's state.}
%\label{table:state}
%\end{table}
These are updated
The {\dmapper} updates its state with information from concrete messages. This enables it to craft concrete messages corresponding to the learner abstractions.
Table~\ref{table:state} shows how the mapper is updated.
%As and thus to interact with the {\dsut}, at times similar to how an SSH client would.
......@@ -107,13 +122,13 @@ timeout values accordingly, so that enough time was allowed for the response to
%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}
To detect non-determinism, we cache all new observations in an SqlLite database and we verify observations against this cache. The cache also enables us to answer to queries answered before
To detect non-determinism, we cache all new observations in an SqlLite database and verify observations against this cache. The cache also enables us to answer to queries answered before
without running inputs on the {\dsut}. A subsequent identical learning run can quickly resume from where the previous one was ended, as the cache from the previous run is used to quickly respond to all queries up to the point the previous run ended.
Aside from non-determinism, SSH implementations can also produce a sequence of outputs in response to an input, whereas Mealy machines allow for only one output. To that end, the {\dmapper}
concatenates all outputs into one, delivering a single output to the {\dlearner}.
Another challenge is presented by buffering, leading to an explosion of states, as buffers cannot be described succintly by Mealy Machines.
We have encountered buffers in two occasions. Firstly, some implementations buffer certain responses when in re-key exchange. As soon as re-keying completes, these queued messages are released all at once. This leads to a \textsc{newkeys} response (indicating re-keying has completed), directly followed by all buffered responses. This combined with concatenation of the multiple output response would lead to non-termination of the learning algorithm, as for every variant of the response queue there would be a different output. To counter this, we replace by concatenation of queued output responses by the single word \textsc{buffered}, thus forming \textsc{newkeys\_buffered}.
We have encountered buffers in two occasions. Firstly, some implementations buffer certain responses when in re-key exchange. As soon as re-keying completes, these queued messages are released all at once. This leads to a \textsc{newkeys} response (indicating re-keying has completed), directly followed by all buffered responses. This, combined with concatenation of the multiple output responses would lead to non-termination of the learning algorithm, as for every variant of the response queue there would be a different output. To counter this, we replace the concatenation of queued output responses by the single string \textsc{buffered}, thus forming \textsc{newkeys\_buffered}.
Buffer behaviour can also be observed when opening and closing channels, since a SUT can close only as many channels as have previously been opened. For this reason, we restricted the number of simultaneously open channels to one. The {\dmapper} returns a custom response \textsc{ch\_max} to a \textsc{ch\_open} message whenever this limit is reached.
\ No newline at end of file
......@@ -2,7 +2,12 @@
\usepackage{booktabs} % For formal tables
\usepackage{amssymb} % math stuff
\usepackage{amsmath} % more math stuff
\usepackage{mathtools} % for \coloneqq (defines-symbol := )
\usepackage{graphicx} % for graphics
\usepackage{listings}
\usepackage{float}
% Copyright
%\setcopyright{none}
%\setcopyright{acmcopyright}
......@@ -30,7 +35,9 @@
\begin{document}
\title{Inference and verification of SSH state machines by state fuzzing and model checking}
\graphicspath{{images/}}
\include{macros}
\title{Leveraging Model Learning and Model Checking to Infer and Verify SSH Implementations}
\author{Ben Trovato}
......@@ -102,12 +109,12 @@
\begin{abstract}
We apply protocol state fuzzing on three SSH implementations to infer state machines, which
We apply protocol state fuzzing on two SSH implementations to infer state machines, which
are then verified by a model checker for basic security properties. Our results show that
all tested SSH servers adhere to these properties. That said, their corresponding state machines differ significantly.
These variances allow anyone to effectively fingerprint the tested servers.
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.
%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.
\end{abstract}
......@@ -155,11 +162,12 @@ Various shortcomings with regards to the RFCs were found. Opening multiple chann
\maketitle
\input{introduction}
\input{3-ssh}
\input{4-preliminaries}
\input{5-setup}
\input{6-results}
\input{7-conclusions}
\input{preliminaries}
\input{the_sut}
\input{learning_setup}
%\input{learning_results}
\input{security_definitions}
%\input{conclusions}
\bibliographystyle{ACM-Reference-Format}
\bibliography{sigproc}
......
......@@ -27,7 +27,7 @@ input enabled and deterministic.
\subsection{MAT Framework} \label{ssec:mat}
The most efficient algorithms for model learning all follow
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Ang87}.
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Angluin1987Learning}.
In the MAT framework, learning is viewed as a game in which a learner has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a deterministic Mealy machine $\M$.
Initially, the learner only knows the inputs $I$ and outputs $O$ of $\M$.
The task of the learner is to learn $\M$ through two types of queries:
......
\section{Checking security specifications} \label{sec:specs}
We use the NuSMV model checker to verify security properties. NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function, which can then be defined to change these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a certain specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
\newfloat{property}{thp}{lop}
\floatname{property}{Property}
The properties we verify are primarily drawn from Verleg's security definitions. To these, we add properties on re-keying, as well as other properties outlined in the RFC specification.
We use the NuSMV model checker to verify security properties. NuSMV is a model checker where a state of a model is specified as a set of finite variables, and a transition-function, which can then be defined to change these variables. Specifications in temporal logic, such as CTL and LTL, can be checked for truth on specified models. NuSMV provides a counterexample if a certain specification is not true. NuSMV models are generated automatically from the learned models. Generation proceeds by first defining in an empty NuSMV file three variables, corresponding to inputs, outputs and states. The transition-function is then extracted from the learned model and appended to the file. This function updates the output and state variable for given valuations of the input variable. Below we give an example of a Mealy machine and it's associated NuSMV model.
In this section, we define the properties that we formalized and verified with the NuSMV model checker. We group these properties into three categories:
\begin{enumerate}
\item \textit{general security properties}, that is properties which must hold if the implementation is to be deemed secure
\item \textit{key exchange properties}, that is properties regarding the key exchange operation
\item \textit{other functional properties}, which are extracted from the SHOULD's and the MUST's of the RFC specifications
\end{enumerate}
\subsection{General security properties}
Verleg defined three security properties, one for each layer. We formalized and checked two, leaving out the one defined for the Connection layer, as it implied manually checking the model for problems.
\subsection{General security properties}
Both the Transport and the Authentication Layers can be said to provide notions of security, which secure access to services of the Connection Layer. For each of these layers, we define general security properties that reflect successful implementation of these notions.
%Each upper SSH layer assumes a notion of security is provided by the layer bellow. The Authentication Layer assumes integrity and confidentiality is provided by the Transport Layer, the Connection Layer the same assumptions, plus it also assumes authentication was successful. We define a general property for each upper layer on the basis of successful implementation of these security notions.
The security property for the Transport layer is defined as follows: ``We consider a transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.'' In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps (*give steps*). These steps have to be performed in order but can be interleaved by other actions. Successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell a authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful
if for the input SERVICE\_REQUEST\_AUTH, the output SERVICE\_ACCEPT was received. Following these principles, we define the LTL specification in Figure~\ref{fig:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
The security property for the Transport layer is defined as follows: ``We consider a transport layer state machine secure if there is no path from the initial state to the point where the authentication service is invoked without exchanging and employing cryptographic keys.''\cite{Verleg2016} In other words, authentication request cannot succeed if key exchange wasn't performed successfully. Key exchange implies performing three steps. These steps have to be performed in order but may be interleaved by other actions. A successful authentication request should necessarily imply successful execution of the key exchange steps. We can tell a authentication request or a key exchange step was successful from the values of the input and output variables. For example, an authentication request is successful if for the input SERVICE\_REQUEST\_AUTH, the output SERVICE\_ACCEPT was received. Following these principles, we define the LTL specification in Property~\ref{prop:prop1}. O stands for the Once-operator, a past time LTL operator, which is true if its argument is true in a past time instant.
\begin{figure}[h]
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G (
(input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT)
->
G ( (input=SERVICE_REQUEST_AUTH & output=SERVICE_ACCEPT) ->
O ( (input=NEWKEYS & output= NO_RESP) &
O ( (input=KEX30 & output=KEX31_NEWKEYS) &
O (output=KEXINIT)
)
)
)
O (output=KEXINIT) ) ) )
\end{lstlisting}
\label{fig:prop1}
\caption{Transport layer security property.}
\end{figure}
\label{prop:prop1}
\end{property}
For the authentication layer, Verleg defined the authentication layer secure ``if there is no path from the unauthenticated state to the authenticated state without providing the correct credentials.''
In a similar way, we say that the Authentication Layer is secure ``if there is no path from the unauthenticated state to the authenticated state without providing the correct credentials.''\cite{Verleg2016}
Since we have no method to directly determine if the model is in an authenticated state, we consider the authenticated state to be a state where opening a channel can be done successfully.
Since opening a channel should only be possible after user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the UA\_FAILURE or UA\_SUCCESS packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Figure~\ref{fig:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
Since opening a channel should only be possible after user authentication, this should show if we are in an authenticated state. The specification then is rather simple: Always, if a channel is opened successfully, has there not been a failure in user authentication since a successful user authentication. Opening a channel successfully in the model is straightforward, a request to open a channel is sent to the server, and a success message is received back. Checking whether there has been a success or failure in user authentication is done by checking if the server ever sends the UA\_FAILURE or UA\_SUCCESS packets. Additional checks if the user actually made a user authentication request could potentially be added. The resulting LTL is shown in Property~\ref{prop:prop2}. This LTL uses the Since-operator (S) which holds if its first argument holds for every state since its second argument holds. Note that the second argument has to hold somewhere in the path for the Since operator to hold.
\begin{figure}[h]
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS)
-> (!(output=UA_FAILURE) S output= UA_SUCCESS) )
G ( (input= CH_OPEN & output= CH_OPEN_SUCCESS) ->
(!(output=UA_FAILURE) S output= UA_SUCCESS) )
\end{lstlisting}
\label{fig:prop2}
\caption{User Authentication layer LTL in NuSMV syntax.}
\end{figure}
\paragraph{Result:} both systems appear to respect this property.
\caption{Authentication layer security property.}
\label{prop:prop2}
\end{property}
\subsection{Re-key properties}
An important property is that re-exchanging keys can be performed in any state of the protocol, and its successful execution doesn't change the protocol state. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. For these, we specify that performing key exchange should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a disconnect action from either side.
\subsection{Key exchange properties}
Important properties are that (re-)exchanging keys is allowed in all states of the protocol, and its successful execution doesn't change the protocol state. We consider 2 general protocol states, pre-authenticated (after a successful authentication request, before authentication) and authenticated. These map to multiple states in the learned models. For each state, we specify the properties that performing key exchange (1) should always be allowed from that state, and (2) if allowed, should always preserve the state, until specific inputs or outputs are encountered that necessarily change it. An example of such inputs or outputs are those corresponding to a \emph{disconnect} action from either side. These properties are useful in characterizing the various implementations. In~\cite{Verleg2016} we noted great variance on satisfaction of these properties.
\subsection{RFC Properties}
We have also formalized and checked properties drawn from the RFC specifications. A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol as per (*ref*). For the Transport Layer, the RFC states that after sending a KEXINIT message, a party MUST not send SERVICE\_REQUEST or SERVICE\_ACCEPT messages, until it has sent a NEWKEYS message. This is translated to the LTL.
\subsection{Other functional properties}
We have also formalized and checked properties drawn from the RFC specifications. A problem was that the specification for each layer seemed to only consider messages specific to that layer. In particular, it didn't consider disconnect messages, that may be sent at any point in the protocol. For the Transport Layer, the RFC states that after sending a KEXINIT message, a party MUST not send SERVICE\_REQUEST or SERVICE\_ACCEPT messages, until it has sent a NEWKEYS message. This is translated to the LTL.
The RFC also states that in case the server rejects a service request, it should send an appropriate DISCONNECT message.
The Connection Layer RFC states that upon receiving a CH\_CLOSE message, a side should send back a CH\_CLOSE message, unless it has already sent this message for the channel. This of course, ignores the case when a side disconnects, in which case a CH\_CLOSE would no longer have to be issued.
\subsection{Model checking results}
Table presents the model checking results. Crucially, all general security properties are met, though key exchange is strangely not universally permitted, while some of the functional properties described are not met.
@misc{NuSMV,
title = {The NuSMV Model Checker},
howpublished = {\url{http://nusmv.fbk.eu/}},
}
@phdthesis{Toon2016,
title={Improving Protocol State Fuzzing of SSH},
author={Lenaerts, T and Vaandrager, FW and Fiterau-Brostean, P and Poll, E},
year={2016}
}
@phdthesis{Verleg2016,
title={Inferring SSH state machines using protocol state fuzzing},
author={Verleg, P and Poll, E and Vaandrager, FW},
year={2016}
}
@article{rfc760,
author = {{Information Sciences Institute, University of Southern California}},
citeulike-article-id = {13912351},
month = jan,
posted-at = {2016-01-19 14:17:48},
priority = {2},
title = {{DOD} standard internet protocol. {RFC} 760, The Internet Engineering Task Force, Network Working Group},
year = {1980}
}
@article{Angluin1987Learning,
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},
citeulike-article-id = {2189861},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=36889},
citeulike-linkout-1 = {http://dx.doi.org/10.1016/0890-5401(87)90052-6},
citeulike-linkout-2 = {http://www.sciencedirect.com/science/article/B6WGK-4DX444W-57/1/495604548d869ef5267ea44746bdd205},
doi = {10.1016/0890-5401(87)90052-6},
issn = {08905401},
journal = {Information and Computation},
month = nov,
number = {2},
pages = {87--106},
posted-at = {2015-12-07 14:09:17},
priority = {2},
publisher = {Academic Press, Inc.},
title = {Learning regular sets from queries and counterexamples},
url = {http://dx.doi.org/10.1016/0890-5401(87)90052-6},
volume = {75},
year = {1987}
}
@incollection{Aarts2010Generating,
author = {Aarts, Fides and Jonsson, Bengt and Uijen, Johan},
booktitle = {Testing Software and Systems},
citeulike-article-id = {13856840},
citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-16573-3_14},
citeulike-linkout-1 = {http://link.springer.com/chapter/10.1007/978-3-642-16573-3_14},
doi = {10.1007/978-3-642-16573-3_14},
editor = {Petrenko, Alexandre and Sim\~{a}o, Adenilso and Maldonado, Jos\'{e} C.},
pages = {188--204},
posted-at = {2015-12-07 11:15:39},
priority = {2},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Generating Models of {Infinite-State} Communication Protocols Using Regular Inference with Abstraction},
url = {http://dx.doi.org/10.1007/978-3-642-16573-3_14},
volume = {6435},
year = {2010}
}
@article{rfc4250,
author = {Lehtinen, Sami},
citeulike-article-id = {13841736},
editor = {Lonvick, Chris},
month = jan,
posted-at = {2015-11-19 11:26:21},
priority = {2},
title = {The Secure Shell ({SSH}) Protocol Assigned Numbers. {RFC} 4250, The Internet Engineering Task Force, Network Working Group},
year = {2006}
}
@article{rfc4255,
author = {Schlyter, Jakob},
citeulike-article-id = {13841173},
month = jan,
posted-at = {2015-11-18 14:54:10},
priority = {2},
title = {Using {DNS} to Securely Publish Secure Shell ({SSH}) Key Fingerprints. {RFC} 4255, The Internet Engineering Task Force, Network Working Group},
year = {2006}
}
@article{Tijssen2014Automatic,
author = {Tijssen, Max},
citeulike-article-id = {13841041},
journal = {Radboud University},
posted-at = {2015-11-18 12:14:47},
priority = {2},
title = {Automatic modeling of {SSH}
implementations with state
machine learning algorithms},
year = {2014}
}
@electronic{FutoranskyAttack,
author = {Futoransky, Ariel and Kargieman, Emiliano},
citeulike-article-id = {13837770},
edition = {oct. 1998},
howpublished = {Online. \url{http://www.coresecurity.com/files/attachments/CRC32.pdf}},
posted-at = {2015-11-13 16:33:04},
priority = {2},
title = {An attack on {CRC}-32 integrity checks of encrypted channels using {CBC} and {CFB} modes}
}
@article{Chalupar2014Automated,
author = {Chalupar, Georg and Peherstorfer, Stefan and Poll, Erik and de Ruiter, Joeri},
citeulike-article-id = {13837720},
journal = {WOOT'14 Proceedings of the 8th USENIX conference on Offensive Technologies},
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},
booktitle = {Leveraging Applications of Formal Methods, Verification, and Validation},
citeulike-article-id = {13837719},
citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-16558-0_54},
citeulike-linkout-1 = {http://link.springer.com/chapter/10.1007/978-3-642-16558-0_54},
doi = {10.1007/978-3-642-16558-0_54},
editor = {Margaria, Tiziana and Steffen, Bernhard},
pages = {673--686},
posted-at = {2015-11-13 14:56:16},
priority = {2},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Inference and Abstraction of the Biometric Passport},
url = {http://dx.doi.org/10.1007/978-3-642-16558-0_54},
volume = {6415},
year = {2010}
}
@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},
citeulike-article-id = {567543},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=996945},
citeulike-linkout-1 = {http://dx.doi.org/10.1145/996943.996945},
doi = {10.1145/996943.996945},
issn = {1094-9224},
journal = {ACM Trans. Inf. Syst. Secur.},
month = may,
number = {2},
pages = {206--241},
posted-at = {2015-11-13 13:57:14},
priority = {2},
publisher = {ACM},
title = {Breaking and Provably Repairing the {SSH} Authenticated Encryption Scheme: A Case Study of the {Encode-then-Encrypt}-{and-MAC} Paradigm},
url = {http://dx.doi.org/10.1145/996943.996945},
volume = {7},
year = {2004}
}
@article{rfc4254,
author = {Ylonen, Tatu},
citeulike-article-id = {13837671},
editor = {Lonvick, C.},
month = jan,
posted-at = {2015-11-13 13:11:06},
priority = {2},
title = {The Secure Shell ({SSH}) Connection Protocol. {RFC} 4254, The Internet Engineering Task Force, Network Working Group},
year = {2006}
}
@article{rfc4252,
author = {Ylonen, Tatu},
citeulike-article-id = {13837669},
editor = {Lonvick, C.},
month = jan,
posted-at = {2015-11-13 13:10:46},
priority = {2},
title = {The Secure Shell ({SSH}) Authentication Protocol. {RFC} 4252, The Internet Engineering Task Force, Network Working Group},
year = {2006}
}
@article{rfc4253,
author = {Ylonen, Tatu},
citeulike-article-id = {13837668},
editor = {Lonvick, C.},
month = jan,
posted-at = {2015-11-13 13:10:24},
priority = {2},
title = {The Secure Shell ({SSH}) Transport Layer Protocol. {RFC} 4253, The Internet Engineering Task Force, Network Working Group},
year = {2006}
}
@article{rfc4251,
author = {Ylonen, Tatu},
citeulike-article-id = {13837660},
citeulike-linkout-0 = {https://www.ietf.org/rfc/rfc4253.txt},
editor = {Lonvick, C.},
month = jan,
posted-at = {2015-11-13 13:05:12},
priority = {2},
title = {The Secure Shell ({SSH}) Protocol Architecture. {RFC} 4251, The Internet Engineering Task Force, Network Working Group},
url = {https://www.ietf.org/rfc/rfc4253.txt},
year = {2006}
}
@article{Poll2007Verifying,
author = {Poll, Erik and Schubert, Aleksy},
citeulike-article-id = {13837644},
journal = {Proceedings of the 17th Workshop on Information Technology and Systems (WITS'07)},
month = dec,
pages = {164--177},
posted-at = {2015-11-13 12:29:00},
priority = {2},
publisher = {Concordia University},
title = {Verifying an implementation of {SSH}},
year = {2007}
}
@incollection{Paterson2010PlaintextDependent,
author = {Paterson, Kenneth G. and Watson, Gaven J.},
booktitle = {Advances in Cryptology – EUROCRYPT 2010},
citeulike-article-id = {13837630},
citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-13190-5_18},
citeulike-linkout-1 = {http://link.springer.com/chapter/10.1007/978-3-642-13190-5_18},
doi = {10.1007/978-3-642-13190-5_18},
editor = {Gilbert, Henri},
pages = {345--361},
posted-at = {2015-11-13 12:20:10},
priority = {2},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {{Plaintext-Dependent} Decryption: A Formal Security Treatment of {SSH}-{CTR}},
url = {http://dx.doi.org/10.1007/978-3-642-13190-5_18},
volume = {6110},
year = {2010}
}
@incollection{Williams2011Analysis,
author = {Williams, Stephen C.},
booktitle = {Cryptography and Coding},
citeulike-article-id = {13837625},
citeulike-linkout-0 = {http://dx.doi.org/10.1007/978-3-642-25516-8_22},
citeulike-linkout-1 = {http://link.springer.com/chapter/10.1007/978-3-642-25516-8_22},
doi = {10.1007/978-3-642-25516-8_22},
editor = {Chen, Liqun},
pages = {356--374},
posted-at = {2015-11-13 12:16:22},
priority = {2},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Analysis of the {SSH} Key Exchange Protocol},
url = {http://dx.doi.org/10.1007/978-3-642-25516-8_22},
volume = {7089},
year = {2011}
}
@inproceedings{Albrecht2009Plaintext,
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},
citeulike-article-id = {13824119},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1608121},
citeulike-linkout-1 = {http://dx.doi.org/10.1109/sp.2009.5},
citeulike-linkout-2 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5207634},
doi = {10.1109/sp.2009.5},
institution = {Inf. Security Group, Univ. of London, Egham, UK},
isbn = {978-0-7695-3633-0},
issn = {1081-6011},
month = may,
pages = {16--26},
posted-at = {2015-11-13 12:14:05},
priority = {2},
publisher = {IEEE},
series = {SP '09},
title = {Plaintext Recovery Attacks against {SSH}},
url = {http://dx.doi.org/10.1109/sp.2009.5},
year = {2009}
}
@book{Barrett2005SSH,
author = {Barrett, Daniel J. and Silverman, Richard E. and Byrnes, Robert G.},
citeulike-article-id = {11858604},
citeulike-linkout-0 = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20&path=ASIN/0596008953},
citeulike-linkout-1 = {http://www.amazon.de/exec/obidos/redirect?tag=citeulike01-21&path=ASIN/0596008953},
citeulike-linkout-2 = {http://www.amazon.fr/exec/obidos/redirect?tag=citeulike06-21&path=ASIN/0596008953},
citeulike-linkout-3 = {http://www.amazon.jp/exec/obidos/ASIN/0596008953},
citeulike-linkout-4 = {http://www.amazon.co.uk/exec/obidos/ASIN/0596008953/citeulike00-21},
citeulike-linkout-5 = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0596008953},
citeulike-linkout-6 = {http://www.worldcat.org/isbn/0596008953},
citeulike-linkout-7 = {http://books.google.com/books?vid=ISBN0596008953},
citeulike-linkout-8 = {http://www.amazon.com/gp/search?keywords=0596008953&index=books&linkCode=qs},
citeulike-linkout-9 = {http://www.librarything.com/isbn/0596008953},
day = {20},
edition = {Second Edition},
howpublished = {Paperback},
isbn = {0596008953},
month = may,
posted-at = {2015-10-01 10:47:14},
priority = {2},
publisher = {O'Reilly Media},
title = {{SSH}, The Secure Shell: The Definitive Guide},
url = {http://www.amazon.com/exec/obidos/redirect?tag=citeulike07-20&path=ASIN/0596008953},
year = {2005}
}
@inproceedings{Aarts2013Formal,
author = {Aarts, Fides and de Ruiter, Joeri and Poll, Erik},
booktitle = {Software Testing, Verification and Validation Workshops (ICSTW), 2013 IEEE Sixth International Conference on},
citeulike-article-id = {13780037},
citeulike-linkout-0 = {http://dx.doi.org/10.1109/icstw.2013.60},
citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6571671},
doi = {10.1109/icstw.2013.60},
institution = {Inst. for Comput. \& Inf. Sci., Radboud Univ. Nijmegen, Nijmegen, Netherlands},
isbn = {978-1-4799-1324-4},
month = mar,
pages = {461--468},
posted-at = {2015-10-01 10:04:08},
priority = {2},
publisher = {IEEE},
title = {Formal Models of Bank Cards for Free},
url = {http://dx.doi.org/10.1109/icstw.2013.60},
year = {2013}
}
@mastersthesis{Janssen2015Learning,
author = {Janssen, Ramon},
citeulike-article-id = {13779542},
howpublished = {Online},
journal = {Radboud University},
posted-at = {2015-09-30 18:55:55},
priority = {2},
school = {Radboud University},
title = {Learning a State Diagram of {TCP} Using Abstraction.},
year = {2015}
}
@electronic{WheelerHow,
author = {Wheeler, David A.},
citeulike-article-id = {13779398},
citeulike-linkout-0 = {http://www.dwheeler.com/essays/heartbleed.html},
edition = {2015-09-18},
howpublished = {Online.\\ \url{http://www.dwheeler.com/essays/heartbleed.html}},
posted-at = {2015-09-30 17:04:16},
priority = {2},
title = {How to Prevent the next {H}eartbleed},
url = {http://www.dwheeler.com/essays/heartbleed.html}
}
@inproceedings{DavidNqsb,
address = {Washington, D.C.},
author = {Kaloper-Mer{v s}injak, David and Mehnert, Hannes and Madhavapeddy, Anil and Sewell, Peter},
booktitle = {24th USENIX Security Symposium (USENIX Security 15)},
citeulike-article-id = {13778670},
citeulike-linkout-0 = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
month = aug,
pages = {223--238},
posted-at = {2015-09-30 08:05:52},
priority = {2},
publisher = {USENIX Association},
title = {{Not-Quite}-{So-Broken} {TLS}: Lessons in {Re-Engineering} a Security Protocol Specification and Implementation},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/kaloper-mersinjak},
year = {2015}
}
@inproceedings{RuiterProtocol,
address = {Washington, D.C.},
author = {de Ruiter, Joeri and Poll, Erik},
booktitle = {24th USENIX Security Symposium (USENIX Security 15)},
citeulike-article-id = {13778669},
citeulike-linkout-0 = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter},
month = aug,
pages = {193--206},
posted-at = {2015-09-30 08:03:40},
priority = {2},
publisher = {USENIX Association},
title = {Protocol State Fuzzing of {TLS} Implementations},
url = {https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter},
year = {2015}
}
@unpublished{Poll2011Rigorous,
abstract = {Abstract. This document presents (semi-)formal specifications of the security protocol {SSH}, more specifically the transport layer protocol, and describe a source code review of {OpenSSH}, the leading implementation of {SSH}, using these specifications. Our specifications, in the form of finite state machines, are at a different level of abstraction that the typical formal descriptions used to study security protocols. Our motivation is to understand actual implementations of {SSH}, so we try to capture some of the details from the official (informal) specification that are irrelevant to the security of the abstract protocol, but which do complicate the implementation. Our specifications should be useful to anyone trying to understand or implement {SSH}. First versions of our specifications were developed for the formal verification of a Java implementation of {SSH} [17]. 1},
author = {Poll, Erik and Schubert, Aleksy},
citeulike-article-id = {13778664},
citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.194.1815},
posted-at = {2015-09-30 08:00:15},
priority = {2},
title = {Rigorous specifications of the {SSH} Transport Layer},
url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.194.1815},
year = {Radboud University, 2011}
}
@article{Pasareanu2008Learning,
abstract = {Assume-guarantee reasoning enables a ” divide-and-conquer” approach to the verification of large systems that checks system components separately while using assumptions about each component's environment. Developing appropriate assumptions used to be a difficult and manual process. Over the past five years, we have developed a framework for performing assume-guarantee verification of systems in an incremental and fully automated fashion. The framework uses an off-the-shelf learning algorithm to compute the assumptions. The assumptions are initially approximate and become more precise by means of counterexamples obtained by model checking components separately. The framework supports different assume-guarantee rules, both symmetric and asymmetric. Moreover, we have recently introduced alphabet refinement, which extends the assumption learning process to also infer assumption alphabets. This refinement technique starts with assumption alphabets that are a subset of the minimal interface between a component and its environment, and adds actions to it as necessary until a given property is shown to hold or to be violated in the system. We have applied the learning framework to a number of case studies that show that compositional verification by learning assumptions can be significantly more scalable than non-compositional verification.},
address = {Hingham, MA, USA},
author = {P\u{a}s\u{a}reanu, Corina S. and Giannakopoulou, Dimitra and Bobaru, Mihaela G. and Cobleigh, Jamieson M. and Barringer, Howard},
booktitle = {Formal Methods in System Design},
citeulike-article-id = {3642638},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1375437},
citeulike-linkout-1 = {http://dx.doi.org/10.1007/s10703-008-0049-6},
citeulike-linkout-2 = {http://www.springerlink.com/content/p68716r3l225k39t},