Skip to main content

A Language-Theoretic View on Network Protocols

  • Conference paper
  • First Online:
Automated Technology for Verification and Analysis (ATVA 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10482))

Abstract

Input validation is the first line of defense against malformed or malicious inputs. It is therefore critical that the validator (which is often part of the parser) is free of bugs.

To build dependable input validators, we propose using parser generators for context-free languages. In the context of network protocols, various works have pointed at context-free languages as falling short to specify precisely or concisely common idioms found in protocols. We review those assessments and perform a rigorous, language-theoretic analysis of several common protocol idioms. We then demonstrate the practical value of our findings by developing a modular, robust, and efficient input validator for HTTP relying on context-free grammars and regular expressions.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This implies it has no “compact” specification by a finite state automaton either.

  2. 2.

    \(f(n)=\varOmega (g(n)) \text { iff } \exists \text { positive } c,n_0 \text { s.t. } \forall n>n_0, \;f(n) \ge c\cdot g(n)\).

  3. 3.

    https://www.gnu.org/software/bison/manual/html_node/GLR-Parsers.html.

  4. 4.

    We run our experiments on an Intel Core i5-5200U CPU 2.20 GHz with 8 GB RAM.

  5. 5.

    https://www.bro.org/.

References

  1. Internet Protocol. RFC 791 (Proposed Standard), September 1981

    Google Scholar 

  2. Bangert, J., Zeldovich, N.: Nail: a practical tool for parsing and generating data formats. In: 11th USENIX Symposium on Operating Systems Design and Implementation (2014)

    Google Scholar 

  3. Bernardy, J.-P., Jansson, P.: Certified context-free parsing: a formalisation of valiant’s algorithm in agda. Logical Methods Comput. Sci. 12(2) (2016)

    Google Scholar 

  4. Borisov, N., Brumley, D., Wang, H.J., Dunagan, J., Joshi, P., Guo, C.: Generic application-level protocol analyzer and its language. In: NDSS 2007 (2007)

    Google Scholar 

  5. Brough, T.: Groups with poly-context-free word problem. Groups Complexity Cryptol. 6(1) (2014)

    Google Scholar 

  6. Crocker, P.D. (ed.): Brandenburg InternetWorking. Augmented BNF for Syntax Specifications: ABNF. RFC 5234 (Proposed Standard), January 2008

    Google Scholar 

  7. Davidson, D., Smith, R., Doyle, N., Jha, S.: Protocol normalization using attribute grammars. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 216–231. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04444-1_14

    Chapter  Google Scholar 

  8. Faronov, V.: HTTPolice (2017). https://github.com/vfaronov/httpolice

  9. Fielding, R., Reschke, J.: Hypertext Transfer Protocol (HTTP/1.1): Message Syntax and Routing. RFC 7230 (Proposed Standard), June 2014

    Google Scholar 

  10. Filmus, Y.: Lower bounds for context-free grammars. Inf. Process. Lett. 111(18) (2011)

    Google Scholar 

  11. Firsov, D., Uustalu, T.: Certified CYK parsing of context-free languages. J. Logical Algebraic Methods Program. 83(5–6) (2014)

    Google Scholar 

  12. Freed, N., Borenstein, N.: Multipurpose internet mail extensions (MIME). RFC 1341 (Proposed Standard), November 1996

    Google Scholar 

  13. Graham-Cumming, J.: Inside shellshock: How hackers are using it to exploit systems. https://blog.cloudflare.com/inside-shellshock/

  14. Lastpass security updates. https://blog.lastpass.com/2016/07/lastpass-security-updates.html/

  15. Latteux, M.: Intersections de langages algébriques bornés. Acta Informatica 11(3) (1979)

    Google Scholar 

  16. Li, Z., Xia, G., Gao, H., Tang, Y., Chen, Y., Liu, B., Jiang, J., Lv, Y.: NetShield: massive semantics-based vulnerability signature matching for high-speed networks. In: ACM SIGCOMM 2010 (2010)

    Google Scholar 

  17. Liu, L.Y., Weiner, P.: An infinite hierarchy of intersections of context-free languages. Math. Syst. Theory 7(2) (1973)

    Google Scholar 

  18. Meiners, C.R., Norige, E., Liu, A.X., Torng, E.: Flowsifter: a counting automata approach to layer 7 field extraction for deep flow inspection. In: IEEE INFOCOM 2012 (2012)

    Google Scholar 

  19. Microsoft releases security advisory 2953095. https://technet.microsoft.com/library/security/2953095

  20. Mockapetris, P.: Domain Names - Implementation and Specification. RFC 1035 (Proposed Standard), November 1987

    Google Scholar 

  21. Pang, R., Paxson, V., Sommer, R., Peterson, L.L.: Binpac: a Yacc for writing application protocol parsers. In: ACM SIGCOMM IMC 2006 (2006)

    Google Scholar 

  22. Postel, J.: User Datagram Protocol. RFC 768 (Proposed Standard), August 1980

    Google Scholar 

  23. Rosenberg, J., Schulzrinne, H., Camarillo, G., Johnston, A., Peterson, J., Sparks, R., Handley, M., Schooler, E.: SIP: Session Initiation Protocol. RFC 3261 (Proposed Standard), June 2002

    Google Scholar 

  24. Valero, P.: HTTPValidator, April 2017. https://github.com/pevalme/HTTPValidator

  25. Ganty, P., Köpf, B., Valero, P.: A Language-theoretic View on Network Protocols (2016). (long version). Pre-print arXiv: https://arxiv.org/abs/1610.07198

Download references

Acknowledgments

We thank Juan Caballero for feedback on an early version of this paper. This work was supported by Ramón y Cajal grant RYC-2014-16766, Spanish projects TIN2015-70713-R DEDETIS, TIN2015-71819-P RISCO, TIN2012-39391-C04-01 StrongSoft, and Madrid regional project S2013/ICE-2731 N-GREENS.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Pedro Valero .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Ganty, P., Köpf, B., Valero, P. (2017). A Language-Theoretic View on Network Protocols. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68167-2_24

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68166-5

  • Online ISBN: 978-3-319-68167-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics