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.
