Annals of Computer Science and Information Systems, Volume 19

DOI: http://dx.doi.org/10.15439/2019F355

Citation: Position Papers of the 2019 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 19, pages 49–56 (2019)

Full text

Abstract. 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.

References

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/