Software Dataplane Verification.
The industry is in the mood for programmable networks, where an operator can dynamically deploy network functions on network devices, akin to how one deploys virtual machines on physical machines in a cloud environment. Such flexibility brings along the threat of unpredictable behavior and performan...
| Publicado en: | Communications of the ACM Vol. 58; no. 11; pp. 113 - 122 |
|---|---|
| Autores principales: | , |
| Formato: | Artículo |
| Publicado: |
Association for Computing Machinery
Nov2015
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=110567344&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 110567344 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00010782 ACM jtl: Communications of the ACM issn: 00010782 maglogo: N pubinfo: dt: Nov2015 vid: 58 iid: 11 pid: 68 pub: Association for Computing Machinery artinfo: ui: 110567344 10.1145/2823400 ppf: 113 ppct: 9 formats: tig: atl: Software Dataplane Verification. aug: au: Dobrescu, Mihai Argyraki, Katerina affil: EPFL, Lausanne, Switzerland su: Software verification Computer network monitoring Data packeting Domain-specific programming languages Coding theory Security systems sug: subj: Software verification Computer network monitoring Data packeting Domain-specific programming languages Coding theory Security systems ab: The industry is in the mood for programmable networks, where an operator can dynamically deploy network functions on network devices, akin to how one deploys virtual machines on physical machines in a cloud environment. Such flexibility brings along the threat of unpredictable behavior and performance. What are the minimum restrictions that we need to impose on network functionality such that we are able to verify that a network device behaves and performs as expected, for example, does not crash or enter an infinite loop? We present the result of working iteratively on two tasks: designing a domain-specific verification tool for packet-processing software, while trying to identify a minimal set of restrictions that packet-processing software must satisfy in order to be verification-friendly. Our main insight is that packet-processing software is a good candidate for domain-specific verification, for example, because it typically consists of distinct pieces of code that share limited mutable state; we can leverage this and other properties to sidestep fundamental verification challenges. We apply our ideas on Click packet-processing software; we perform complete and sound verification of an IP router and two simple middleboxes within tens of minutes, whereas a state-of-the-art general-purpose tool fails to complete the same task within several hours. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2015 holdings: @attributes: islocal: N |
|---|