Combatendo vulnerabilidades em programas P4 com verificação baseada em asserções

• Lucas Freire UFRGS
• Miguel Neves UFRGS
• Alberto Schaeffer-Filho UFRGS
• Marinho Barcellos UFRGS

DOI: https://doi.org/10.5753/sbseg.2017.19508

Abstract

Current trends in SDN extend the network programmability to the data plane through the usage of programming languages like P4. In this context, the chances of introducing errors, and consequently software vulnerabilities in the network significantly increases, since packets can be processed in a general fashion. Existing data plane verification mechanisms are incapable of modeling P4 programs or present severe restrictions in the set of modeled properties. To circumvent these limitations and make programmable data planes more secure, we present a P4 program verification approach based on the usage of assertions and symbolic execution. First, P4 programs are annotated with assertions expressing general correctness and security properties. Then, the annotated programs are transformed in C code and all their possible paths are symbolically executed to verify the inserted assertions validity. Results show that it is possible to prove an expressive set of properties in the order of seconds using the proposed technique.

References

Beckett, R., Zou, X. K., Zhang, S., Malik, S., Rexford, J., and Walker, D. (2014). An assertion language for debugging sdn applications. In Proceedings of the ThirdWorkshop on Hot Topics in Software Defined Networking, HotSDN ’14, pages 91–96, New York, NY, USA. ACM.

Bosshart, P., Daly, D., Gibb, G., Izzard, M., McKeown, N., Rexford, J., Schlesinger, C., Talayco, D., Vahdat, A., Varghese, G., and Walker, D. (2014). P4: Programming protocol-independent packet processors. SIGCOMM Comput. Commun. Rev., 44(3):87–95.

Cadar, C., Dunbar, D., and Engler, D. (2008). 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, OSDI’08, pages 209–224, Berkeley, CA, USA. USENIX Association.

Dang, H. T., Sciascia, D., Canini, M., Pedone, F., and Soulé, R. (2015). Netpaxos: Consensus at network speed. In Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research, SOSR ’15, pages 5:1–5:7, New York, NY, USA. ACM.

Dang, H. T., Wang, H., Jepsen, T., Brebner, G., Kim, C., Rexford, J., Soulé, R., and Weatherspoon, H. (2017). Whippersnapper: A p4 language benchmark suite. In Proceedings of the Symposium on SDN Research, SOSR ’17, pages 95–101, New York, NY, USA. ACM.

Dobrescu, M. and Argyraki, K. (2014). Software dataplane verification. In 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI 14), pages 101–114, Seattle, WA. USENIX Association.

Khurshid, A., Zhou, W., Caesar, M., and Godfrey, P. B. (2012). Veriflow: Verifying network-wide invariants in real time. In Proceedings of the First Workshop on Hot Topics in Software Defined Networks, HotSDN ’12, pages 49–54, New York, NY, USA. ACM.

Krupp, J., Backes, M., and Rossow, C. (2016). Identifying the scan and attack infrastructures behind amplification ddos attacks. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS ’16, pages 1426–1437, New York, NY, USA. ACM.

Lee, T., Pappas, C., Perrig, A., Gligor, V., and Hu, Y.-C. (2017). The case for in-network replay suppression. In Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security, ASIA CCS ’17, pages 862–873, New York, NY, USA. ACM.

Lopes, N., Bjørner, N., McKeown, N., Rybalchenko, A., Talayco, D., and Varghese, G. (2016). Automatically verifying reachability and well-formedness in p4 networks. Technical report.

Lopes, N. P., Bjørner, N., Godefroid, P., Jayaraman, K., and Varghese, G. (2015). Checking beliefs in dynamic networks. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 499–512, Oakland, CA. USENIX Association.

Sivaraman, A., Kim, C., Krishnamoorthy, R., Dixit, A., and Budiu, M. (2015). Dc.p4: Programming the forwarding plane of a data-center switch. In Proceedings of the 1st ACM SIGCOMM Symposium on Software Defined Networking Research, SOSR ’15, pages 2:1–2:8, New York, NY, USA. ACM.

Sivaraman, V., Narayana, S., Rottenstreich, O., Muthukrishnan, S., and Rexford, J. (2017). Smoking out the heavy-hitter flows with hashpipe. SOSR ’17.

Son, S., Shin, S., Yegneswaran, V., Porras, P., and Gu, G. (2013). Model checking invariant security properties in openflow. In 2013 IEEE International Conference on Communications (ICC), pages 1974–1979. IEEE.

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, pages 314–327, New York, NY, USA. ACM.