Paul Fiterău-Broştean
ABSTRACT
We apply model learning on three SSH implementations to infer state machine models, and then use model checking to verify that these models satisfy basic security properties and conform to the RFCs. Our analysis showed that all tested SSH server models satisfy the stated security properties, but uncovered several violations of the standard.
- F. Aarts, P. Fiterău-Broştean, H. Kuppens, and F.W. Vaandrager. 2015. Learning Register Automata with Fresh Value Generation. In ICTAC 2015 (LNCS), Vol. 9399. Google Scholar
Digital Library
- Springer, 165–183.Google Scholar
- F. Aarts, B. Jonsson, J. Uijen, and F.W. Vaandrager. 2015. Generating Models of Infinite-State Communication Protocols using Regular Inference with Abstraction. FMSD 46, 1 (2015), 1–41. Google ScholarDigital Library
- F. Aarts, J. de Ruiter, and E. Poll. 2013. Formal Models of Bank Cards for Free. In Software Testing, Verification and Validation Workshops (ICSTW). IEEE, 461–468. Google ScholarDigital Library
- F. Aarts, J. Schmaltz, and F. Vaandrager. 2010. Inference and Abstraction of the Biometric Passport. In Leveraging Applications of Formal Methods, Verification, and Validation. LNCS, Vol. 6415. Springer, 673–686. Google ScholarDigital Library
- M.R. Albrecht, K.G. Paterson, and G.J. Watson. 2009. Plaintext Recovery Attacks against SSH. In SP’09. IEEE, Washington, DC, USA, 16–26. Google ScholarDigital Library
- D. Angluin. 1987. Learning regular sets from queries and counterexamples. Inf. and Comp. 75, 2 (Nov. 1987), 87–106. Google ScholarDigital Library
- M. Bellare, T. Kohno, and C. Namprempre. 2004. Breaking and Provably Repairing the SSH Authenticated Encryption Scheme: A Case Study of the Encode-then-Encrypt-and-MAC Paradigm. ACM Trans. Inf. Syst. Secur. 7, 2 (2004), 206–241. Google ScholarDigital Library
- B. Beurdouche, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P.-Y. Strub, and J. K. Zinzindohoue. 2017. A Messy State of the Union: Taming the Composite State Machines of TLS. CACM 60, 2 (2017), 99–107. Google ScholarDigital Library
- E. Boss. 2012.Google Scholar
- Evaluating implementations of SSH by means of model-based testing. Bachelor’s Thesis. Radboud University.Google Scholar
- S. Cassel, F. Howar, and B. Jonsson. 2015.Google Scholar
- RALib: A LearnLib extension for inferring EFSMs. In DIFTS. http://www.faculty.ece.vt.edu/chaowang/difts2015/ papers/paper_5.pdfGoogle Scholar
- G. Chalupar, S. Peherstorfer, E. Poll, and J. de Ruiter. 2014. Automated Reverse Engineering using LEGO. In Proc. USENIX workshop on Offensive Technologies (WOOT’14). 1–10. Google ScholarDigital Library
- H. Chen, D. Dean, and D. Wagner. 2004. Model Checking One Million Lines of C Code. In NDSS. The Internet Society. http://www.isoc.org/isoc/conferences/ ndss/04/proceedings/Papers/Chen.pdfGoogle Scholar
- A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. 2002. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In CAV (LNCS), Vol. 2404. Springer, 359–364. Google ScholarDigital Library
- P. Fiterău-Broştean, R. Janssen, and F.W. Vaandrager. 2016. Combining Model Learning and Model Checking to Analyze TCP Implementations. In CAV’16 (LNCS), Vol. 9780. Springer, 454–471.Google Scholar
- A. Futoransky and E. Kargieman. 1998.Google Scholar
- An attack on CRC-32 integrity checks of encrypted channels using CBC and CFB modes. Online. https://www.coresecurity.com/system/files/publications/2016/05/ KargiemanPacettiRicharte_1998-CRC32.pdf, (1998).Google Scholar
- O. Grinchtein, B. Jonsson, and M. Leucker. 2010. Learning of event-recording automata. TCS 411, 47 (2010), 4029–4054. Google ScholarDigital Library
- M. Isberner. 2015.Google Scholar
- Foundations of Active Automata Learning: An Algorithmic Perspective. Ph.D. Dissertation. TU Dortmund.Google Scholar
- D. Lee and M. Yannakakis. 1996. Principles and methods of testing finite state machines — a survey. Proc. IEEE 84, 8 (1996), 1090–1123.Google ScholarCross Ref
- T. Lenaerts. 2016.Google Scholar
- Improving Protocol State Fuzzing of SSH. Bachelor’s Thesis. Radboud University.Google Scholar
- K.G. Paterson and G.J. Watson. 2010. Plaintext-Dependent Decryption: A Formal Security Treatment of SSH-CTR. In EUROCRYPT 2010. LNCS, Vol. 6110. Springer, 345–361. Google ScholarDigital Library
- D. Peled, M.Y. Vardi, and M. Yannakakis. 2002. Black Box Checking. Journal of Automata, Languages, and Combinatorics 7, 2 (2002), 225–246. Google Scholar
- E. Poll and A. Schubert. 2007. Verifying an implementation of SSH. In WITS’07. 164–177.Google Scholar
- E. Poll and A. Schubert. 2011.Google Scholar
- Rigorous specifications of the SSH Transport Layer. Technical Report. Radboud University.Google Scholar
- H. Raffelt, B. Steffen, T. Berg, and T. Margaria. 2009. LearnLib: a framework for extrapolating behavioral models. STTT 11, 5 (2009), 393–407. Google ScholarDigital Library
- J. de Ruiter and E. Poll. 2015. Protocol State Fuzzing of TLS Implementations. In USENIX Security. USENIX Association, Washington, D.C., 193–206. Google ScholarDigital Library
- W. Smeenk, J. Moerman, D.N. Jansen, and F.W. Vaandrager. 2015. Applying Automata Learning to Embedded Control Software. In ICFEM 2015 (LNCS), Vol. 9407.Google Scholar
- Springer, 1–17.Google Scholar
- O. Udrea, C. Lumezanu, and J.S. Foster. 2008. Rule-based static analysis of network protocol implementations. Inf. and Comp. 206, 2-4 (2008), 130–157. Google ScholarDigital Library
- F.W. Vaandrager. 2017. Model Learning. CACM 60, 2 (2017), 86–95. Google ScholarDigital Library
- P. Verleg. 2016.Google Scholar
- Inferring SSH state machines using protocol state fuzzing. Master’s thesis. Radboud University.Google Scholar
- Y. Wang, Z. Zhang, D. Yao, B. Qu, and L. Guo. 2011. Inferring Protocol State Machine from Network Traces: A Probabilistic Approach. In Applied Cryptography and Network Security. LNCS, Vol. 6715. Springer, 1–18. Google ScholarDigital Library
- S.C. Williams. 2011. Analysis of the SSH Key Exchange Protocol. In Cryptography and Coding. LNCS, Vol. 7089. Springer, 356–374. Google ScholarDigital Library
- T. Ylonen and C. Lonvick. 2006. The Secure Shell (SSH) Authentication Protocol. RFC 4252, IETF, Network Working Group. (2006).Google Scholar
- T. Ylonen and C. Lonvick. 2006. The Secure Shell (SSH) Connection Protocol. RFC 4254, IETF, Network Working Group. (2006).Google Scholar
- T. Ylonen and C. Lonvick. 2006. The Secure Shell (SSH) Protocol Architecture. RFC 4251, IETF, Network Working Group. (2006).Google Scholar
- T. Ylonen and C. Lonvick. 2006. The Secure Shell (SSH) Transport Layer Protocol. RFC 4253, IETF, Network Working Group. (2006).Google Scholar
Index Terms
- Model learning and model checking of SSH implementations
Recommendations
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technologyModel checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software EngineeringSoftware model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
Fair stateless model checking
PLDI '08Stateless model checking is a useful state-space exploration technique for systematically testing complex real-world software. Existing stateless model checkers are limited to the verification of safety properties on terminating programs. However, ...
Comments