Uncovering bugs in P4 programs with assertion-based verification

Lucas Freire, Miguel Neves, Lucas Leal, Kirill Levchenko, Alberto Schaeffer-Filho, Marinho Barcellos

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.

Original languageEnglish (US)
Title of host publicationProceedings of the Symposium on SDN Research, SOSR 2018
PublisherAssociation for Computing Machinery, Inc
ISBN (Electronic)9781450356640
DOIs
StatePublished - Mar 28 2018
Externally publishedYes
Event2018 Symposium on SDN Research, SOSR 2018 - Los Angeles, United States
Duration: Mar 28 2018Mar 29 2018

Publication series

NameProceedings of the Symposium on SDN Research, SOSR 2018

Other

Other2018 Symposium on SDN Research, SOSR 2018
CountryUnited States
CityLos Angeles
Period3/28/183/29/18

Fingerprint

Computer programming languages
Defects
Software defined networking

Keywords

  • P4
  • Programmable data planes
  • Verification

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications

Cite this

Freire, L., Neves, M., Leal, L., Levchenko, K., Schaeffer-Filho, A., & Barcellos, M. (2018). Uncovering bugs in P4 programs with assertion-based verification. In Proceedings of the Symposium on SDN Research, SOSR 2018 [3185499] (Proceedings of the Symposium on SDN Research, SOSR 2018). Association for Computing Machinery, Inc. https://doi.org/10.1145/3185467.3185499

Uncovering bugs in P4 programs with assertion-based verification. / Freire, Lucas; Neves, Miguel; Leal, Lucas; Levchenko, Kirill; Schaeffer-Filho, Alberto; Barcellos, Marinho.

Proceedings of the Symposium on SDN Research, SOSR 2018. Association for Computing Machinery, Inc, 2018. 3185499 (Proceedings of the Symposium on SDN Research, SOSR 2018).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Freire, L, Neves, M, Leal, L, Levchenko, K, Schaeffer-Filho, A & Barcellos, M 2018, Uncovering bugs in P4 programs with assertion-based verification. in Proceedings of the Symposium on SDN Research, SOSR 2018., 3185499, Proceedings of the Symposium on SDN Research, SOSR 2018, Association for Computing Machinery, Inc, 2018 Symposium on SDN Research, SOSR 2018, Los Angeles, United States, 3/28/18. https://doi.org/10.1145/3185467.3185499
Freire L, Neves M, Leal L, Levchenko K, Schaeffer-Filho A, Barcellos M. Uncovering bugs in P4 programs with assertion-based verification. In Proceedings of the Symposium on SDN Research, SOSR 2018. Association for Computing Machinery, Inc. 2018. 3185499. (Proceedings of the Symposium on SDN Research, SOSR 2018). https://doi.org/10.1145/3185467.3185499
Freire, Lucas ; Neves, Miguel ; Leal, Lucas ; Levchenko, Kirill ; Schaeffer-Filho, Alberto ; Barcellos, Marinho. / Uncovering bugs in P4 programs with assertion-based verification. Proceedings of the Symposium on SDN Research, SOSR 2018. Association for Computing Machinery, Inc, 2018. (Proceedings of the Symposium on SDN Research, SOSR 2018).
@inproceedings{e825c6d111974832b1cd8067a6374941,
title = "Uncovering bugs in P4 programs with assertion-based verification",
abstract = "Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.",
keywords = "P4, Programmable data planes, Verification",
author = "Lucas Freire and Miguel Neves and Lucas Leal and Kirill Levchenko and Alberto Schaeffer-Filho and Marinho Barcellos",
year = "2018",
month = "3",
day = "28",
doi = "10.1145/3185467.3185499",
language = "English (US)",
series = "Proceedings of the Symposium on SDN Research, SOSR 2018",
publisher = "Association for Computing Machinery, Inc",
booktitle = "Proceedings of the Symposium on SDN Research, SOSR 2018",

}

TY - GEN

T1 - Uncovering bugs in P4 programs with assertion-based verification

AU - Freire, Lucas

AU - Neves, Miguel

AU - Leal, Lucas

AU - Levchenko, Kirill

AU - Schaeffer-Filho, Alberto

AU - Barcellos, Marinho

PY - 2018/3/28

Y1 - 2018/3/28

N2 - Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.

AB - Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.

KW - P4

KW - Programmable data planes

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85049408295&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85049408295&partnerID=8YFLogxK

U2 - 10.1145/3185467.3185499

DO - 10.1145/3185467.3185499

M3 - Conference contribution

AN - SCOPUS:85049408295

T3 - Proceedings of the Symposium on SDN Research, SOSR 2018

BT - Proceedings of the Symposium on SDN Research, SOSR 2018

PB - Association for Computing Machinery, Inc

ER -