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

TC：小型：协作研究：建立分析和实施安全路由协议的正式框架

• 批准号: 1115706
• 负责人: Limin Jia
• 金额: $ 29.93万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2011
• 资助国家: 美国
• 起止时间: 2011-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1115706&HistoricalAwards=false
• 关键词: TC; Small; Collaborative; Research; Towards

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.

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