research-article

Public Access

Scalable verification of probabilistic networks

Authors:

Steffen Smolka,

Alexandra SilvaAuthors Info & Claims

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 190 - 203

https://doi.org/10.1145/3314221.3314639

Published: 08 June 2019 Publication History

Abstract

This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the guarded and history-free fragment of Probabilistic NetKAT in terms of finite-state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT's scalability using real-world topologies, compare its performance against state-of-the-art tools, and develop an extended case study on a recently proposed data center network design.

Supplementary Material

WEBM File (p190-smolka.webm)

Download
67.03 MB

MP4 File (3314221.3314639.mp4)

Video Presentation

Download
46.42 MB

References

[1]

S. B. Akers. 1978. Binary Decision Diagrams. IEEE Trans. Comput. 27, 6 (June 1978), 509–516.

Digital Library

[2]

Mohammad Al-Fares, Alexander Loukissas, and Amin Vahdat. 2008. A Scalable, Commodity Data Center Network Architecture. In ACM SIGCOMM Computer Communication Review, Vol. 38. ACM, 63–74.

Digital Library

[3]

Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. 2014. NetKAT: Semantic Foundations for Networks. In POPL. 113–126.

Digital Library

[4]

Manav Bhatia, Mach Chen, Sami Boutros, Marc Binderberger, and Jeffrey Haas. 2014. Bidirectional Forwarding Detection (BFD) on Link Aggregation Group (LAG) Interfaces. RFC 7130.

[5]

Pat Bosshart, Dan Daly, Glen Gibb, Martin Izzard, Nick McKeown, Jennifer Rexford, Cole Schlesinger, Dan Talayco, Amin Vahdat, George Varghese, and David Walker. 2014. P4: Programming ProtocolIndependent Packet Processors. SIGCOMM CCR 44, 3 (July 2014), 87–95.

Digital Library

[6]

Martin Casado, Nate Foster, and Arjun Guha. 2014. Abstractions for Software-Defined Networks. CACM 57, 10 (Oct. 2014), 86–95.

Digital Library

[7]

Timothy A. Davis. 2004. Algorithm 832: UMFPACK V4.3—an Unsymmetric-pattern Multifrontal Method. ACM Trans. Math. Softw. 30, 2 (June 2004), 196–199.

Digital Library

[8]

Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. 2005. Probabilistic λ-calculus and quantitative program analysis. Journal of Logic and Computation 15, 2 (2005), 159–179.

Digital Library

[9]

Roger Dingledine, Nick Mathewson, and Paul Syverson. 2004. Tor: The Second-generation Onion Router. In USENIX Security Symposium (SSYM). 21–21.

Digital Library

[10]

A. Dixit, P. Prakash, Y. C. Hu, and R. R. Kompella. 2013. On the impact of packet spraying in data center networks. In IEEE INFOCOM. 2130– 2138.

[11]

Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. 282–309.

[12]

Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. 2015. A Coalgebraic Decision Procedure for NetKAT. In POPL. ACM, 343–355.

Digital Library

[13]

M. Fujita, P. C. McGeer, and J. C.-Y. Yang. 1997. Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation. Form. Methods Syst. Des. 10, 2-3 (April 1997), 149–169.

Digital Library

[14]

Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin T. Vechev. 2018. Bayonet: Probabilistic Computer Network Analysis. Available at https://github.com/eth-sri/ bayonet/ .

[15]

Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin T. Vechev. 2018. Bayonet: probabilistic inference for networks. In ACM SIGPLAN PLDI. 586–602.

Digital Library

[16]

Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. 62–83.

[17]

Phillipa Gill, Navendu Jain, and Nachiappan Nagappan. 2011. Understanding Network Failures in Data Centers: Measurement, Analysis, and Implications. In ACM SIGCOMM. 350–361.

Digital Library

[18]

Andrew D Gordon, Thomas A Henzinger, Aditya V Nori, and Sriram K Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering. ACM, 167–181.

Digital Library

[19]

Peyman Kazemian, George Varghese, and Nick McKeown. 2012. Header Space Analysis: Static Checking for Networks. In USENIX NSDI 2012. 113–126. https://www.usenix.org/conference/nsdi12/ technical-sessions/presentation/kazemian

Digital Library

[20]

John G Kemeny and James Laurie Snell. 1960. Finite markov chains. Vol. 356. van Nostrand Princeton, NJ.

