Commit 8841f134 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Changed conclusions slightly. Added another spec

parent efc6e4d3
......@@ -17,12 +17,12 @@ leading to a considerable increase in the number of states. Moreover, the system
several days. 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 elements 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. Moreover,
abstraction produced by the {\dmapper} could be made less coarse, so more insight into the implementation is gained. Parameters which are now abstracted,
such as the channel identifier or data sent over channels, could be extracted and potentially handled by Register Automata learners. The {\dmapper} also caused
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. Another thing which
warrants improvement is the handling of buffering behavior. Buffering leads to many uninteresting states and greatly lengthens the learning process.
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.
Furthermore, the {\dmapper} abstraction could be refined, so more insight into the implementation is gained. 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
can infer systems with parameterized alphabets, state variables and simple operations on data. Finally, we had to eliminate any timing related behavior, as it could not be handled by the classical learners used. To that end, preliminary work on learning timed automata\cite{GrinchteinJL10} could be leveraged .
Despite these limitations, our work provides a compelling application of learning and model checking in a security setting, on a widely used protocol. We hope this lays
some more groundwork for further case studies, as well as fresh advancements in learning techniques.
\ No newline at end of file
......@@ -80,7 +80,7 @@ The remainder of this section defines the properties we formalized and verified.
\end{enumerate}
A key note is that properties are checked not on the actual concrete model of the {\dsut}, but on an abstract model, which represents an over-approximation of the {\dsut} induced by the {\dmapper}. This is unlike in~\cite{TCP2016}, where properties where checked on a concretization of the learned model, concretization obtained by application of a reverse mapping. Building a reverse mapper is far from trivial given the {\dmapper}'s complexity. Performing model checking on an abstract model means we cannot fully translate model checking results to the concrete (unknown) model of the implementation. In particular, properties which hold for the abstract model do not necessarily hold for the implementation. Properties that don't hold however, also don't hold for the {\dsut}.
\subsection{Basic characterizing properties}
\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, once the connection is lost, it can no longer be recovered and the {\dmapper} will itself respond with \textsc{no\_conn} to any subsequent non-Connection layer inputs sent by the {\dlearner}. This behavior is described by Property~\ref{prop:noconn}, where \emph{isConnectionInput} is a predicate which only holds if the input supplied is a Connection layer input. The reason we exclude connection inputs is due to a mapper characteristic we touched on in Section~\ref{sec:result}. The {\dmapper} maintains a buffer of opened channels and limits its size to 1. From the perspective of the {\dmapper}, a channel is open, and thus added to the buffer, whenever \textsc{ch\_open} is received from the learner, regardless if a channel was actually opened on the {\dsut}. If an attempt to open an additional channel is made, the {\dmapper} itself responds by \textsc{ch\_max} without querying the {\dsut}. Conversely, if there is no channel open (the buffer is empty) and an input operating on a channel is sent, the {\dmapper} responds by \textsc{ch\_none}, again, without querying the {\dsut}. Additionally, a channel opened on the {\dmapper} is closed and removed from the buffer on a {ch\_close} from the {\dlearner}, with a corresponding SSH CHANNEL CLOSE message being sent to the {\dsut}. We use Property~\label{prop:channel} to describe this mapper induced behavior.
......@@ -202,6 +202,17 @@ G ( (inp=SR_AUTH & out!=NO_CONN & state!=s0) ->
\label{prop:trans-sr}
\end{property}
A general property can also be defined for the \textsc{disconnect} output. The RFC specifies that after sending this message, a party MUST not send or receive any data. While we cannot assess on what the server actually receives, we can check that the server doesn't generate any output after sending \textsc{disconnect}. All output following this \textsc{disconnect} message should be generated directly by the {\dmapper}, and never derived from {\dsut} messages. Knowing the {\dmapper} induced outputs are \textsc{no\_conn}, \textsc{ch\_max} and \textsc{ch\_none}, we formulate by Property~\ref{prop-trans-disc}.
\begin{property}[h]
\begin{lstlisting}[basicstyle=\footnotesize]
G ( out=DISCONNECT ->
X G (out=CH_NONE | out=CH_MAX | out=NO_CONN) )
\end{lstlisting}
\caption{Only {\dmapper} outputs after DISCONNECT}
\label{prop:trans-disc}
\end{property}
%\textit{Could strengthen this so we check that it disconnects (DISCONNECT) after the first rejected service request}
The RFC for the Authentication layer states in~\cite[p. 6]{rfc4252} that if the server rejects the authentication request, it MUST respond with a \textsc{ua\_failure} message. Conversely, if the requests succeeds, a \textsc{ua\_success} MUST be sent only once. Authentication requests received thereafter SHOULD be ignored. While not explicitly stated, we assume this to be in a context where the authentication service had been successfully requested. We define two properties, Property~\ref{prop:auth-pre-ua} for behavior before an \textsc{ua\_success}, Property~\ref{prop:auth-post-ua} for behavior afterward, until the connection is lost.
......@@ -265,6 +276,7 @@ Table~\ref{tab:mcresults} presents model checking results. Crucially, all the cr
& Auth. & & & \\ \hline
Functional& Prop.~\ref{prop:trans-kexinit} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-sr} & & & \\ \cline{2-5}
& Prop.~\ref{prop:trans-disc} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-pre-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:auth-post-ua} & & & \\ \cline{2-5}
& Prop.~\ref{prop:conn-close} & & & \\ \hline
......
......@@ -212,6 +212,42 @@ machine learning algorithms},
title = {An attack on {CRC}-32 integrity checks of encrypted channels using {CBC} and {CFB} modes}
}
@article{GrinchteinJL10,
author = {Olga Grinchtein and
Bengt Jonsson and
Martin Leucker},
title = {Learning of event-recording automata},
journal = {Theor. Comput. Sci.},
volume = {411},
number = {47},
pages = {4029--4054},
year = {2010},
url = {http://dx.doi.org/10.1016/j.tcs.2010.07.008},
doi = {10.1016/j.tcs.2010.07.008}
}
@inproceedings{tomte2015,
title={Learning register automata with fresh value generation},
author={Aarts, Fides and Fiterau-Brostean, Paul and Kuppens, Harco and Vaandrager, Frits},
booktitle={International Colloquium on Theoretical Aspects of Computing},
pages={165--183},
year={2015},
organization={Springer International Publishing}
}
@inproceedings{ralib2015,
title = {{RALib}: {A} {LearnLib} extension for inferring {EFSMs}},
shorttitle = {{RALib}},
url = {https://it.uu.se/katalog/socas172/thesis/difts-final.pdf},
urldate = {2016-09-05},
booktitle = {{DIFTS}},
author = {Cassel, Sofia and Howar, Falk and Jonsson, Bengt},
year = {2015},
keywords = {learning, ralib, register-automata},
file = {2015-RALib A LearnLib extension for inferring EFSMs.pdf:C\:\\Users\\Paul\\AppData\\Roaming\\Zotero\\Zotero\\Profiles\\tt1zn5x1.default\\zotero\\storage\\TQUR4TS7\\2015-RALib A LearnLib extension for inferring EFSMs.pdf:application/pdf}
}
@article{Chalupar2014Automated,
author = {Chalupar, Georg and Peherstorfer, Stefan and Poll, Erik and de Ruiter, Joeri},
citeulike-article-id = {13837720},
......
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