Commit b1f395e6 authored by Frits Vaandrager's avatar Frits Vaandrager
Browse files

minor edits intro

parent 3fcdc57a
......@@ -2,7 +2,7 @@
The SSH protocol is used interact securely with remote machines. Alongside TLS and IPSec, SSH is among the most frequently used network security protocols~\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.
SSH has been subjected to various security analyses \cite{Albrecht2009Plaintext,Bellare2004Breaking,Williams2011Analysis,Paterson2010PlaintextDependent}.
Formal methods have been applied in analysing implmentations of
Formal methods have been applied in analysing implementations of
SSH: Protocol state machines of SSH's transport layer
were used in a manual code review of OpenSSH
\cite{Poll_rigorous_2011} and a formal program verification of a Java
......@@ -13,10 +13,11 @@ two implementations of SSH against an extensive set of rules.
%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, or simply, model learning, to infer state machines of three SSH implementations, which we then verify by model checking.
Model learning has previously been applied to infer state machines of EMV bank cards~\cite{Aarts2013Formal}, electronic passports~\cite{Aarts2010Inference}, hand-held readers for online banking~\cite{Chalupar2014Automated}, and implementations of TCP~\cite{TCP2016} and TLS~\cite{RuiterProtocol}. Model learning aims to obtain a state machine 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\cite{LeeY96}, 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. Any anomalies are then exposed in the learned model.
In this work, we use model learning (a.k.a.\ active automata learning) \cite{Angluin1987Learning,Vaa17},
to infer state machines of three SSH implementations, which we then verify by model checking.
Model learning has previously been applied to infer state machines of EMV bank cards~\cite{Aarts2013Formal}, electronic passports~\cite{Aarts2010Inference}, hand-held readers for online banking~\cite{Chalupar2014Automated}, and implementations of TCP~\cite{TCP2016} and TLS~\cite{RuiterProtocol}. Model learning aims to obtain a state machine 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 \cite{LeeY96}, 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. Any anomalies are then exposed in the learned model.
Having obtained models, we use model checking to automatically verify their conformance to both functional and security properties. The properties are drawn out of the RFC specifications\cite{rfc4251,rfc4252,rfc4253,rfc4254} and formalized in LTL. They are then checked for truth on the learned model using NuSMV~\cite{NuSMV}. Manually verifying these properties would be difficult, as the learned models are reasonably large. Moreover, formalizing properties means we can also better assess and overcome vagueness or under-specification in the RFC standards.
Having obtained models, we use model checking to automatically verify their conformance to both functional and security properties. The properties are drawn out of the RFC specifications \cite{rfc4251,rfc4252,rfc4253,rfc4254} and formalized in LTL. They are then checked for truth on the learned model using NuSMV~\cite{NuSMV2}. Manually verifying these properties would be difficult, as the learned models are reasonably large. Moreover, formalizing properties means we can also better assess and overcome vagueness or under-specification in the RFC standards.
%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.
......
......@@ -94,9 +94,9 @@ tabsize=2
We apply protocol state fuzzing on three SSH implementations to infer state machines, 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 only
satisf the functional properties
only by a varying degree . Moreover, the state machines of the
implementations differ significantly, allowing them to be
satisfy the functional properties
only by a varying degree. Moreover, 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.
......
@inproceedings{NuSMV2,
author = {Alessandro Cimatti and
Edmund M. Clarke and
Enrico Giunchiglia and
Fausto Giunchiglia and
Marco Pistore and
Marco Roveri and
Roberto Sebastiani and
Armando Tacchella},
title = {NuSMV 2: An OpenSource Tool for Symbolic Model Checking},
booktitle = {Computer Aided Verification, 14th International Conference, {CAV}
2002,Copenhagen, Denmark, July 27-31, 2002, Proceedings},
pages = {359--364},
year = {2002},
editor = {Ed Brinksma and
Kim Guldstrand Larsen},
series = {Lecture Notes in Computer Science},
volume = {2404},
publisher = {Springer},
}
@misc{NuSMV,
title = {The NuSMV Model Checker},
howpublished = "\url{http://nusmv.fbk.eu/}",
......@@ -549,3 +570,15 @@ machine learning algorithms},
pages = {164-177},
}
@article{Vaa17,
author = {F.W. Vaandrager},
journal = {Communications of the ACM},
title = {Model Learning},
volume = {60},
number = {2},
month = feb,
year = {2017},
pages = {86--95},
publisher = {ACM},
address = {New York, NY, USA},
}
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