nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Netter: Probabilistic, Stateful Network Models

verfasst von : Han Zhang, Chi Zhang, Arthur Azevedo de Amorim, Yuvraj Agarwal, Matt Fredrikson, Limin Jia

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We study the problem of using probabilistic network models to formally analyze their quantitative properties, such as the effect of different load-balancing strategies on the long-term traffic on a server farm. Compared to prior work, we explore a different design space in terms of tradeoffs between model expressiveness and analysis scalability, which we realize in a language we call Netter. Netter code is compiled to probabilistic automata, undergoing optimization passes to reduce the state space of the generated models, thus helping verification scale. We evaluate Netter on several case studies, including a probabilistic load balancer, a routing scheme reminiscent of MPLS, and a network defense mechanism against link-flooding attacks. Our results show that Netter can analyze quantitative properties of interesting routing schemes that prior work hadn’t addressed, for networks of small size (4–9 nodes and a few different types of flows). Moreover, when specialized to simpler, stateless networks, Netter can parallel the performance of previous state-of-the-art tools, scaling up to millions of nodes.

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 Formal Semantics and Verification of Network-Based Biocomputation Circuits

Nächstes Kapitel Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories

Due to dependency issues, we only managed to run part of the experiment of Smolka et al. [27], so our comparison is mostly based on the numbers reported by the authors. While this prevents us from making a precise comparison, their setup was similar to ours, and we do not expect the performance of their code to change substantially.

In principle, since variables are bounded, it would be possible to do away with expressions by evaluating them at every possible state. However, this would result in much larger compiled models, making the analysis more costly.

Abley, J., Lindqvist, K., Davies, E., Black, B., Gill, V.: IPv4 multihoming practices and limitations. RFC 4116, RFC Editor, July 2005. http://www.rfc-editor.org/rfc/rfc4116.txt

Anderson, C.J., et al.: NetKAT: semantic foundations for networks. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 113–126. ACM (2014). https://doi.org/10.1145/2535838.2535862

Braden, B., Zhang, L., Berson, S., Herzog, S., Jamin, S.: Resource reservation protocol (RSVP) - version 1 functional specification. RFC 2205, RFC Editor, September 1997. http://www.rfc-editor.org/rfc/rfc2205.txt

Fayaz, S.K., Yu, T., Tobioka, Y., Chaki, S., Sekar, V.: BUZZ: testing context-dependent policies in stateful networks. In: 13th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2016), pp. 275–289. USENIX Association, Santa Clara (2016). https://www.usenix.org/conference/nsdi16/technical-sessions/presentation/fayaz

Foster, N., Kozen, D., Mamouras, K., Reitblatt, M., Silva, A.: Probabilistic NetKAT. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 282–309. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49498-1_12CrossRef

Gehr, T., Misailovic, S., Tsankov, P., Vanbever, L., Wiesmann, P., Vechev, M.T.: Bayonet: probabilistic inference for networks. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, 18–22 June 2018, pp. 586–602. ACM (2018). https://doi.org/10.1145/3192366.3192400

Henriksen, T.: VMCAI 2021 virtual machine, September 2020. https://doi.org/10.5281/zenodo.4017293

Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker storm. CoRR abs/2002.07080 (2020). https://arxiv.org/abs/2002.07080

Horn, A., Kheradmand, A., Prasad, M.: Delta-net: real-time network verification using atoms. In: 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2017), pp. 735–749. USENIX Association, Boston (2017). https://www.usenix.org/conference/nsdi17/technical-sessions/presentation/horn-alex

10.

Hsu, J.: Probabilistic couplings for probabilistic reasoning. CoRR abs/1710.09951 (2017). http://arxiv.org/abs/1710.09951

11.

Jensen, J.S., Krogh, T.B., Madsen, J.S., Schmid, S., Srba, J., Thorgersen, M.T.: P-Rex: fast verification of MPLS networks with multiple link failures. In: Proceedings of the 14th International Conference on Emerging Networking EXperiments and Technologies, CoNEXT 2018 (2018)

12.

Juniwal, G., Bjorner, N., Mahajan, R., Seshia, S.A., Varghese, G.: Quantitative network analysis. Technical report (2016). http://cseweb.ucsd.edu/~varghese/qna.pdf

13.

Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., Whyte, S.: Real time network policy checking using header space analysis. In: Presented as Part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2013), pp. 99–111. USENIX, Lombard (2013). https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/kazemian

14.

Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: Presented as Part of the 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2012), pp. 113–126. USENIX, San Jose (2012). https://www.usenix.org/conference/nsdi12/technical-sessions/presentation/kazemian

15.

Khurshid, A., Zou, X., Zhou, W., Caesar, M., Godfrey, P.B.: VeriFlow: verifying network-wide invariants in real time. In: Presented as Part of the 10th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2013), pp. 15–27. USENIX, Lombard (2013). https://www.usenix.org/conference/nsdi13/technical-sessions/presentation/khurshid

16.

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47CrossRef

17.

Larsen, K.G., Schmid, S., Xue, B.: WNetKAT: a weighted SDN programming and verification language. In: 20th International Conference on Principles of Distributed Systems (OPODIS 2016) (2016)

18.

Lee, S.B., Kang, M.S., Gligor, V.D.: CoDef: collaborative defense against large-scale link-flooding attacks. In: Proceedings of the Ninth ACM Conference on Emerging Networking Experiments and Technologies, CoNEXT 2013, p. 417–428. Association for Computing Machinery, New York (2013). https://doi.org/10.1145/2535372.2535398

