{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/18419"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/18419","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Diagnose network failures via data-plane analysis","abstract":"Diagnosing problems in networks is a time-consuming and error-prone process. Previous tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems, checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large campus network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.","abstract_html":"Diagnosing problems in networks is a time-consuming and error-prone process. Previous tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems, checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large campus network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.","abstract_has_math":false,"creators":["Mai, Haohui"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["King, Samuel T."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-01-14T22:50:14Z","date_published":"2011-01-14T22:50:14Z","updated_at":"2026-07-22T22:25:11Z","subjects":["Data-Plane Analysis","Network Failure","Satisfiability"],"languages":["en"],"rights":["Copyright 2010 Haohui Mai"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/18419","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["King, Samuel T."]},{"key":"dc:creator","label":"Author","values":["Mai, Haohui"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-01-14T22:50:14Z","2010-12"]},{"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":["Data-Plane Analysis","Network Failure","Satisfiability"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2010 Haohui Mai"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/18419"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Diagnosing problems in networks is a time-consuming and error-prone process. Previous tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems, checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large campus network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-11-17T21:31:51Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 master-thesis.tar.bz2: 744324 bytes, checksum: 41d0f5ddbbb9bcb14f91ee7cb50056a7 (MD5) Mai_Haohui.pdf: 500779 bytes, checksum: 06c64236b9732b07e830da8774bf1aa7 (MD5)","Made available in DSpace on 2011-01-14T22:50:14Z (GMT). No. of bitstreams: 3 Mai_Haohui.pdf: 500779 bytes, checksum: 06c64236b9732b07e830da8774bf1aa7 (MD5) license.txt: 4056 bytes, checksum: ccb6ce23a058623eac584b4fa7224fec (MD5) master-thesis.tar.bz2: 744324 bytes, checksum: 41d0f5ddbbb9bcb14f91ee7cb50056a7 (MD5)"]},{"key":"dc:title","label":"Title","values":["Diagnose network failures via data-plane analysis"]}]}],"canonical_facts":{"dc:contributor":["King, Samuel T."],"dc:creator":["Mai, Haohui"],"dc:date":["2011-01-14T22:50:14Z","2010-12"],"dc:description":["Diagnosing problems in networks is a time-consuming and error-prone process. Previous tools to assist operators primarily focus on analyzing control plane configuration. Configuration analysis is limited in that it cannot find bugs in router software, and is harder to generalize across protocols since it must model complex configuration languages and dynamic protocol behavior. This paper studies an alternate approach: diagnosing problems through static analysis of the data plane. This approach can catch bugs that are invisible at the level of configuration files, and simplifies unified analysis of a network across many protocols and implementations. We present Anteater, a tool for checking invariants in the data plane. Anteater translates high-level network invariants into boolean satisfiability problems, checks them against network state using a SAT solver, and reports counterexamples if violations have been found. Applied to a large campus network, Anteater revealed 23 bugs, including forwarding loops and stale ACL rules, with only five false positives. Nine of these faults are being fixed by campus network operators.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-11-17T21:31:51Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 master-thesis.tar.bz2: 744324 bytes, checksum: 41d0f5ddbbb9bcb14f91ee7cb50056a7 (MD5) Mai_Haohui.pdf: 500779 bytes, checksum: 06c64236b9732b07e830da8774bf1aa7 (MD5)","Made available in DSpace on 2011-01-14T22:50:14Z (GMT). No. of bitstreams: 3 Mai_Haohui.pdf: 500779 bytes, checksum: 06c64236b9732b07e830da8774bf1aa7 (MD5) license.txt: 4056 bytes, checksum: ccb6ce23a058623eac584b4fa7224fec (MD5) master-thesis.tar.bz2: 744324 bytes, checksum: 41d0f5ddbbb9bcb14f91ee7cb50056a7 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/18419"],"dc:language":["en"],"dc:rights":["Copyright 2010 Haohui Mai"],"dc:subject":["Data-Plane Analysis","Network Failure","Satisfiability"],"dc:title":["Diagnose network failures via data-plane analysis"],"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:25:11Z"}