TC: Small: Collaborative Research: Towards a Formal Framework for Analyzing and Implementing Secure Routing Protocols

今天好吗?Internet运行边界网关协议BGP (Border Gateway Protocol)，这是一种复杂的域间路由协议。在过去的几年里，人们对BGP路由的复杂性和脆弱性达成了越来越多的共识。除了存在路由振荡和收敛速度慢的问题外，BGP还容易受到恶意攻击。尽管针对BGP的安全漏洞提出了各种各样的解决方案，但目前还缺乏一套通用的工具来供研究人员分析、比较和对比各种方案的有效性。该项目的目标是开发一个统一的框架，用于设计、分析和实现可证明安全的互联网路由协议。该项目的第一部分探讨了安全网络数据表（SeNDlog）的使用，这是一种用于编码安全互联网路由协议的声明性网络语言。将探索SeNDLog的语言扩展，以解决互联网规模的实际部署问题，并促进对一系列安全路由协议的正式分析。这些扩展包括可定制的身份验证、面向目标的评估、密钥分发和管理，以及对手的建模。该项目的第二部分旨在识别互联网路由协议的安全属性，并根据协议执行轨迹在逻辑上正式指定它们。该项目的第三部分旨在设计和实现一种形式化分析方法，用于验证SeNDlog程序是否符合逻辑中指定的所需安全属性。就更广泛的影响而言，该项目将为可信路由协议的分析和开发提供更清晰的基础。

Today?s Internet runs Border Gateway Protocol (BGP), a complex inter-domain routing protocol. Over the past few years, there has been a growing consensus on the complexity and fragility of BGP routing. In addition to the problems of route oscillation and slow convergence, BGP has been shown to be susceptible to malicious attacks. Despite the wide range of proposed solutions to BGP's security vulnerabilities, there is currently a lack of a set of common tools for researchers to analyze, compare, and contrast the effectiveness of various schemes.The goal of this project is to develop a unifying framework towards the design, analysis and implementation of provably secure Internet routing protocols. The first part of the project explores the use of Secure Network Datalog (SeNDlog), a declarative networking language for encoding secure Internet routing protocols. Language extensions to SeNDLog will be explored, in order to address practical deployments issues at Internet-scale, and facilitate formal analysis of a range of secure routing protocols. These extensions include customizable authentication, goal-oriented evaluation, key distribution and management, and modeling of adversaries. The second part of this project aims to identify security properties of Internet routing protocols, and formally specify them logically in terms of protocol execution traces. The third part of this project aims to design and implement a formal analysis methodology towards verifying SeNDlog programs for desired security properties specified in logic.In terms of broader impact, this project will result a cleaner foundation towards the analysis and development of trustworthy routing protocols.