FMitF: Track I: Privacy-Preserving Policy Verification of Interdomain Routing

现在几乎所有实体之间的数字通信都是通过互联网进行的。通过互联网进行的通信包括促进科学进步的合作、商业交易和促进人类福祉的医疗信息传递。拥有一个安全和可预测的互联网是非常重要的。与其重要性相悖的是，互联网去中心化的本质使其难以分析。没有一个单一的实体拥有关于互联网的完美信息，也缺乏在信息不完全的情况下对互联网进行推理的正式模型。因此，由于意外或恶意，Internet中很小的局部策略更改可能会产生流量被不适当路由的巨大净影响。该项目寻求开发工具和技术来解决这一限制，并将利用外联向管理互联网政策的学术界和标准化机构宣传这些方法。互联网连接了由互联网服务提供商、公司和大学运营的数千个自治系统（as）。as之间通过BGP （Border Gateway Protocol）协议互通，路由流量并交换可达性信息。BGP允许每个自治系统使用自己的本地策略进行路由决策，而不需要透露它使用的是哪种策略。各种未知策略的使用使得分析网络是否容易受到流量劫持的影响，或者一个AS中的策略更改是否会导致网络中意外的紧急行为变得极其困难。这个项目将寻求开发一个正式的框架来推理路由策略及其影响。网络运营商可以在这个框架中提出查询，以找出路由策略设置是否会导致漏洞或其他不良行为。来自网络运营商的查询将被表示为SMT公式，并带有额外的特定于领域的抽象和不变量，以帮助支持可伸缩性。重要的是，由于认识到BGP中的路由策略是私有的，因此正式框架将是隐私保护的，因此每个自治系统都可以在不泄露其策略的情况下参与。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.