P4AIG: Circuit-Level Verification of P4 Programs

Mohammad A. Noureddine, Amanda Hsu, Matthew Chapman Caesar, Fadi A. Zaraket, William H Sanders

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

Abstract

In this work, we set out to develop P4 AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4 AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4 AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4 AIG will exploit the nature of P4 programs to achieve higher scalability in verification.

Original languageEnglish (US)
Title of host publicationProceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages21-22
Number of pages2
ISBN (Electronic)9781728130286
DOIs
StatePublished - Jun 2019
Event49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019 - Portland, United States
Duration: Jun 24 2019Jun 27 2019

Publication series

NameProceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019

Conference

Conference49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019
CountryUnited States
CityPortland
Period6/24/196/27/19

Fingerprint

Networks (circuits)
Sequential circuits
Electric network analysis
Scalability
Pipelines
Hardware
Software

Keywords

  • data plane programs
  • software defined networks
  • verification

ASJC Scopus subject areas

  • Safety, Risk, Reliability and Quality
  • Information Systems
  • Information Systems and Management
  • Computer Networks and Communications

Cite this

Noureddine, M. A., Hsu, A., Caesar, M. C., Zaraket, F. A., & Sanders, W. H. (2019). P4AIG: Circuit-Level Verification of P4 Programs. In Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019 (pp. 21-22). [8805757] (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/DSN-S.2019.00016

P4AIG : Circuit-Level Verification of P4 Programs. / Noureddine, Mohammad A.; Hsu, Amanda; Caesar, Matthew Chapman; Zaraket, Fadi A.; Sanders, William H.

Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019. Institute of Electrical and Electronics Engineers Inc., 2019. p. 21-22 8805757 (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019).

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

Noureddine, MA, Hsu, A, Caesar, MC, Zaraket, FA & Sanders, WH 2019, P4AIG: Circuit-Level Verification of P4 Programs. in Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019., 8805757, Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019, Institute of Electrical and Electronics Engineers Inc., pp. 21-22, 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019, Portland, United States, 6/24/19. https://doi.org/10.1109/DSN-S.2019.00016
Noureddine MA, Hsu A, Caesar MC, Zaraket FA, Sanders WH. P4AIG: Circuit-Level Verification of P4 Programs. In Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019. Institute of Electrical and Electronics Engineers Inc. 2019. p. 21-22. 8805757. (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019). https://doi.org/10.1109/DSN-S.2019.00016
Noureddine, Mohammad A. ; Hsu, Amanda ; Caesar, Matthew Chapman ; Zaraket, Fadi A. ; Sanders, William H. / P4AIG : Circuit-Level Verification of P4 Programs. Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019. Institute of Electrical and Electronics Engineers Inc., 2019. pp. 21-22 (Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019).
@inproceedings{11eab43a84b44ccfbffd331e77243e45,
title = "P4AIG: Circuit-Level Verification of P4 Programs",
abstract = "In this work, we set out to develop P4 AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4 AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4 AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4 AIG will exploit the nature of P4 programs to achieve higher scalability in verification.",
keywords = "data plane programs, software defined networks, verification",
author = "Noureddine, {Mohammad A.} and Amanda Hsu and Caesar, {Matthew Chapman} and Zaraket, {Fadi A.} and Sanders, {William H}",
year = "2019",
month = "6",
doi = "10.1109/DSN-S.2019.00016",
language = "English (US)",
series = "Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "21--22",
booktitle = "Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019",
address = "United States",

}

TY - GEN

T1 - P4AIG

T2 - Circuit-Level Verification of P4 Programs

AU - Noureddine, Mohammad A.

AU - Hsu, Amanda

AU - Caesar, Matthew Chapman

AU - Zaraket, Fadi A.

AU - Sanders, William H

PY - 2019/6

Y1 - 2019/6

N2 - In this work, we set out to develop P4 AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4 AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4 AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4 AIG will exploit the nature of P4 programs to achieve higher scalability in verification.

AB - In this work, we set out to develop P4 AIG, a tool for the static verification of programmable data planes using sequential circuit analysis. P4 AIG targets P4 programs by treating them as hardware pipelines rather than software programs. P4 AIG allows for the circuit-level treatment of P4 programs, a feature not available for traditional software verification techniques. We believe that P4 AIG will exploit the nature of P4 programs to achieve higher scalability in verification.

KW - data plane programs

KW - software defined networks

KW - verification

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

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

U2 - 10.1109/DSN-S.2019.00016

DO - 10.1109/DSN-S.2019.00016

M3 - Conference contribution

AN - SCOPUS:85072041103

T3 - Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019

SP - 21

EP - 22

BT - Proceedings - 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental Volume, DSN-S 2019

PB - Institute of Electrical and Electronics Engineers Inc.

ER -