{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/108300"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/108300","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Practical verification of network planes","abstract":"Formal network verification is a rapidly advancing field of research, encompassing a wide array of verticals such as data plane verification, configuration verification, network software verification etc. More and more real-world networks are deploying network verification as a tool to prevent outages and vulnerabilities. However, the fundamental challenges of scope and scalability make network verification unusable in a significant fraction of real-world networks. In this thesis, we discuss a new generation of verification techniques, algorithms and data structures designed to make network verification more universally applicable. We first present Plankton, a configuration verification platform that combines efficient explicit state model checking with domain-specific optimizations to enhance the scalability of configuration verification. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art. Then, we discuss how the model checking-based technique can be used to verify network dataplanes with software components. We propose Plankton-neo, a tool for checking such dataplanes without the need for faithful middlebox models. 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 a subroutine for each device. Plankton-neo incorporates predefined models of specific protocols such as TCP and ICMP, along with a rich collection of policies that can be checked over dataplanes incorporating NFV components. We show that Plankton-neo can detect correctness issues that would be missed both by existing verification and testing approaches, and describe an implementation that can scale to large networks with good performance. Finally, we identify the fundamental challenges for scalable dataplane verification in the real world and propose ways to solve them better than the state of the art. We describe a new data structure for representing symbolic sets of packets for dataplane verification. Our design is inspired by Binary Decision Diagrams, but is able to overcome some specific limitations of BDDs in the context of storing packet sets. We describe a set of benchmark traces for evaluating packet set data structures, and perform an experimental comparison of our proposed data structure with BDDs. The experiments show that we are able to improve the time and memory overhead by significant amounts compared to BDDs.","abstract_html":"Formal network verification is a rapidly advancing field of research, encompassing a wide array of verticals such as data plane verification, configuration verification, network software verification etc. More and more real-world networks are deploying network verification as a tool to prevent outages and vulnerabilities. However, the fundamental challenges of scope and scalability make network verification unusable in a significant fraction of real-world networks. In this thesis, we discuss a new generation of verification techniques, algorithms and data structures designed to make network verification more universally applicable. We first present Plankton, a configuration verification platform that combines efficient explicit state model checking with domain-specific optimizations to enhance the scalability of configuration verification. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art. Then, we discuss how the model checking-based technique can be used to verify network dataplanes with software components. We propose Plankton-neo, a tool for checking such dataplanes without the need for faithful middlebox models. 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 a subroutine for each device. Plankton-neo incorporates predefined models of specific protocols such as TCP and ICMP, along with a rich collection of policies that can be checked over dataplanes incorporating NFV components. We show that Plankton-neo can detect correctness issues that would be missed both by existing verification and testing approaches, and describe an implementation that can scale to large networks with good performance. Finally, we identify the fundamental challenges for scalable dataplane verification in the real world and propose ways to solve them better than the state of the art. We describe a new data structure for representing symbolic sets of packets for dataplane verification. Our design is inspired by Binary Decision Diagrams, but is able to overcome some specific limitations of BDDs in the context of storing packet sets. We describe a set of benchmark traces for evaluating packet set data structures, and perform an experimental comparison of our proposed data structure with BDDs. The experiments show that we are able to improve the time and memory overhead by significant amounts compared to BDDs.","abstract_has_math":false,"creators":["Prabhu Muraleedhara Prabhu, Santhosh"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Caesar, Matthew C","Godfrey, Philip B","Xu, Tianyin","Mishchenko, Alan","Panda, Aurojit"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2020,"date_issued":"2020-08-27T00:50:16Z","date_published":"2020-08-27T00:50:16Z","updated_at":"2026-07-22T22:24:48Z","subjects":["Computer Networks, Formal Verification"],"languages":["en"],"rights":["Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/108300","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Caesar, Matthew C","Godfrey, Philip B","Xu, Tianyin","Mishchenko, Alan","Panda, Aurojit"]},{"key":"dc:creator","label":"Author","values":["Prabhu Muraleedhara Prabhu, Santhosh"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2020-08-27T00:50:16Z","2022-08-27T00:51:40Z","2020-05-05","2020-05"]},{"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 Networks, Formal Verification"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/108300"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Formal network verification is a rapidly advancing field of research, encompassing a wide array of verticals such as data plane verification, configuration verification, network software verification etc. More and more real-world networks are deploying network verification as a tool to prevent outages and vulnerabilities. However, the fundamental challenges of scope and scalability make network verification unusable in a significant fraction of real-world networks. In this thesis, we discuss a new generation of verification techniques, algorithms and data structures designed to make network verification more universally applicable. We first present Plankton, a configuration verification platform that combines efficient explicit state model checking with domain-specific optimizations to enhance the scalability of configuration verification. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art. Then, we discuss how the model checking-based technique can be used to verify network dataplanes with software components. We propose Plankton-neo, a tool for checking such dataplanes without the need for faithful middlebox models. 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 a subroutine for each device. Plankton-neo incorporates predefined models of specific protocols such as TCP and ICMP, along with a rich collection of policies that can be checked over dataplanes incorporating NFV components. We show that Plankton-neo can detect correctness issues that would be missed both by existing verification and testing approaches, and describe an implementation that can scale to large networks with good performance. Finally, we identify the fundamental challenges for scalable dataplane verification in the real world and propose ways to solve them better than the state of the art. We describe a new data structure for representing symbolic sets of packets for dataplane verification. Our design is inspired by Binary Decision Diagrams, but is able to overcome some specific limitations of BDDs in the context of storing packet sets. We describe a set of benchmark traces for evaluating packet set data structures, and perform an experimental comparison of our proposed data structure with BDDs. The experiments show that we are able to improve the time and memory overhead by significant amounts compared to BDDs.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2022-05-01","The student, Santhosh Prabhu Muraleedhara Prabhu, accepted the attached license on 2020-05-04 at 10:20.","The student, Santhosh Prabhu Muraleedhara Prabhu, submitted this Dissertation for approval on 2020-05-04 at 10:34.","This Dissertation was approved for publication on 2020-05-05 at 10:50.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15155 on 2020-08-25 at 17:42:30","Made available in DSpace on 2020-08-27T00:50:16Z (GMT). No. of bitstreams: 3 PRABHUMURALEEDHARAPRABHU-DISSERTATION-2020.pdf: 4825543 bytes, checksum: 57c122b65156dca617505fe0b56e215e (MD5) LICENSE.txt: 4232 bytes, checksum: ab55e6450f76ea0cd62aee12419b702e (MD5) PROQUEST_LICENSE.txt: 4578 bytes, checksum: 828cbb8872f2670c0604a5fc126e23e1 (MD5) Previous issue date: 2020-05-05","Embargo set by: Seth Robbins for item 115914 Lift date: 2022-08-27T00:50:22Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 115914 Lift date: 2022-08-27T00:51:40Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Practical verification of network planes"]}]}],"canonical_facts":{"dc:contributor":["Caesar, Matthew C","Godfrey, Philip B","Xu, Tianyin","Mishchenko, Alan","Panda, Aurojit"],"dc:creator":["Prabhu Muraleedhara Prabhu, Santhosh"],"dc:date":["2020-08-27T00:50:16Z","2022-08-27T00:51:40Z","2020-05-05","2020-05"],"dc:description":["Formal network verification is a rapidly advancing field of research, encompassing a wide array of verticals such as data plane verification, configuration verification, network software verification etc. More and more real-world networks are deploying network verification as a tool to prevent outages and vulnerabilities. However, the fundamental challenges of scope and scalability make network verification unusable in a significant fraction of real-world networks. In this thesis, we discuss a new generation of verification techniques, algorithms and data structures designed to make network verification more universally applicable. We first present Plankton, a configuration verification platform that combines efficient explicit state model checking with domain-specific optimizations to enhance the scalability of configuration verification. Thanks to a highly effective suite of optimizations including state hashing, partial order reduction, and policy-based pruning, Plankton successfully verifies policies in industrial-scale networks quickly and compactly, at times reaching a 10000× speedup compared to the state of the art. Then, we discuss how the model checking-based technique can be used to verify network dataplanes with software components. We propose Plankton-neo, a tool for checking such dataplanes without the need for faithful middlebox models. 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 a subroutine for each device. Plankton-neo incorporates predefined models of specific protocols such as TCP and ICMP, along with a rich collection of policies that can be checked over dataplanes incorporating NFV components. We show that Plankton-neo can detect correctness issues that would be missed both by existing verification and testing approaches, and describe an implementation that can scale to large networks with good performance. Finally, we identify the fundamental challenges for scalable dataplane verification in the real world and propose ways to solve them better than the state of the art. We describe a new data structure for representing symbolic sets of packets for dataplane verification. Our design is inspired by Binary Decision Diagrams, but is able to overcome some specific limitations of BDDs in the context of storing packet sets. We describe a set of benchmark traces for evaluating packet set data structures, and perform an experimental comparison of our proposed data structure with BDDs. The experiments show that we are able to improve the time and memory overhead by significant amounts compared to BDDs.","Submission published under a 24 month embargo labeled 'Closed Access', the embargo will last until 2022-05-01","The student, Santhosh Prabhu Muraleedhara Prabhu, accepted the attached license on 2020-05-04 at 10:20.","The student, Santhosh Prabhu Muraleedhara Prabhu, submitted this Dissertation for approval on 2020-05-04 at 10:34.","This Dissertation was approved for publication on 2020-05-05 at 10:50.","DSpace SAF Submission Ingestion Package generated from Vireo submission #15155 on 2020-08-25 at 17:42:30","Made available in DSpace on 2020-08-27T00:50:16Z (GMT). No. of bitstreams: 3 PRABHUMURALEEDHARAPRABHU-DISSERTATION-2020.pdf: 4825543 bytes, checksum: 57c122b65156dca617505fe0b56e215e (MD5) LICENSE.txt: 4232 bytes, checksum: ab55e6450f76ea0cd62aee12419b702e (MD5) PROQUEST_LICENSE.txt: 4578 bytes, checksum: 828cbb8872f2670c0604a5fc126e23e1 (MD5) Previous issue date: 2020-05-05","Embargo set by: Seth Robbins for item 115914 Lift date: 2022-08-27T00:50:22Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Embargo set by: Seth Robbins for item 115914 Lift date: 2022-08-27T00:51:40Z Reason: Author requested closed access (OA after 2yrs) in Vireo ETD system","Author requested closed access (OA after 2yrs) in Vireo ETD system","Limited"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/108300"],"dc:language":["en"],"dc:rights":["Copyright 2020 Santhosh Prabhu Muraleedhara Prabhu"],"dc:subject":["Computer Networks, Formal Verification"],"dc:title":["Practical verification of network planes"],"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:48Z"}