{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/105115"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/105115","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Network analysis, inference and verification","abstract":"Securely operating large-scale networks is a non-trivial task involving interactions between various hardware devices, protocols, and configurations, all of which need to work in tandem for the network to be secure and in the desired state that the network administrators want it to be in. Misconfigurations or malicious activities in the network can disrupt it resulting in dire effects including but not limited to outages of critical applications and breach of sensitive information. In this work, we propose a robust framework for diagnosing such anomalies across enterprise networks, and study their impact in terms of changes in routing behavior and reachability. To study the network as closely as possible to its actual behavior we perform analysis on data plane features as they govern the journey of a packet during its life-cycle across the network. We perform temporal analysis of the network as a whole and inspect the evolution of various properties. We then determine the deviation of the network relative to its previous states and identify as accurately as possible if the current state is anomalous. Given the historic states of the network over some time, we also try to infer high-level policies and invariants in the network. These allow for running various verification techniques on the network. Finally, we propose a network verification tool designed to verify the network as a dynamic, multi-layer distributed system. The richness of this tool’s network model allows it to find network issues that are not detectable using state of the art tools which work solely on either data plane states or control plane states without examining the interaction of the two among themselves and temporally with the network environment. Building on this verification tool, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks; our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests that the technique can scale to larger networks with reasonable performance. Thus, our framework provides an end to end solution for network analysis, inference and verification.","abstract_html":"Securely operating large-scale networks is a non-trivial task involving interactions between various hardware devices, protocols, and configurations, all of which need to work in tandem for the network to be secure and in the desired state that the network administrators want it to be in. Misconfigurations or malicious activities in the network can disrupt it resulting in dire effects including but not limited to outages of critical applications and breach of sensitive information. In this work, we propose a robust framework for diagnosing such anomalies across enterprise networks, and study their impact in terms of changes in routing behavior and reachability. To study the network as closely as possible to its actual behavior we perform analysis on data plane features as they govern the journey of a packet during its life-cycle across the network. We perform temporal analysis of the network as a whole and inspect the evolution of various properties. We then determine the deviation of the network relative to its previous states and identify as accurately as possible if the current state is anomalous. Given the historic states of the network over some time, we also try to infer high-level policies and invariants in the network. These allow for running various verification techniques on the network. Finally, we propose a network verification tool designed to verify the network as a dynamic, multi-layer distributed system. The richness of this tool’s network model allows it to find network issues that are not detectable using state of the art tools which work solely on either data plane states or control plane states without examining the interaction of the two among themselves and temporally with the network environment. Building on this verification tool, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks; our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests that the technique can scale to larger networks with reasonable performance. Thus, our framework provides an end to end solution for network analysis, inference and verification.","abstract_has_math":false,"creators":["Chaudhry, Gohar Irfan"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Caesar, Matthew"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019-08-23T20:44:18Z","date_published":"2019-08-23T20:44:18Z","updated_at":"2026-07-22T22:24:44Z","subjects":["anomaly","detection","veriflow","testing","networks","analysis","inference","verification","plankton","anomaly detection"],"languages":["en"],"rights":["Copyright 2018 Gohar Irfan Chaudhry"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/105115","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Caesar, Matthew"]},{"key":"dc:creator","label":"Author","values":["Chaudhry, Gohar Irfan"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2019-08-23T20:44:18Z","2021-08-24T09:15:31Z","2018-04-24","2018-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"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":["anomaly","detection","veriflow","testing","networks","analysis","inference","verification","plankton","anomaly detection"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Gohar Irfan Chaudhry"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/105115"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Securely operating large-scale networks is a non-trivial task involving interactions between various hardware devices, protocols, and configurations, all of which need to work in tandem for the network to be secure and in the desired state that the network administrators want it to be in. Misconfigurations or malicious activities in the network can disrupt it resulting in dire effects including but not limited to outages of critical applications and breach of sensitive information. In this work, we propose a robust framework for diagnosing such anomalies across enterprise networks, and study their impact in terms of changes in routing behavior and reachability. To study the network as closely as possible to its actual behavior we perform analysis on data plane features as they govern the journey of a packet during its life-cycle across the network. We perform temporal analysis of the network as a whole and inspect the evolution of various properties. We then determine the deviation of the network relative to its previous states and identify as accurately as possible if the current state is anomalous. Given the historic states of the network over some time, we also try to infer high-level policies and invariants in the network. These allow for running various verification techniques on the network. Finally, we propose a network verification tool designed to verify the network as a dynamic, multi-layer distributed system. The richness of this tool’s network model allows it to find network issues that are not detectable using state of the art tools which work solely on either data plane states or control plane states without examining the interaction of the two among themselves and temporally with the network environment. Building on this verification tool, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks; our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests that the technique can scale to larger networks with reasonable performance. Thus, our framework provides an end to end solution for network analysis, inference and verification.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2020-05-01","The student, Gohar Irfan Chaudhry, accepted the attached license on 2018-04-23 at 21:13.","The student, Gohar Irfan Chaudhry, submitted this Thesis for approval on 2018-04-23 at 21:16.","This Thesis was approved for publication on 2018-04-24 at 12:28.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12437 on 2019-08-22 at 16:17:51","Made available in DSpace on 2019-08-23T20:44:18Z (GMT). No. of bitstreams: 2 CHAUDHRY-THESIS-2018.pdf: 9733981 bytes, checksum: e9bc81e075768c62a2abbc0c90d1c2eb (MD5) LICENSE.txt: 4217 bytes, checksum: 34322a2fe53f873f2039adb2ecba21d6 (MD5) Previous issue date: 2018-04-24","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:44:50Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:46:41Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:47:38Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:48:32Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited Restriction Lifted for Item 112234 on 2021-08-24T09:15:31Z."]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Network analysis, inference and verification"]}]}],"canonical_facts":{"dc:contributor":["Caesar, Matthew"],"dc:creator":["Chaudhry, Gohar Irfan"],"dc:date":["2019-08-23T20:44:18Z","2021-08-24T09:15:31Z","2018-04-24","2018-05"],"dc:description":["Securely operating large-scale networks is a non-trivial task involving interactions between various hardware devices, protocols, and configurations, all of which need to work in tandem for the network to be secure and in the desired state that the network administrators want it to be in. Misconfigurations or malicious activities in the network can disrupt it resulting in dire effects including but not limited to outages of critical applications and breach of sensitive information. In this work, we propose a robust framework for diagnosing such anomalies across enterprise networks, and study their impact in terms of changes in routing behavior and reachability. To study the network as closely as possible to its actual behavior we perform analysis on data plane features as they govern the journey of a packet during its life-cycle across the network. We perform temporal analysis of the network as a whole and inspect the evolution of various properties. We then determine the deviation of the network relative to its previous states and identify as accurately as possible if the current state is anomalous. Given the historic states of the network over some time, we also try to infer high-level policies and invariants in the network. These allow for running various verification techniques on the network. Finally, we propose a network verification tool designed to verify the network as a dynamic, multi-layer distributed system. The richness of this tool’s network model allows it to find network issues that are not detectable using state of the art tools which work solely on either data plane states or control plane states without examining the interaction of the two among themselves and temporally with the network environment. Building on this verification tool, we propose a technique for high-coverage testing of end-to-end network correctness using the real software that is deployed in these networks; our design is effectively a hybrid, using an explicit-state model checker to explore all network-wide execution paths and event orderings, but executing real software as subroutines for each device. We show that this approach can detect correctness issues that would be missed both by existing verification and testing approaches, and a prototype implementation suggests that the technique can scale to larger networks with reasonable performance. Thus, our framework provides an end to end solution for network analysis, inference and verification.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2020-05-01","The student, Gohar Irfan Chaudhry, accepted the attached license on 2018-04-23 at 21:13.","The student, Gohar Irfan Chaudhry, submitted this Thesis for approval on 2018-04-23 at 21:16.","This Thesis was approved for publication on 2018-04-24 at 12:28.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12437 on 2019-08-22 at 16:17:51","Made available in DSpace on 2019-08-23T20:44:18Z (GMT). No. of bitstreams: 2 CHAUDHRY-THESIS-2018.pdf: 9733981 bytes, checksum: e9bc81e075768c62a2abbc0c90d1c2eb (MD5) LICENSE.txt: 4217 bytes, checksum: 34322a2fe53f873f2039adb2ecba21d6 (MD5) Previous issue date: 2018-04-24","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:44:50Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:46:41Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:47:38Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 112234 Lift date: 2021-08-23T20:48:32Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited Restriction Lifted for Item 112234 on 2021-08-24T09:15:31Z."],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/105115"],"dc:language":["en"],"dc:rights":["Copyright 2018 Gohar Irfan Chaudhry"],"dc:subject":["anomaly","detection","veriflow","testing","networks","analysis","inference","verification","plankton","anomaly detection"],"dc:title":["Network analysis, inference and verification"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:44Z"}