Bio

Overview:

I am a 4th year PhD student at Princeton studying programming language theory with my advisor David Walker. I received Bachelors degrees in Computer Science and Mathematics from the University of Virginia. More recently, I have been working on applications of domain-specific languages to software-defined networking. My interests broadly include type theory, automata, verification, and program synthesis. [PDF iconCurrent CV]

Current Projects:

Kleen Algebra Modulo Theories: A new, modular approach to extending Kleene Algebras with domain-specific theories. Given a complete and decidable theory for a predicate language, and a restriction we call "pushback", we show how to derive soundness, completeness, and decidability results, as well as an implementation in OCaml that can decide equivalence of terms, for a Kleene Algebra that embeds this predicate language. Using this framework, we have been able to create theories for bitvectors, natural numbers, unbounded sets and maps, NetKAT, Past-time Linear Temporal Logic, Temporal NetKAT, and distributed routing protocols.

Minesweeper: A new network control plane verification tool. Minesweeper can read unmodified configurations from languages provided by Cisco, Juniper, Arista and other vendors, and verify many properties such as reachability between devices. Unlike existing data plane analysis tools, Minesweeper will check correctness for all possible data planes that might emerge from the control plane -- taking into account possible link failures, collections of eBGP messages from neighbors, and different control plane message orderings. It does this by translating configurations for BGP, OSPF, static routes and more into a collection of logical constraints that can be solved by off-the-shelf SMT solvers.

[Home Page]

Propane: A language and compiler for writing high-level specifications of centralized routing policy and generating distributed, fault-tolerant, low-level router configurations. Propane extends the SDN model of network programming to both intra-domain and inter-domain routing, allowing programmers to write high-level constraints on the types of paths traffic may take through either their own network or other networks. The compiler generates device-by-device BGP configurations that run on traditional, unmodified network devices in such a way that the distributed implementation is guaranteed to remain policy-compliant even when any combinations of device/link failures occur in the network. 

[Home Page]

Temporal NetKAT: A network programming language that extends the NetKAT language with a richer set of temporal logic predicates for dynamically querying packet history. The addition of temporal queries allows Temporal NetKAT to express problems related to network programming, traffic monitoring, network debugging, security enforcement, and program verification in a single language. The metatheory extends the soundness and completeness results from the NetKAT language.

[Home Page]

Papers:

  • Kleene Algebra Modulo Theories. Ryan Beckett, Eric Campbell, and Michael Greenberg. In Submission. [Paper

 

  • A General Approach to Network Configuration Verification. Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker. In ACM SIGCOMM, August 2017. [Paper]

 

  • Network Configuration Synthesis with Abstract Topologies. Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, David Walker.  In ACM SIGPLANN Conference on Programming Language Design and Implementation (PLDI), June, 2017. [Paper]

 

  • Don't Mind the Gap: Bridging Network-wide Objectives and Device-level Configurations. Ryan Beckett, Ratul Mahajan, Todd Millstein, Jitu Padhye, David Walker. ACM SIGCOMM, August 2016. Best Paper Award. [Paper]

 

  • Temporal NetKAT. Ryan Beckett, Michael Greenberg, David Walker. In ACM SIGPLANN Conference on Programming Language Design and Implementation (PLDI), June, 2016. [Paper]

 

  • Temporal NetKAT. Ryan Beckett, Michael Greenberg, David Walker. PLVNET 2015: 1st Workshop on Programming Languages and Verification Technology for Networking, January 2015. [Paper]

 

  • An Assertion Language for Debugging SDN Applications. Ryan Beckett, Kelvin Zou, Shuyuan Zhang, Sharad Malik, Jennifer Rexford, David Walker. ACM SIGCOMM HotSDN Workshop, August 2014. [Paper]