A formal method to detect possible P4 specific errors

• Autorzy: Tóth Gabriella , Tejfel Máté

Identyfikatory

DOI

10.15439/2019F355

• Konferencja: Federated Conference on Computer Science and Information Systems (14 ; 01-04.09.2019 ; Leipzig, Germany)
• Języki publikacji: EN

Abstrakty

EN

P4 is a programming language to develop data processing of networks. These kind of programs are used in network devices - like switches - to describe the way of forwarding the received packets to the proper device. Checking the correctness of these program is not an obvious task, because they can easily hide the run time errors. We are working on a method to detect violation of P4 specific properties for these programs. The method if based on a rule system, which can detect suspicious program parts and indicate the violated property to correct it easily. As a first step, we introduce the main idea, dealing with the access of invalid header and uninitialized fields with presenting it with a case study.

Słowa kluczowe

EN

programming language; network devices; switch

PL

język programowania; urządzenia sieciowe; przełącznik

• Wydawca: Polskie Towarzystwo Informatyczne
• Czasopismo: Annals of Computer Science and Information Systems
• Rocznik: 2019
• Tom: Vol. 19
• Strony: 49--56
• Opis fizyczny: Bibliogr. 14 poz., rys.

Twórcy

autor

Tóth Gabriella

• Eötvös Loránd University, Faculty of Informatics, 1/C. Pázmány Péter sny, Budapest, 1117, Hungary

autor

Tejfel Máté

• Eötvös Loránd University, Faculty of Informatics, 1/C. Pázmány Péter sny, Budapest, 1117, Hungary

Bibliografia

• 1. P. Bosshart, D. Daly, G. Gibb, M. Izzard, N. McKeown, J. Rexford, C. Schlesinger, D. Talayco, A. Vahdat, G. Varghese, and D. Walker, “P4: Programming protocol-independent packet processors,” SIGCOMM Comput. Commun. Rev., vol. 44, no. 3, pp. 87–95, 2014. http://dx.doi.org/10.1145/2656877.2656890. [Online]. Available: http://dx.doi.org/10.1145/2656877.2656890
• 2. M. Budiu and C. Dodd, “The p416 programming language,” SIGOPS Oper. Syst. Rev., vol. 51, no. 1, pp. 5–14, Sep. 2017. http://dx.doi.org/10.1145/3139645.3139648. [Online]. Available: http://dx.doi.org/10.1145/3139645.3139648
• 3. L. Freire, M. Neves, L. Leal, K. Levchenko, A. Schaeffer-Filho, and M. Barcellos, “Uncovering Bugs in P4 Programs with Assertion-based Verification,” in Proceedings of the Symposium on SDN Research, ser. SOSR ’18. New York, NY, USA: ACM, 2018. http://dx.doi.org/10.1145/3185467.3185499. ISBN 978-1-4503-5664-0 pp. 4:1–4:7. [Online]. Available: http://dx.doi.org/10.1145/3185467.3185499
• 4. J. Liu, W. Hallahan, C. Schlesinger, M. Sharif, J. Lee, R. Soulé, H. Wang, C. Caşcaval, N. McKeown, and N. Foster, “P4v: Practical Verification for Programmable Data Planes,” in Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, ser. SIGCOMM ’18. New York, NY, USA: ACM, 2018. http://dx.doi.org/10.1145/3230543.3230582. ISBN 978-1-4503-5567-4 pp. 490–503. [Online]. Available: http://dx.doi.org/10.1145/3230543.3230582
• 5. R. Stoenescu, D. Dumitrescu, M. Popovici, L. Negreanu, and C. Raiciu, “Debugging P4 Programs with Vera,” in Proceedings of the 2018 Conference of the ACM Special Interest Group on Data Communication, ser. SIGCOMM ’18. New York, NY, USA: ACM, 2018. ISBN 978-1-4503-5567-4 pp. 518–532. [Online]. Available: http://dx.doi.org/10.1145/3230543.3230548
• 6. (2018) The P4 Language Specification. [Online]. Available: https://p4.org/p4-spec/p4-14/v1.0.5/tex/p4.pdf
• 7. (2018) P 416 Language Specification. [Online]. Available: https://p4.org/p4-spec/docs/P4-16-v1.1.0-spec.pdf
• 8. C. Cadar, D. Dunbar, and D. Engler, “Klee: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs,” in Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, ser. OSDI’08. Berkeley, CA, USA: USENIX Association, 2008, pp. 209–224. [Online]. Available: http://dl.acm.org/citation.cfm?id=1855741.1855756
• 9. L. De Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS’08/ETAPS’08. Berlin, Heidelberg: Springer-Verlag, 2008. http://dx.doi.org/10.1007/978-3-540-78800-3-24. ISBN 3-540-78799-2, 978-3-540-78799-0 pp. 337–340. [Online]. Available: http://dx.doi.org/10.1007/978-3-540-78800-3-24
• 10. R. Stoenescu, M. Popovici, L. Negreanu, and C. Raiciu, “Symnet: Scalable Symbolic Execution for Modern Networks,” in Proceedings of the 2016 ACM SIGCOMM Conference, ser. SIGCOMM ’16. New York, NY, USA: ACM, 2016. http://dx.doi.org/10.1145/2934872.2934881. ISBN 978-1-4503-4193-6 pp. 314–327. [Online]. Available: http://dx.doi.org/10.1145/2934872.2934881
• 11. A. Kheradmand and G. Rosu, “P4K: A formal semantics of P4 and applications,” CoRR, vol. abs/1804.01468, 2018. [Online]. Available: http://arxiv.org/abs/1804.01468
• 12. G. Roşu, K: A semantic framework for programming languages and formal analysis tools, 01 2017, pp. 186–206. [Online]. Available: http://dx.doi.org/10.3233/978-1-61499-810-5-186
• 13. A. Stefănescu, D. Park, S. Yuwen, Y. Li, and G. Roşu, “Semantics-based Program Verifiers for All Languages,” SIGPLAN Not., vol. 51, no. 10, pp. 74–91, Oct. 2016. http://dx.doi.org/10.1145/3022671.2984027. [Online]. Available: http://dx.doi.org/10.1145/3022671.2984027
• 14. The Reference Manual of the Coq. [Online]. Available: https://coq.inria.fr/distrib/current/refman/

Uwagi

1. Track 2: Computer Science & Systems

2. Technical Session: 7th Workshop on Advances in Programming Languages

3. Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).