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


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
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


Other2018 Symposium on SDN Research, SOSR 2018
Country/TerritoryUnited States
CityLos Angeles


  • P4
  • Programmable data planes
  • Verification

ASJC Scopus subject areas

  • Software
  • Computer Networks and Communications


Dive into the research topics of 'Uncovering bugs in P4 programs with assertion-based verification'. Together they form a unique fingerprint.

Cite this