19.

Lopes, N.P., Bjorner, N., Godefroid, P., Jayaraman, K., Varghese, G.: Checking beliefs in dynamic networks. In: 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2015), pp. 499–512. USENIX Association, Oakland (2015). https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/lopes

20.

Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. In: Proceedings of the ACM SIGCOMM 2011 Conference, SIGCOMM 2011, pp. 290–301. ACM, New York (2011). https://doi.org/10.1145/2018436.2018470

21.

Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, New York (2005)CrossRef

22.

Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), Pacific Grove, California, USA, 5–8 June 1989, pp. 14–23. IEEE Computer Society (1989). https://doi.org/10.1109/LICS.1989.39155

23.

Panda, A., Lahav, O., Argyraki, K., Sagiv, M., Shenker, S.: Verifying reachability in networks with mutable datapaths. In: 14th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2017), pp. 699–718. USENIX Association, Boston, March 2017. https://www.usenix.org/conference/nsdi17/technical-sessions/presentation/panda-mutable-datapaths

24.

Pathak, A., Zhang, M., Hu, Y.C., Mahajan, R., Maltz, D.A.: Latency inflation with MPLS-based traffic engineering. In: Thiran, P., Willinger, W. (eds.) Proceedings of the 11th ACM SIGCOMM Internet Measurement Conference, IMC 2011, Berlin, Germany, 2 November 2011, pp. 463–472. ACM (2011). https://doi.org/10.1145/2068816.2068859

25.

Smith, J.M., Schuchard, M.: Routing around congestion: defeating DDoS attacks and adverse network conditions via reactive BGP routing. In: 2018 IEEE Symposium on Security and Privacy (SP), pp. 599–617. IEEE (2018)

26.

Smolka, S., Kumar, P., Foster, N., Kozen, D., Silva, A.: Cantor meets scott: semantic foundations for probabilistic networks. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 557–571. Association for Computing Machinery, New York (2017). https://doi.org/10.1145/3009837.3009843

27.

Smolka, S., et al.: Scalable verification of probabilistic networks. In: McKinley, K.S., Fisher, K. (eds.) Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, 22–26 June 2019, pp. 190–203. ACM (2019). https://doi.org/10.1145/3314221.3314639

28.

Stoenescu, R., Popovici, M., Negreanu, L., Raiciu, C.: SymNet: scalable symbolic execution for modern networks. In: Proceedings of the 2016 Conference on ACM SIGCOMM 2016 Conference, SIGCOMM 2016, pp. 314–327. ACM, New York (2016). https://doi.org/10.1145/2934872.2934881

29.

Tarreau, W.: Test driving “power of two random choices” load balancing, April 2019. https://www.haproxy.com/blog/power-of-two-load-balancing/

30.

The Coq Development Team: The Coq proof assistant, version 8.12.0, July 2020. https://doi.org/10.5281/zenodo.4021912

31.

Tran, M., Kang, M.S., Hsiao, H.C., Chiang, W.H., Tung, S.P., Wang, Y.S.: On the feasibility of rerouting-based DDoS defenses. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1169–1184. IEEE (2019)

32.

Tschaen, B., Zhang, Y., Benson, T., Benerjee, S., Lee, J., Kang, J.M.: SFC-checker: checking the correct forwarding behavior of service function chaining. In: IEEE SDN-NFV Conference (2016)

33.

Xie, G.G., et al.: On static reachability analysis of IP networks. In: IEEE Proceedings of the 24th Annual Joint Conference of the IEEE Computer and Communications Societies, INFOCOM 2005, vol. 3, pp. 2170–2183. IEEE (2005)

34.

Xue, L., Luo, X., Chan, E.W., Zhan, X.: Towards detecting target link flooding attack. In: 28th Large Installation System Administration Conference (LISA 2014), pp. 90–105 (2014)

35.

Yang, H., Lam, S.S.: Real-time verification of network properties using atomic predicates. IEEE/ACM Trans. Netw. 24(2), 887–900 (2016). https://doi.org/10.1109/TNET.2015.2398197CrossRef

36.

Yuan, Y., Moon, S.J., Uppal, S., Jia, L., Sekar, V.: NetSMC: a custom symbolic model checker for stateful network verification. In: Bhagwan, R., Porter, G. (eds.) 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2020, Santa Clara, CA, USA, 25–27 February 2020, pp. 181–200. USENIX Association (2020). https://www.usenix.org/conference/nsdi20/presentation/yuan

37.

Zeng, H., Kazemian, P., Varghese, G., McKeown, N.: Automatic test packet generation. IEEE/ACM Trans. Netw. 22(2), 554–566 (2014). https://doi.org/10.1109/TNET.2013.2253121CrossRef

38.

Zeng, H., et al.: Libra: divide and conquer to verify forwarding tables in huge networks. In: NSDI 2014, pp. 87–99 (2014)

39.

Zhang, H., Zhang, C., Azevedo de Amorim, A., Agarwal, Y., Fredrikson, M., Jia, L.: Netter: probabilistic, stateful network models, October 2020. https://doi.org/10.5281/zenodo.4089060

Titel: Netter: Probabilistic, Stateful Network Models
verfasst von: Han Zhang
Chi Zhang
Arthur Azevedo de Amorim
Yuvraj Agarwal
Matt Fredrikson
Limin Jia
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-67066-5

Electronic ISBN: 978-3-030-67067-2

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-67067-2_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"