Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Overview
  • Symposium Organizers
  • Registration Information
    • Registration Discounts
    • Venue, Hotel, and Travel
  • At a Glance
  • Calendar
  • Technical Sessions
  • Activities
    • Posters and Demos
    • Birds-of-a-Feather Sessions
  • Sponsorship
  • Students and Grants
    • Grants for Women
  • Services
  • Questions?
  • Help Promote!
  • For Participants
  • Call for Papers
  • Past Symposia

sponsors

Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
General Sponsor
General Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Software Dataplane Verification
Tweet

connect with us

https://twitter.com/usenix
https://www.facebook.com/usenixassociation
http://www.linkedin.com/groups/USENIX-Association-49559/about
https://plus.google.com/108588319090208187909/posts
http://www.youtube.com/user/USENIXAssociation

Software Dataplane Verification

Authors: 

Mihai Dobrescu and Katerina Argyraki, École Polytechnique Fédérale de Lausanne
Awarded Best Paper!

Abstract: 

Software dataplanes are emerging as an alternative to traditional hardware switches and routers, promising programmability and short time to market. These advantages are set against the risk of disrupting the network with bugs, unpredictable performance, or security vulnerabilities. We explore the feasibility of verifying software dataplanes to ensure smooth network operation. For general programs, verifiability and performance are competing goals; we argue that software dataplanes are different—we can write them in a way that enables verification and preserves performance. We present a verification tool that takes as input a software dataplane, written in a way that meets a given set of conditions, and (dis)proves that the dataplane satisfies crash-freedom, bounded-execution, and filtering properties. We evaluate our tool on stateless and simple stateful Click pipelines; we perform complete and sound verification of these pipelines within tens of minutes, whereas a state-of-the art general-purpose tool fails to complete the same task within several hours.

Mihai Dobrescu, École Polytechnique Fédérale de Lausanne

Katerina Argyraki, École Polytechnique Fédérale de Lausanne

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {179737,
author = {Mihai Dobrescu and Katerina Argyraki},
title = {Software Dataplane Verification},
booktitle = {11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14)},
year = {2014},
isbn = {978-1-931971-09-6},
address = {Seattle, WA},
pages = {101--114},
url = {https://www.usenix.org/conference/nsdi14/technical-sessions/presentation/dobrescu},
publisher = {USENIX Association},
month = apr,
}
Download
Dobrescu PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

Award: 
Best Paper
  • Log in or    Register to post comments

Gold Sponsors

Silver Sponsors

Bronze Sponsors

General Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us