I am a software developer at Nefeli Networks and starting Fall 2018 an assistant professor in Computer Science at NYU. Previously, I received my PhD from UC Berkeley where I was advised by Scott Shenker and worked in the NetSys Lab.

My research interest lie in finding lightweight mechanisms for achieving correctness in systems (broadly defined). My dissertation looked at how to implement and execute network functions; and how to verify correctness for NFV (network function virtualization) deployments. A complete list of my publications can be found below.

Before Berkeley, I worked on the Midori kernel at Microsoft. Before that, I received a Sc.B. in Math-CS with honors from Brown. My honors thesis was on symmetry breaking in constraint satisfaction problems.

I am looking for PhD students interested in systems, distributed systems, networking, formal methods or just working with me at NYU. The application can be found here. Feel free to e-mail me if you have questions.

Selected Projects


Networks -- including the one you used to access this page -- now need to do a lot more than routing packets to a destination. This includes ensuring security -- through firewalls and IDSes -- providing caching, implementing proxies for video conferencing etc. How should NFs be built and deployed on shared servers? NetBricks provides a set of high-level abstractions that allow NFs to be expressed in a safe language, without sacrificing performance. Processes and VMs cannot meet the I/O requirement of NFs, and NetBricks instead uses software isolation techniques for isolation.
OSDI'16 Paper | OSDI'16 Slides | Website.

Verification for Network with Network Functions

While network functions are essential for adding functionality to networks, they also affect network correctness. For example a misconfigured cache might allow access to unauthorized data. Current network verification techniques cannot account for network functions, or any stateful network components. However, since NFs are general applications, verification on the actual semantics is often undecidable and is infeasible for large networks. In a series of network verification papers we have proposed the use of models, and different techniques -- including compositional verification -- for networks with network functions.
NSDI'17 Paper | SNAPL'15 Paper | arXiv Paper | TACAS'16 paper on complexity | SNAPL'15 Slides | NetPL'16 Slides.

Consistency Requirements for SDN

Software defined networks increasingly rely on distributed control planes. In many cases the control plane can be partitioned while the data plane is connected. What limits does this place on network policies? We investigated this in CAP for networks. Next, in SCL we investigated the consistency requirement of SDN control planes, and found that this depended on the policy being implemented. Further we showed that eventual consistency is sufficient for implementing many common policies.
NSDI'17 Paper | HotSDN'13 Paper

Perfect Routing Resilience

Can a routing algorithm provide perfect resilience and ensure that paths are available as long as the network remains connected? The answer is no when packet sizes are bounded and changes to the forwarding table are disallowed. DDC achieves perfect resilience while using only 2-extra bits in the packet header. In subsequent work we have also explored the limits of resilience achievable with fixed forwarding tables.
NSDI'13 Paper | NSDI'13 Slides | NSDI'13 Video | PODC'12 Paper | INFOCOM'16 Paper.

Interdomain Routing

Routing traffic on the internet requires traversing several independent autonomous systems (ASes). Since ASes do not always trust each other, the set of available paths is decided through contract negotiations between these ASes, and this limits flexibility on the internet. We proposed a new inter-domain routing system, Route Bazaar, that uses cryptocurrency block-chains (which provide a tamper proof log) and automated agents to provide greater routing flexibility.
HotOS'15 Paper