introduction.tex 7.47 KB
Newer Older
 Paul Fiterau Brostean committed Jan 18, 2017 1 2 \section{Introduction}\label{introduction}  Frits Vaandrager committed Feb 17, 2017 3 SSH is a security protocol that is widely used to interact securely with  Paul Fiterau Brostean committed Feb 17, 2017 4 remote machines. The Transport layer of SSH has been subjected to security analysis  Erik Poll committed Feb 16, 2017 5 6 7 \cite{Williams2011Analysis}, incl.\ analyses that revealed cryptographic shortcomings \cite{Albrecht2009Plaintext,Bellare2004Breaking,Paterson2010PlaintextDependent}.  Paul Fiterau Brostean committed Jan 18, 2017 8   Paul Fiterau Brostean committed Feb 17, 2017 9 Whereas these analyses consider the abstract cryptographic  Erik Poll committed Feb 16, 2017 10 11 12 13 14 15 protocol, this paper looks at actual implementations of SSH, and investigates flaws in the program logic of these implementations, rather than cryptographic flaws. Such logical flaws have occurred in implementations of other security protocols, notably TLS, with Apple's 'goto fail' bug and the FREAK attack \cite{Beurdouche:2017}. For this we use model learning (a.k.a.\ active automata learning)  Frits Vaandrager committed Feb 17, 2017 16 \cite{Angluin1987Learning,PeVaYa02,Vaa17} to infer state machines of three SSH  Paul Fiterau Brostean committed Feb 16, 2017 17 implementations, which we then analyze by model checking for  Erik Poll committed Feb 16, 2017 18 conformance to both functional and security properties.  Paul Fiterau Brostean committed Jan 18, 2017 19   Erik Poll committed Feb 16, 2017 20 21 22 The properties we verify for the inferred state machines are based on the RFCs that specify SSH \cite{rfc4251,rfc4252,rfc4253,rfc4254}. These properties are formalized in LTL and verified using  Frits Vaandrager committed Feb 17, 2017 23 24 25 26 NuSMV~\cite{NuSMV2}. We use a model checker since the models are too complex for manual inspection (they are trivial for NuSMV). Moreover, by formalizing the properties we can better assess and overcome vagueness or  Erik Poll committed Feb 16, 2017 27 under-specification in the RFC standards.  Paul Fiterau Brostean committed Jan 18, 2017 28   Paul Fiterau Brostean committed Feb 17, 2017 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43  This paper is born out of two recent theses \cite{Verleg2016,Toon2016}, and is to our knowledge the first combined application of model learning and model checking in verifying SSH implementations, or more generally, implementations of any network security protocol. %Model learning obtains a state machine model of a black-box system by %providing inputs and observing outputs. Since model learning uses 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 complete. In the context of testing security protocols, model %learning can be seen as a form of fuzzing, where inputs are sent in %unexpected orders to expose any hidden anomalies.  Paul Fiterau Brostean committed Feb 13, 2017 44   Erik Poll committed Feb 16, 2017 45 \paragraph{Related work}  Paul Fiterau Brostean committed Feb 13, 2017 46   Erik Poll committed Feb 16, 2017 47 48 49 50 %The SSH protocol has been investigated for cryptographic flaws, e.g.\ %\cite{Williams2011Analysis,Albrecht2009Plaintext,Bellare2004Breaking,Paterson2010PlaintextDependent}, %but that research does not consider logical flaws in actual software %implementations.  Paul Fiterau Brostean committed Feb 13, 2017 51   Frits Vaandrager committed Feb 17, 2017 52 53 54 55 Chen et al.\cite{ChenDW04} use the MOPS software model checking tool to detect security vulnerabilities in the OpenSSH C implementation due to violation of folk rules for the construction of secure programs such as Do not open a file in writing mode to stdout or stderr''.  Erik Poll committed Feb 16, 2017 56 57 58 59 60 61 62 63 64 Udrea et al.\cite{Udrea_rule-based_2008} also investigated SSH implementations for logical flaws. They used a static analysis tool to check two C implementations of SSH against an extensive set of rules. These rules not only express properties of the SSH protocol logic, but also of message formats and support for earlier versions and various options. Our analysis only considers the protocol logic. However, their rules were tied to routines in the code, so had to be slightly adapted to fit the different implementations. In contrast, our properties are defined at an abstract level so do not need such tailoring. Moreover,  Erik Poll committed Feb 17, 2017 65 our black box approach means we can analyze any implementation  Paul Fiterau Brostean committed Feb 17, 2017 66 of SSH, not just open source C implementations.  Paul Fiterau Brostean committed Feb 13, 2017 67   Frits Vaandrager committed Feb 17, 2017 68   Erik Poll committed Feb 16, 2017 69 70 71 72 73 74 75 Formal models of SSH in the form of state machines have been used 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 protocol layers.  Paul Fiterau Brostean committed Feb 13, 2017 76   Erik Poll committed Feb 17, 2017 77 Model learning has previously been used to infer state machines of  Erik Poll committed Feb 16, 2017 78 79 80 81 82 83 84 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}. Some of these case studies relied on manual analysis of the learned models \cite{Aarts2013Formal,Aarts2010Inference,RuiterProtocol}, but some also used model checkers \cite{TCP2016,Chalupar2014Automated}.  Paul Fiterau Brostean committed Jan 20, 2017 85   Erik Poll committed Feb 16, 2017 86 87 88 89 Instead of using active learning as we do, it is also possible to use passive learning to obtain protocol state machines \cite{Wang2011Inferring}. Here network traffic is observed, and not actively generated. This can then also provide a probabilistic  Paul Fiterau Brostean committed Feb 16, 2017 90 characterization of normal network traffic, but it cannot uncover  Erik Poll committed Feb 16, 2017 91 92 implementation flaws that occur in strange message flows, which is our goal.  Paul Fiterau Brostean committed Jan 18, 2017 93   Erik Poll committed Feb 16, 2017 94 95 96 97 98 99 100 101 102 103 104 105 %Our approach, most closely resembles work on TCP~\cite{TCP2016}, %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 involving model learning %rely on manual analysis of the learned models %~\cite{Aarts2013Formal,TCP2016,Chalupar2014Automated,RuiterProtocol}. %Our work differs, since we use a model checker to automatically check %specifications. Inference of protocols has also been done from %observing network traffic ~\cite{Wang2011Inferring}. Such inference %is limited to the traces that occur over a network. Inference is %further hampered if the analyzed protocols communicate over encrypted %channels, as this severely limits information available from traces without knowledge of the security key.  Paul Fiterau Brostean committed Jan 18, 2017 106 107 108 109 110 111 112 113 114 115  %In this thesis, we will be using protocol state fuzzing to extract an implementations state machine. All fuzzing algorithms rely on the idea of sending unexpected input data to a system under test (SUT) in the hope that this triggers anomalies. Using protocol state fuzzing, however, we will fuzz on the \textit{order} of otherwise correctly-formed messages. %This technique 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}. Furthermore, implementations of TCP~\cite{Janssen2015Learning} and TLS~\cite{RuiterProtocol} have state-fuzzed. As in these works, we implement state fuzzing % %State machines inferred are large and hard to check manually. %Once a state machine has been inferred, security-related logical flaws are usually easily spotted by an auditor with some knowledge about the protocol~\cite{RuiterProtocol}. An example of a logical flaw is exchanging user credentials before an encrypted connection has been established. % %Besides security-related logical flaws, inferred state machines can show quirks such as superfluous states. Although these might not be directly exploitable, OpenBSD auditors illustrate why these small bugs should be resolved: we are not so much looking for security holes, as we are looking for basic software bugs, and if years later someone discovers the problem used to be a security issue, and we fixed it because it was just a bug, well, all the better''\footnote{\url{http://www.openbsd.org/security.html}}. % %\textit{Organization.} An outline of the SSH protocol will be provided in Section~\ref{ssh}. The experimental setup is discussed in Section~\ref{setup}. The results are subsequently discussed in Section~\ref{results}, after which we conclude in Section~\ref{conclusions}.  Erik Poll committed Feb 15, 2017 116 %