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

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

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.