[21]

Ahmed Khurshid, Wenxuan Zhou, Matthew Caesar, and Brighten Godfrey. 2012. Veriflow: Verifying Network-Wide Invariants in Real Time. In ACM SIGCOMM. 467–472.

Digital Library

[22]

Praveen Kumar, Yang Yuan, Chris Yu, Nate Foster, Robert Kleinberg, Petr Lapukhov, Chiun Lin Lim, and Robert Soulé. 2018. Semi-Oblivious Traffic Engineering: The Road Not Taken. In USENIX NSDI.

Digital Library

[23]

M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV’11) (LNCS), G. Gopalakrishnan and S. Qadeer (Eds.), Vol. 6806. Springer, 585–591.

Digital Library

[24]

Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV. 585–591.

Digital Library

[25]

Jed Liu, William Hallahan, Cole Schlesinger, Milad Sharif, Jeongkeun Lee, Robert Soulé, Han Wang, Calin Cascaval, Nick McKeown, and Nate Foster. 2018. p4v: Practical Verification for Programmable Data Planes. In SIGCOMM. 490–503.

[26]

Vincent Liu, Daniel Halperin, Arvind Krishnamurthy, and Thomas E Anderson. 2013. F10: A Fault-Tolerant Engineered Network. In USENIX NSDI. 399–412.

Digital Library

[27]

Haohui Mai, Ahmed Khurshid, Rachit Agarwal, Matthew Caesar, P. Brighten Godfrey, and Samuel Talmadge King. 2011. Debugging the Data Plane with Anteater. In ACM SIGCOMM. 290–301.

Digital Library

[28]

Nick McKeown, Tom Anderson, Hari Balakrishnan, Guru Parulkar, Larry Peterson, Jennifer Rexford, Scott Shenker, and Jonathan Turner. 2008. OpenFlow: Enabling Innovation in Campus Networks. SIGCOMM CCR 38, 2 (2008), 69–74.

Digital Library

[29]

Maciej Olejnik, Herbert Wiklicky, and Mahdi Cheraghchi. 2016. Probabilistic Programming and Discrete Time Markov Chains. http://www.imperial.ac.uk/media/imperial-college/ faculty-of-engineering/computing/public/MaciejOlejnik.pdf

[30]

Arjun Roy, Hongyi Zeng, Jasmeet Bagga, George Porter, and Alex C. Snoeren. 2015. Inside the Social Network’s (Datacenter) Network. In ACM SIGCOMM. 123–137.

Digital Library

[31]

Vyas Sekar, Michael K. Reiter, Walter Willinger, Hui Zhang, Ramana Rao Kompella, and David G. Andersen. 2008. CSAMP: A System for Network-wide Flow Monitoring. In USENIX NSDI. 233–246.

Digital Library

[32]

Micha Sharir, Amir Pnueli, and Sergiu Hart. 1984. Verification of probabilistic programs. SIAM J. Comput. 13, 2 (1984), 292–314.

Digital Library

[33]

Rachee Singh, Manya Ghobadi, Klaus-Tycho Foerster, Mark Filer, and Phillipa Gill. 2018. RADWAN: Rate Adaptive Wide Area Network. In ACM SIGCOMM.

Digital Library

[34]

Steffen Smolka, Spiros Eliopoulos, Nate Foster, and Arjun Guha. 2015. A Fast Compiler for NetKAT. In ICFP 2015.

Digital Library

[35]

Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. 2017. Cantor Meets Scott: Semantic Foundations for Probabilistic Networks. In POPL 2017.

Digital Library

[36]

Steffen Smolka, Praveen Kumar, David M Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks (Extended Version). arXiv (2019). arXiv: 1904.08096

[37]

Ken Thompson. 1968. Regular Expression Search Algorithm. Commun. ACM 11, 6 (1968), 419–422.

Digital Library

[38]

L. Valiant. 1982. A Scheme for Fast Parallel Communication. SIAM J. Comput. 11, 2 (1982), 350–361.

Digital Library

[39]

Di Wang, Jan Hoffmann, and Thomas Reps. 2018. PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs. In POPL 2018. https://www.cs.cmu.edu/~janh/papers/WangHR17.pdf

Digital Library

[40]

Geoffrey G. Xie, Jibin Zhan, David A. Maltz, Hui Zhang, Albert G. Greenberg, Gísli Hjálmtýsson, and Jennifer Rexford. 2005. On static reachability analysis of IP networks. In INFOCOM.

