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

今天的互联网运行边界网关协议（BGP），一个复杂的域间路由协议。在过去的几年里，人们对BGP路由的复杂性和脆弱性达成了越来越多的共识。除了路由振荡和收敛速度慢的问题，BGP已被证明是容易受到恶意攻击。尽管BGP的安全漏洞提出了广泛的解决方案，目前还缺乏一套共同的工具，研究人员来分析，比较和对比各种schems.The目标的有效性，这个项目是开发一个统一的框架，可证明安全的互联网路由协议的设计，分析和实施。该项目的第一部分探讨了安全网络数据库（SeNDlog）的使用，这是一种用于编码安全Internet路由协议的声明性网络语言。 将探讨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.