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 their policy.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
