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 language | English (US) |
|---|---|
| Title of host publication | Proceedings of the Symposium on SDN Research, SOSR 2018 |
| Publisher | Association for Computing Machinery, Inc |
| ISBN (Electronic) | 9781450356640 |
| DOIs | |
| State | Published - Mar 28 2018 |
| Externally published | Yes |
| Event | 2018 Symposium on SDN Research, SOSR 2018 - Los Angeles, United States Duration: Mar 28 2018 → Mar 29 2018 |
Publication series
| Name | Proceedings of the Symposium on SDN Research, SOSR 2018 |
|---|
Other
| Other | 2018 Symposium on SDN Research, SOSR 2018 |
|---|---|
| Country | United States |
| City | Los Angeles |
| Period | 3/28/18 → 3/29/18 |
Fingerprint
Keywords
- P4
- Programmable data planes
- Verification
ASJC Scopus subject areas
- Software
- Computer Networks and Communications
Cite this
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 proceeding › Conference contribution
}
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 -