Cornell-Princeton
Center for Network Programming

About

The Center for Network Programming supports research on languages, algorithms, and tools for network programming, and facilitates closer interactions with partners in industry and government. For more details, read our whitepaper.

Projects

Our recent research efforts have produced solutions to a number of fundamental problems related to network programming.

COSciN

COSciN is a new research network connecting Cornell's main campus in Ithaca and medical campus in NYC.

Frenetic

Frenetic is a domain-specific programming language for software-defined networks. Distinguishing features of the language include support for modular composition operators and a careful treatment of routing and monitoring.

iSDX

iSDX (Software-Defined IXP) brings the features of SDN to interdomain routing, offering direct control over packet-processing rules that match on multiple header fields and perform a variety of actions. IXPs are a compelling place to deploy these changes, given their role in interconnecting many networks and their growing importance in bringing popular content closer to end users.

NetKAT

NetKAT is a network programming langauge based on a solid mathematical foundation: Kleene Algebra with Tests (KAT). The langauge has a sound and complete deductive reasoning system and a decision procedure that can be used to address many practical verification problems.

People

Our interdisciplinary research team combines expertise in algorithms, networking, programming languages, systems, and verification.

Co-Directors

Nate Foster

Cornell

Jennifer Rexford

Princeton

Faculty

Rachit Agarwal

Cornell

Nick Feamster

Princeton

Aarti Gupta

Princeton

Bobby Kleinberg

Cornell

Dexter Kozen

Cornell

Sharad Malik

Princeton

David Shmoys

Cornell

Kevin Tang

Cornell

Robbert Van Renesse

Cornell

David Walker

Princeton

Hakim Weatherspoon

Cornell

PhD Students, Postdocs, and Researchers

Mina Tahmasbi Arashloo

Princeton

Shrutarshi Basu

Cornell

Yingjie Bi

Cornell

Ryan Beckett

Princeton

Jennifer Gossels

Princeton

Arpit Gupta

Princeton

Hossein Hojjat

Cornell

Naga Katta

Princeton

Praveen Kumar

Cornell

Craig Riecke

Cornell

Muhammad Shahbaz

Princeton

Steffen Smolka

Cornell

Shih-Hao Tseng

Cornell

Ning Wu

Cornell

>

Seminars

Our monthly "hangouts-on-air" seminar series will be held starting in 2017.

DateApril 18, 2017
Time1:30-2:30pm ET
Videohttps://www.youtube.com/watch?v=zjnm5jlYgrU
TitleNetKAT Tutorial: Programming, Modelling, and Reasoning about Networks
Abstract

NetKAT is a formal system that can be used to program, model, and reason about networks. It comes with a rich formal toolkit including a sounds and complete algebraic axiomatization; an automata theory; a denotational semantics; and an efficient symbolic representation. These theoretic foundations enable powerful tools such as a decision procedure that allows fully automatic verification of important network properties; and a fast compiler that implements powerful programming abstractions. I will give a tutorial on NetKAT, showing how to use it to program networks and reason about their properties.

Bio

Steffen Smolka is a PhD student in Computer Science at Cornell University advised by Nate Foster. Currently his research focuses on languages, tools, and formal foundations for software defined networking. General areas of interest include (probabilistic) semantics, automata theory, and compilers.

Steffen Smolka

Cornell

DateMarch 14, 2017
Time1:30-2:30pm
Video
TitleSNAP: Stateful Network-Wide Abstractions for Packet Processing
Abstract

Early programming languages for software-defined networking (SDN) were built on top of the simple match- action paradigm offered by OpenFlow 1.0. However, emerging hardware and software switches offer much more sophisticated support for persistent state in the data plane, without involving a central controller. Nevertheless, managing stateful, distributed systems efficiently and correctly is known to be one of the most challenging programming problems. To simplify this new SDN problem, we introduce SNAP.

SNAP offers a simpler "centralized" stateful programming model, by allowing programmers to develop programs on top of one big switch rather than many. These programs may contain reads and writes to global, persistent arrays, and as a result, programmers can implement a broad range of applications, from stateful firewalls to fine-grained traffic monitoring. The SNAP compiler relieves programmers of having to worry about how to distribute, place, and optimize access to these stateful arrays by doing it all for them. More specifically, the compiler discovers read/write dependencies between arrays and translates one-big-switch programs into an efficient internal representation based on a novel variant of binary decision diagrams. This internal representation is used to construct a mixed-integer linear program, which jointly optimizes the placement of state and the routing of traffic across the underlying physical topology. We have implemented a prototype compiler and applied it to about 20 SNAP programs over various topologies to demonstrate our techniques’ scalability.

Bio

Mina is a third-year PhD student in Computer Science at Princeton University, advised by Jennifer Rexford. Her research focuses on designing high-level abstractions for network programming and management, specifically in software defined networks (SDNs).

Mina Tahmasbi Arashloo

Princeton