[41]

Zhiyong Zhang, Ovidiu Mara, and Katerina Argyraki. 2014. Network Neutrality Inference. In ACM SIGCOMM. 63–74.

Digital Library

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Buckley AChuprikov POtoni RSoulé RRand REugster P(2024)An Algebraic Language for Specifying Quantum NetworksProceedings of the ACM on Programming Languages10.1145/36564308:PLDI(1313-1335)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656430
Mertens HKatoen JQuatmann TWinkler T(2024)Accurately Computing Expected Visiting Times and Stationary Distributions in Markov ChainsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_12(237-257)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_12
Show More Cited By

Index Terms

Scalable verification of probabilistic networks

Recommendations

ProbNV: probabilistic verification of network control planes

ProbNV is a new framework for probabilistic network control plane verification that strikes a balance between generality and scalability. ProbNV is general enough to encode a wide range of features from the most common protocols (eBGP and OSPF) and yet ...
Probabilistic relational verification for cryptographic implementations
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Relational program logics have been used for mechanizing formal proofs of various cryptographic constructions. With an eye towards scaling these successes towards end-to-end security proofs for implementations of distributed systems, we present RF*, a ...
Expressing and verifying probabilistic assertions
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

Traditional assertions express correctness properties that must hold on every program execution. However, many applications have probabilistic outcomes and consequently their correctness properties are also probabilistic (e.g., they identify faces in ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2019

1162 pages

ISBN:9781450367127

DOI:10.1145/3314221

General Chair:
Kathryn S. McKinley
Google, USA
,
Program Chair:
Kathleen Fisher
Tufts University, USA

Copyright © 2019 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 08 June 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '19

Sponsor:

SIGPLAN

PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 22 - 26, 2019

AZ, Phoenix, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
593
Total Downloads

Downloads (Last 12 months)99
Downloads (Last 6 weeks)10

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Moeller MJacobs JBelanger ODarais DSchlesinger CSmolka SFoster NSilva A(2024)KATch: A Fast Symbolic Verifier for NetKATProceedings of the ACM on Programming Languages10.1145/36564548:PLDI(1905-1928)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656454
Buckley AChuprikov POtoni RSoulé RRand REugster P(2024)An Algebraic Language for Specifying Quantum NetworksProceedings of the ACM on Programming Languages10.1145/36564308:PLDI(1313-1335)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656430
Mertens HKatoen JQuatmann TWinkler T(2024)Accurately Computing Expected Visiting Times and Stationary Distributions in Markov ChainsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57249-4_12(237-257)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57249-4_12
Li JAhmed AHoltzen S(2023)Lilac: A Modal Separation Logic for Conditional ProbabilityProceedings of the ACM on Programming Languages10.1145/35912267:PLDI(148-171)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591226
Das AWang DHoffmann J(2023)Probabilistic Resource-Aware Session TypesProceedings of the ACM on Programming Languages10.1145/35712597:POPL(1925-1956)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571259
Kappé TSchmid TSilva A(2023)A Complete Inference System for Skip-free Guarded Kleene Algebra with TestsProgramming Languages and Systems10.1007/978-3-031-30044-8_12(309-336)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_12
Giannarakis NSilva AWalker D(2021)ProbNV: probabilistic verification of network control planesProceedings of the ACM on Programming Languages10.1145/34735955:ICFP(1-30)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473595
Sonchack JLoehr DRexford JWalker DKuipers FCaesar M(2021)LucidProceedings of the 2021 ACM SIGCOMM 2021 Conference10.1145/3452296.3472903(731-747)Online publication date: 9-Aug-2021
https://dl.acm.org/doi/10.1145/3452296.3472903
Kang QXing JQiu YChen ASherwood TBerger EKozyrakis C(2021)Probabilistic profiling of stateful data planes for adversarial testingProceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3445814.3446764(286-301)Online publication date: 19-Apr-2021
https://dl.acm.org/doi/10.1145/3445814.3446764
Holtzen SJunges SVazquez-Chanlatte MMillstein TSeshia SVan den Broeck G(2021)Model Checking Finite-Horizon Markov Chains with Probabilistic InferenceComputer Aided Verification10.1007/978-3-030-81688-9_27(577-601)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1007/978-3-030-81688-9_27
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents