{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/113886"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/113886","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Foundations for practical network verification","abstract":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","abstract_html":"Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","abstract_has_math":false,"creators":["Kheradmand, Ali"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Godfrey, Brighten","Rosu, Grigore","Xu, Tianyin","Padhye, Jitendra"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-04-29T21:34:40Z","date_published":"2022-04-29T21:34:40Z","updated_at":"2026-07-22T22:24:53Z","subjects":["Computer science"],"languages":["en","eng"],"rights":["Copyright 2021 Ali Kheradmand"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/113886","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Godfrey, Brighten","Rosu, Grigore","Xu, Tianyin","Padhye, Jitendra"]},{"key":"dc:creator","label":"Author","values":["Kheradmand, Ali"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2022-04-29T21:34:40Z","2021-12","2021-12-02"]},{"key":"dc:type","label":"Dc Type","values":["text","Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en","eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2021 Ali Kheradmand"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/113886"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","The student, Ali Kheradmand, accepted the attached license on 2021-11-30 at 21:44.","The student, Ali Kheradmand, submitted this Dissertation for approval on 2021-11-30 at 22:18.","This Dissertation was approved for publication on 2021-12-02 at 17:16.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17320 on 2022-04-06 at 17:10:27","Made available in DSpace on 2022-04-29T21:34:40Z (GMT). No. of bitstreams: 4 KHERADMAND-DISSERTATION-2021.pdf: 1771008 bytes, checksum: c67057d400468b73c2e7c33bf2b32652 (MD5) Ali-Kheradmand-PhD-thesis (1).zip: 3306451 bytes, checksum: 1ef5156ac2ee6930ba3f2fc3901a5119 (MD5) LICENSE.txt: 4211 bytes, checksum: 12d755c1ebb88e46820caa9a7082d468 (MD5) PROQUEST_LICENSE.txt: 4557 bytes, checksum: 557a92b4cf0fc0b81a7ad20e43d64fc7 (MD5) Previous issue date: 2021-12-02","Computer networks are large and complex and the often manual process of configuring such systems is error-prone, leading to network outages and breaches. This has ignited research into network verification tools that given a set of operator intents, automatically check whether the configured network satisfies the intents. In this dissertation, we argue that existing works in this area have important limitations that prevent their widespread adoption in the real world. We set to address these limitations by revisiting the main aspects of network verification: verification framework, intent specification, and network modeling. First, we develop #PEC, a symbolic packet header analysis framework that resolves the tension between expressiveness and efficiency in previous works. We provide an extensible library of efficient match-types that allows encoding and analyzing more types of forwarding rules (e.g. Linux iptables) compared to most previous works. Similar to the state-of-the-art, #PEC partitions the space of packet headers into a set of equivalence classes (PECs) before the analysis. However, it uses a lattice-based approach to do so, refraining from using computationally expensive negation and subtraction operations. Our experiments with a broad range of real-world datasets show that #PEC is 10× faster than similarly expressive state-of-the-art. We also demonstrate how empty PECs in previous works lead to unsound/incomplete analysis and develop a counting-based method to eliminate empty PECs from #PEC that outperforms baseline approaches by 10 − 100×. Next, we note that network verification requires formal specifications of the intents of the network operator as a starting point, which are almost never available or even known in a complete form. We mitigate this problem by providing a framework to utilize existing low-level network behavior to infer the high-level intents. We design Anime, a system that given observed packet forwarding behavior, mines a compact set of possible intents that best describe the observations. Anime accomplishes this by applying optimized clustering algorithms to a set of observed network paths, encoded using path features with hierarchical values that yield a way to control the precision-recall tradeoff. The resulting inferred intents can be used as input to verification/synthesis tools for continued maintenance. They can also be viewed as a summary of network behavior, and as a way to find anomalous behavior. Our experiments, including data from an operational network, demonstrate that Anime produces higher quality (F-score) intents than past work, can generate compact summaries with minimal loss of precision, is resilient to imperfect input and policy changes, scales to large networks, and finds actionable anomalies in an operational network. Finally, we turn our attention to modeling networking devices. We envision basing data plane analysis on P4 as the modeling language. Unlike most tools, we believe P4 analysis must be based on a precise model of the language rather than its informal specification. To this end, we develop a formal operational semantics of the P4 language during the process of which we have identified numerous issues with the design of the language. We then provide a suite of formal analysis tools derived directly from our semantics including an interpreter, a symbolic model checker, a deductive program verifier, and a program equivalence checker. Through a set of case studies, we demonstrate the use of our semantics beyond just a reference model for the language. This includes applications for the detection of unportable code, state-space exploration, search for bugs, full functional verification, and compiler translation validation."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Foundations for practical network verification"]}]}],"canonical_facts":{"dc:contributor":["Godfrey, Brighten","Rosu, Grigore","Xu, Tianyin","Padhye, Jitendra"],"dc:creator":["Kheradmand, Ali"],"dc:date":["2022-04-29T21:34:40Z","2021-12","2021-12-02"],"dc:description":["Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2022-04-06 without embargo terms","The student, Ali Kheradmand, accepted the attached license on 2021-11-30 at 21:44.","The student, Ali Kheradmand, submitted this Dissertation for approval on 2021-11-30 at 22:18.","This Dissertation was approved for publication on 2021-12-02 at 17:16.","DSpace SAF Submission Ingestion Package generated from Vireo submission #17320 on 2022-04-06 at 17:10:27","Made available in DSpace on 2022-04-29T21:34:40Z (GMT). No. of bitstreams: 4 KHERADMAND-DISSERTATION-2021.pdf: 1771008 bytes, checksum: c67057d400468b73c2e7c33bf2b32652 (MD5) Ali-Kheradmand-PhD-thesis (1).zip: 3306451 bytes, checksum: 1ef5156ac2ee6930ba3f2fc3901a5119 (MD5) LICENSE.txt: 4211 bytes, checksum: 12d755c1ebb88e46820caa9a7082d468 (MD5) PROQUEST_LICENSE.txt: 4557 bytes, checksum: 557a92b4cf0fc0b81a7ad20e43d64fc7 (MD5) Previous issue date: 2021-12-02","Computer networks are large and complex and the often manual process of configuring such systems is error-prone, leading to network outages and breaches. This has ignited research into network verification tools that given a set of operator intents, automatically check whether the configured network satisfies the intents. In this dissertation, we argue that existing works in this area have important limitations that prevent their widespread adoption in the real world. We set to address these limitations by revisiting the main aspects of network verification: verification framework, intent specification, and network modeling. First, we develop #PEC, a symbolic packet header analysis framework that resolves the tension between expressiveness and efficiency in previous works. We provide an extensible library of efficient match-types that allows encoding and analyzing more types of forwarding rules (e.g. Linux iptables) compared to most previous works. Similar to the state-of-the-art, #PEC partitions the space of packet headers into a set of equivalence classes (PECs) before the analysis. However, it uses a lattice-based approach to do so, refraining from using computationally expensive negation and subtraction operations. Our experiments with a broad range of real-world datasets show that #PEC is 10× faster than similarly expressive state-of-the-art. We also demonstrate how empty PECs in previous works lead to unsound/incomplete analysis and develop a counting-based method to eliminate empty PECs from #PEC that outperforms baseline approaches by 10 − 100×. Next, we note that network verification requires formal specifications of the intents of the network operator as a starting point, which are almost never available or even known in a complete form. We mitigate this problem by providing a framework to utilize existing low-level network behavior to infer the high-level intents. We design Anime, a system that given observed packet forwarding behavior, mines a compact set of possible intents that best describe the observations. Anime accomplishes this by applying optimized clustering algorithms to a set of observed network paths, encoded using path features with hierarchical values that yield a way to control the precision-recall tradeoff. The resulting inferred intents can be used as input to verification/synthesis tools for continued maintenance. They can also be viewed as a summary of network behavior, and as a way to find anomalous behavior. Our experiments, including data from an operational network, demonstrate that Anime produces higher quality (F-score) intents than past work, can generate compact summaries with minimal loss of precision, is resilient to imperfect input and policy changes, scales to large networks, and finds actionable anomalies in an operational network. Finally, we turn our attention to modeling networking devices. We envision basing data plane analysis on P4 as the modeling language. Unlike most tools, we believe P4 analysis must be based on a precise model of the language rather than its informal specification. To this end, we develop a formal operational semantics of the P4 language during the process of which we have identified numerous issues with the design of the language. We then provide a suite of formal analysis tools derived directly from our semantics including an interpreter, a symbolic model checker, a deductive program verifier, and a program equivalence checker. Through a set of case studies, we demonstrate the use of our semantics beyond just a reference model for the language. This includes applications for the detection of unportable code, state-space exploration, search for bugs, full functional verification, and compiler translation validation."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/113886"],"dc:language":["en","eng"],"dc:rights":["Copyright 2021 Ali Kheradmand"],"dc:subject":["Computer science"],"dc:title":["Foundations for practical network verification"],"dc:type":["text","Thesis"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:53Z"}