Skip to main content

Seminar:  Verifying Networking Protocols Using Declarative Networking

Date:March 3, 2014 
Talk Title:Verifying Networking Protocols Using Declarative Networking
Speaker:Limin Jia
Time & Location:12:00pm - 1:00pm
CIC Building, Pittsburgh

Abstract

The stability and security of routing protocols is critical to ensuring the operability of today's increasingly network-oriented computing environments. Unfortunately, current tools make it difficult to effectively analyze the properties of routing protocols: they typically require protocols to be specified very abstractly, and don't support empirical evaluation, which is an important aspect of protocol analysis.

In this talk, I will present our work on leveraging NDlog, a declarative networking language, to build a unified framework for implementing, formally verifying, and empirically evaluating network protocols. In this framework, the RapidNet compiler compiles NDlog programs into efficient low-level code that can be deployed in the network. Furthermore, the declarative nature of NDlog enables us to apply a variety of verification techniques to analyze protocols encoded in NDlog. I will explain how we reduce route convergence problems to SAT and our recent work on designing a program logic for NDlog programs that can be used to verify path authenticity properties of secure routing protocols.d program verification.

Speaker Bio

Limin Jia is an Associate Research Professor at CyLab at Carnegie Mellon University. Her research interests include programming languages, language-based security, type systems, logic, and program verification.