A Simple Approach to Verify and Debug Data Plane Programs

  • Eduardo Castilho Rosa IFGoiano / UFU
  • Italo Tiago da Cunha UFJ / UFU
  • Flávio de Oliveira Silva UFU

Resumo


The advances in data plane programmability through domain-specific languages such as P4 require the adoption of verification methods to ensure that a given code behaves appropriately. The standard approach in the literature is to use formal methods to verify a provided software. However, traditional techniques are often time-consuming and expensive. In this work, we propose a model to demonstrate the behavior of a P4 program that is simple and fast. To validate our model, we have used a name-based forwarding program and a control plane application that injects in a P4 table a total of 1 million random name prefixes. The results have shown that our model can quickly indicate whether or not a given program is behaving correctly.

Referências

de Moura, L. and Bjørner, N. (2008). Z3: An efficient smt solver. In Ramakrishnan, C. R. and Rehof, J., editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, Berlin, Heidelberg. Springer Berlin Heidelberg.

DomCop.com (2021). Top 10 million websites. https://www.domcop.com/top-10-million-website. last accessed: May 1, 2021.

Hancock, D. and van der Merwe, J. (2016). Hyper4: Using p4 to virtualize the programmable data plane. In Proceedings of the 12th International on Conference on Emerging Networking EXperiments and Technologies, CoNEXT '16, page 35-49, New York, NY, USA. Association for Computing Machinery.

Jin, X., Li, X., Zhang, H., Soulé, R., Lee, J., Foster, N., Kim, C., and Stoica, I. (2017). Netcache: Balancing key-value stores with fast in-network caching. In Proceedings of the 26th Symposium on Operating Systems Principles, SOSP '17, page 121-136, New York, NY, USA. Association for Computing Machinery.

Liu, J., Hallahan, W., Schlesinger, C., Sharif, M., Lee, J., Soulé, R., Wang, H., Cascaval, C., McKeown, N., and Foster, N. (2018). P4v: Practical verification for programmable data planes. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '18, page 490-503, New York, NY, USA. Association for Computing Machinery.

Rosa, E. C. and Silva, F. d. O. (2022). A hash-free method for fib and lnpm in icn programmable data planes. In 2022 International Conference on Information Networking (ICOIN), pages 186-191.

Stoenescu, R., Dumitrescu, D., Popovici, M., Negreanu, L., and Raiciu, C. (2018). Debugging p4 programs with vera. In Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, SIGCOMM '18, page 518-532, New York, NY, USA. Association for Computing Machinery.

Stoenescu, R., Popovici, M., Negreanu, L., and Raiciu, C. (2016). Symnet: Scalable symbolic execution for modern networks. In Proceedings of the 2016 ACM SIGCOMM Conference, SIGCOMM '16, page 314-327, New York, NY, USA. Association for Computing Machinery.
Publicado
27/05/2022
Como Citar

Selecione um Formato
ROSA, Eduardo Castilho; CUNHA, Italo Tiago da; SILVA, Flávio de Oliveira. A Simple Approach to Verify and Debug Data Plane Programs. In: WORKSHOP DE PESQUISA EXPERIMENTAL DA INTERNET DO FUTURO (WPEIF), 13. , 2022, Fortaleza. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2022 . p. 47-52. ISSN 2595-2692. DOI: https://doi.org/10.5753/wpeif.2022.223586.