Privacy-Preserving Policy Verification of Interdomain Routing



National Science Foundation

About the Project

Nearly all digital communication between entities is now carried by the Internet. Communications through the Internet include collaborations that enable scientific progress, transaction of business, and transfer of medical information that promotes human welfare. Having a secure and predictable Internet is of great importance. In tension with its importance, the decentralized nature of the Internet makes it hard to analyze. No single entity has perfect information about the internet, and there is lack of formal models for reasoning about the Internet with incomplete information. As a result, through accident or malice, it is possible for small localized policy changes in the Internet to have large net effects of traffic being inappropriately routed. This project seeks to develop tools and techniques to address this limitation, and will use outreach to publicize these approaches to the academic community and standardization bodies that govern Internet policy.

The Internet connects thousands of Autonomous Systems (ASs) operated by Internet Service Providers, companies, and universities. The ASs interconnect to each other to route traffic and exchange reachability information using the Border Gateway Protocol (BGP). BGP allows each AS to use its own local policy for making routing decisions, without revealing what policy it is using. The use of diverse and unknown policies makes it extremely difficult to analyze whether a network may be susceptible to traffic hijacking, or whether a policy change in one AS might lead to unintended emergent behaviors in a network. This project will seek to develop a formal framework for reasoning about routing policies and their impact. Network operators can pose queries in this framework to find out whether routing-policy settings may lead to vulnerabilities or other undesirable behaviors. The queries from network operators will be posed as SMT formulas, with additional domain-specific abstractions and invariants to help support scalability. Critically, in recognition that routing policies are private within BGP, the formal framework will be privacy-preserving, so that each AS can participate without revealing its policy.



Prof. Lixin Gao (PI)

Prof. Daniel Holcomb (co-PI)

Research Assistants 

Xiaozhe Shao

Zibin Chen

Bharadwaj Madabhushi

Mohammad Waquas Usmani


  • Zibin Chen and Lixin Gao, "CURSOR: Configuration Update Synthesis Using Order Rules", (slides) IEEE INFOCOM 2023 - IEEE Conference on Computer Communications, New York City, NY, USA, 2023, pp. 1-10, doi: 10.1109/INFOCOM53939.2023.10228930.
  • Xiaozhe Shao, Zibin Chen, Daniel Holcomb, and Lixin Gao, "Accelerating BGP Configuration Verification Through Reducing Cycles in SMT Constraints", in IEEE/ACM Transactions on Networking, vol. 30, no. 6, pp. 2493-2504, Dec. 2022, doi: 10.1109/TNET.2022.3176267.
  • Xiaozhe Shao and Lixin Gao, "Policy-rich Interdomain Routing with Local Coordination", Computer Networks, Volume 197, 2021, 108292, ISSN 1389-1286, doi: 10.1016/j.comnet.2021.108292.
  • Xiaozhe Shao and Lixin Gao, "Verifying Policy-based Routing at Internet Scale", (technical report, slides) IEEE INFOCOM 2020 - IEEE Conference on Computer Communications, Toronto, ON, Canada, 2020, pp. 2293-2302, doi: 10.1109/INFOCOM41043.2020.9155235.
  • Nazanin Takbiri, Xiaozhe Shao, Lixin Gao, and Hossein Pishro-Nik, "Improving Privacy in Graphs Through Node Addition", in Proceeding of Annual Allerton Conference on Communication, Control, and Computing (Allerton), 2019.
  • Links to Code Repositories

  • Incremental Network Verification,
  • Network Verification with BiNode,
  • BiNode,
  • Outreach Activities

    Co-PI Holcomb served as program chair of the 3rd annual New England Hardware Security Day, held at Northeastern University on April 7, 2023. The event drew over 120 attendees from academia, defense, and industry. Students attended free of charge, thanks to sponsorship from NSF and industrial partners. The event featured talks, panels, a poster contest, and lively discussion.


    This material is based upon work supported by the National Science Foundation under Grant CCF-1918187. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.