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
N1 - Publisher Copyright:
© 2018 held by the owner/author(s).
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
T2 - 2018 Symposium on SDN Research, SOSR 2018
Y2 - 28 March 2018 through 29 March 2018
ER -