Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Model Checking at Scale: Automated Air Traffic Control Design Space Exploration Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Combining Model Learning and Model Checking to Analyze TCP Implementations

verfasst von : Paul Fiterău-Broştean, Ramon Janssen, Frits Vaandrager

Erschienen in: Computer Aided Verification

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We combine model learning and model checking in a challenging case study involving Linux, Windows and FreeBSD implementations of TCP. We use model learning to infer models of different software components and then apply model checking to fully explore what may happen when these components (e.g. a Linux client and a Windows server) interact. Our analysis reveals several instances in which TCP implementations do not conform to their RFC specifications.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Property Directed Equivalence via Abstract Simulation
Nächstes Kapitel BFS-Based Model Checking of Linear-Time Properties with an Application on GPUs
Fußnoten
Literatur
1.
Aarts, F.: Tomte: Bridging the Gap between Active Learning and Real-World Systems. Ph.D. thesis, Radboud University Nijmegen, October 2014
2.
Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.W.: Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods Syst. Des. 46(1), 1–41 (2015)CrossRefMATH
3.
Aarts, F., Vaandrager, F.: Learning I/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71–85. Springer, Heidelberg (2010)CrossRef
4.
Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.: Learning register automata with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 165–183. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-25150-9_​11 CrossRef
5.
Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.W.: Generat-ing models of infinite-state communication protocols using regular inference withabstraction. Formal Methods Syst. Des. 46(1), 1–41 (2015)CrossRefMATH
6.
7.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
8.
Berendsen, J., Gebremichael, B., Vaandrager, F.W., Zhang, M.: Formal specification and analysis of Zeroconf using Uppaal. ACM Trans. Embed. Comput. Syst. 10(3), 1–32 (2011)CrossRef
9.
Braden, R.: RFC 1122 Requirements for Internet Hosts - Communication Layers. Internet Engineering Task Force, October 1989
10.
Brinksma, E., Mader, A.: On verification modelling of embedded systems. Technical report TR-CTIT-04-03, Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands, January 2004
11.
Bruns, G., Staskauskas, M.G.: Applying formal methods to a protocol standard and its implementations. In: Proceedings International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE 1998), 20–21 April 1998, Kyoto, Japan, pp. 198–205. IEEE Computer Society (1998)
12.
Cassel, S.: Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data. Ph.D. thesis, University of Uppsala (2015)
13.
Chalupar, G., Peherstorfer, S., Poll, E., de Ruiter, J.: Automated reverse engineering using Lego. In: Proceedings 8th USENIX Workshop on Offensive Technologies (WOOT 2014), San Diego, California, Los Alamitos, CA, USA, IEEE Computer Society, August 2014
14.
Cho, C.Y., Babic, D., Shin, E.C.R., Song, D.: Inference and analysis of formal models of botnet command and control protocols. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) ACM Conference on Computer and Communications Security, pp. 426–439. ACM (2010)
15.
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRef
16.
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefMATH
17.
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
18.
Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Learning fragments of the TCP network protocol. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 78–93. Springer, Heidelberg (2014)
19.
Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029–4054 (2010)MathSciNetCrossRefMATH
20.
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)CrossRef
21.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Reading (2004)
22.
23.
Isberner, M: Foundations of Active Automata Learning: An Algorithmic Perspective. Ph.D. thesis, Technical University of Dortmund (2015)
24.
Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1–21:54 (2009)CrossRef
25.
26.
van Langevelde, I., Romijn, J.M.T., Goga, N.: Founding FireWire bridges through Promela prototyping. In: 8thInternational Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA). IEEE Computer Society Press, April 2003
27.
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – a survey. Proc. IEEE 84(8), 1090–1123 (1996)CrossRef
28.
Lockefeer, L., Williams, D.M., Fokkink, W.J.: Formal specification and verification of TCP extended with the window scale option. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 63–77. Springer, Heidelberg (2014)
29.
Loiseaux, C., Graf, S., Sifakis, J., Boujjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11–44 (1995)CrossRefMATH
30.
Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 134–151. Springer, Heidelberg (2011)CrossRef
31.
Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: Morris, R., Savage, S. (eds.) 1st Symposium on Networked Systems Design and Implementation (NSDI 2004), March 29–31, 2004, San Francisco, California, USA, Proceedings, pp. 155–168. USENIX (2004)
32.
Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Culler, D.E., Druschel, P. (eds.) 5th Symposium on Operating System Design and Implementation (OSDI 2002), Boston, Massachusetts, USA, December 9–11, 2002. USENIX Association (2002)
33.
34.
Paxson, V., Allman, M., Dawson, S., Fenner, W., Griner, J., Heavens, I., Lahey, K., Semke, J., Volz, B.: Known TCP Implementation Problems. RFC 2525 (Informational), March 1999
35.
36.
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225–246 (2002)MathSciNetMATH
37.
38.
Postel, J.: Transmission control protocol. RFC 793 (Standard), Updated by RFCs 1122, 3168, September 1981
39.
Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393–407 (2009)CrossRef
40.
de Ruiter, J., Poll, E.: Protocol state fuzzing of tls implementations. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 193–206. SENIX Association, Washington, D.C., August 2015
41.
42.
Shahbaz, M., Groz, R.: Analysis and testing of black-box component-based systems by inferring partial models. Softw. Test. Verif. Reliab. 24(4), 253–288 (2014)CrossRef
43.
Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67–83. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-25423-4_​5 CrossRef
44.
Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296. Springer, Heidelberg (2011)CrossRef
45.
Stoelinga, M.: Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Aspects Comput. J. 14(3), 328–337 (2003)CrossRefMATH
46.
Verleg, P.: Inferring SSH state machines using protocol state fuzzing. Master thesis, Radboud University (2016)
47.
Verwer, S.: Efficient Identification of Timed Automata – Theory and Practice. Ph.D. thesis, Delft University of Technology, March 2010
48.
Volpato, M., Tretmans, J.: Active learning of nondeterministic systems from an ioco perspective. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 220–235. Springer, Heidelberg (2014)
Metadaten
Titel
Combining Model Learning and Model Checking to Analyze TCP Implementations
verfasst von
Paul Fiterău-Broştean
Ramon Janssen
Frits Vaandrager
Copyright-Jahr
2016
Buch
Computer Aided Verification

Print ISBN: 978-3-319-41539-0

Electronic ISBN: 978-3-319-41540-6

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-41540-6_25

Premium Partner

    Bildnachweise