a language for simple, correct-by-construction network configuration

Overview

Propane is a new language for configuring the network. It lets you write a single, high-level routing policy for your network. The Propane compiler can then generate a collection of legacy vendor configurations that are guaranteed to implement the policy correctly. The language and compiler provide the following features and guarantees:

Language and Compiler Guarantees

  • The language lets your write routing policy as if you alway have centralized visibilty of the network
    •  
  • The compiler performs static analysis of the routing policy to proactively find potential issues.
    •  
  • The Propane compiler generates a collection of configurations that run the distributed BGP routing protocol. There is no centralized coordination
    •  
  • The BGP configurations are guaranteed to correctly adapt to all possible failures so that the most preferred paths are always used when available.
    •  
Example Propane Policy:
# Define our function
define Customer = {as101, as102, as103}
define Peer = {Sprint, ATT}

define Routing = {
    true => exit(Customer >> Peer)
}

define transit(X,Y) = 
  enter(X or Y) & exit(X or Y)

define NoTransit = {
    true => not transit(Peer,Peer)
}

define Main = Routing & NoTransit

Members

PrincetonPrinceton

Intnetionet

PrincetonMicrosoft

UCLA UCLA

Publications

Conference Papers

Network Configuration Synthesis With Abstract Topologies.
Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, and David Walker.
In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), , Barcelona, Spain, June 2017.
[ paper]

Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations.
Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, and David Walker.
In ACM SIGCOMM Conference on Communications Architectures, Protocols and Applications (SIGCOMM), Florianopolis , Brazil, August 2016.
[ paper | slides]