Commit 857d8b2b authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Consistency edits

parent fb7b522f
......@@ -71,7 +71,7 @@ before, namely for a manual code review of OpenSSH
\cite{Poll_rigorous_2011}, formal program verification of a Java
implementation of SSH \cite{PollSchubert07}, and for model based
testing of SSH implementations \cite{Boss2012}. All this research
only considered the SSH transport layer, and not the other SSH
only considered the SSH Transport layer, and not the other SSH
protocol layers.
Model learning has previously been used to infer state machines of
......
......@@ -43,9 +43,9 @@ $\M$ and $\N$ if and only if $A_{\M}(\sigma) \neq A_{\N}(\sigma)$.
The most efficient algorithms for model learning all follow
the pattern of a \emph{minimally adequate teacher (MAT)} as proposed by Angluin~\cite{Angluin1987Learning}.
Here learning is viewed as a game in which a \emph{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a Mealy machine $\M$,
Here learning is viewed as a game in which a \textit{learner} has to infer an unknown automaton by asking queries to a teacher. The teacher knows the automaton, which in our setting is a Mealy machine $\M$,
also called the System Under Learning ({\dsut}).
Initially, the learner only knows the input alphabet $I$ and output alphabet $O$ of $\M$.
Initially, the {\dlearner} only knows the input alphabet $I$ and output alphabet $O$ of $\M$.
The task of the learner is to learn $\M$ via two types of queries:
\begin{itemize}
\item
......@@ -71,7 +71,7 @@ algorithms for this setting see \cite{Isberner2015}.
\subsection{Abstraction} \label{ssec:mappers}
Most current learning algorithms are only applicable to Mealy machines with small alphabets comprising abstract messages. Practical systems typically
have parameterized input/output alphabets, whose application triggers updates on the system's state variables. To learn
these systems we place a \emph{mapper} between the learner and the {\dsut}. The mapper is a transducer which translates
these systems we place a \emph{mapper} between the {\dlearner} and the {\dsut}. The {\dmapper} is a transducer which translates
concrete inputs to abstract inputs and concrete outputs to abstract outputs. For a thorough discussion of mappers, we refer to \cite{AJUV15}.
%Perhaps some explanation
......
......@@ -361,7 +361,7 @@ after successful authentication, both BitVise and OpenSSH respond with \textsc{u
Property~\ref{prop:auth-post-ua}. Whether the alternative behavior adapted is acceptable, is up for debate. Definitely the RFC does not suggest it, though the RFC
does leave room for interpretation of the \textsc{unimpl} message.
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all transport layer specifications, however,
DropBear is the only implementation that allows rekey in both general states of the protocol. DropBear also satisfies all Transport layer specifications, however,
problematically, it violates properties of the higher layers. Upon receiving \text{ch\_close}, it responds by \textsc{ch\_eof} instead of \text{ch\_close}, not respecting
Property~\ref{prop:conn-close}. Moreover, the output \textsc{ua\_success} can be generated multiple times, violating both Properties ~\ref{prop:auth-post-ua-strong} and
~\ref{prop:auth-post-ua}.
......
......@@ -21,7 +21,7 @@ SSHv2 follows a client-server paradigm. The protocol consists of three layers (F
Each layer has its own specific messages. The SSH protocol is interesting in that outer layers do not encapsulate inner layers. This means that different layers can interact. Hence, it makes sense to analyze SSH as a whole, instead of analyzing its constituent layers independently. Below we discuss each layer, outlining the relevant messages which are later used in learning, and characterising the so-called \textit{happy flow} that a normal protocol
run follows.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys, which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to access services on the server, for example the terminal service.
At a high level, a typical SSH protocol run uses the three constituent protocols in the order given above: after the client establishes a TCP connection with the server, (1) the two sides use the Transport layer protocol to negotiate key exchange and encryption algorithms, and use these to establish session keys, which are then used to secure further communication; (2) the client uses the user authentication protocol to authenticate to the server; (3) the client uses the connection protocol to access services on the server, for example the terminal service.
%Different layers are identified by their message numbers. These message numbers will form the basis of the state fuzzing. The SSH protocol is especially interesting because outer layers do not encapsulate inner layers. This means that different layers can interact. One could argue that this is a less systematic approach, in which a programmer is more likely to make state machine-related errors.
......@@ -33,7 +33,7 @@ Subsequently, key exchange using the negotiated algorithm takes place. Following
\begin{figure}[!hb]
%\vspace{-1cm}
\includegraphics[scale=0.285]{hf-trans_cropped.pdf}
\caption{The happy flow for the transport layer.}
\caption{The happy flow for the Transport layer.}
\label{fig:hf-trans}
\vspace{-3mm}
\end{figure}
......@@ -53,7 +53,7 @@ Once a secure tunnel has been established, the client can authenticate. For this
\begin{figure}[!ht]
%\vspace{-1cm}
\includegraphics[scale=0.45]{hf-auth_cropped.pdf}
\caption{The happy flow for the user authentication layer.}
\caption{The happy flow for the user Authentication layer.}
\label{fig:hf-auth}
\vspace{-3mm}
\end{figure}
......@@ -61,7 +61,7 @@ Once a secure tunnel has been established, the client can authenticate. For this
\subsection{Connection layer}\label{ssh-run-conn}
Successful authentication makes services of the connection layer available. The connection layer enables the user to open and close channels of various types, with each type providing access to specific services. Of the various services available, we focus on the remote terminal over a session channel, a classical use of SSH. The happy flow consists of opening a session channel, \textsc{ch\_open}, requesting a ``pseudo terminal'' \textsc{ch\_request\_pty}, optionally sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}, as depicted in Figure~\ref{fig:hf-conn}.
Successful authentication makes services of the Connection layer available. The Connection layer enables the user to open and close channels of various types, with each type providing access to specific services. Of the various services available, we focus on the remote terminal over a session channel, a classical use of SSH. The happy flow consists of opening a session channel, \textsc{ch\_open}, requesting a ``pseudo terminal'' \textsc{ch\_request\_pty}, optionally sending and managing data via the messages \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}, and eventually closing the channel via \textsc{ch\_close}, as depicted in Figure~\ref{fig:hf-conn}.
%\marginpar{\tiny Erik: to match this text, the figure should include a cycle
%for \textsc{ch\_send\_data}, \textsc{ch\_window\_adjust}, \textsc{ch\_send\_eof}??}
......@@ -73,7 +73,7 @@ Successful authentication makes services of the connection layer available. The
\begin{figure}[!ht]
%\vspace{-1cm}
\includegraphics[scale=0.35]{hf-conn_cropped.pdf}
\caption{The happy flow for the connection layer.}
\caption{The happy flow for the Connection layer.}
\label{fig:hf-conn}
\vspace{-3mm}
\end{figure}
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