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

Resumo

Tendências recentes em SDN estendem a programabilidade da rede ao plano de dados através do uso de linguagens de programação como P4. Nesse contexto, a chance de se introduzir erros e, por consequência, vulnerabilidades de software na rede aumenta significativamente já que pacotes passam a ser processados de maneira genérica. Mecanismos de verificação de planos de dados existentes são incapazes de modelar programas P4 ou apresentam grandes restrições no conjunto de propriedades modeladas. Para contornar essas limitações e tornar planos de dados programáveis mais seguros, apresentamos um método de verificação de programas P4 baseado no uso de asserções e execução simbólica. Primeiro, programas P4 são anotados com asserções que expressam propriedades genéricas de corretude e segurança. Em seguida, os programas anotados são transformados em código C e todos seus possíveis caminhos são executados simbolicamente a fim de verificar a validade das asserções inseridas. Resultados mostram que é possível provar um conjunto expressivo de propriedades na ordem de segundos utilizando a técnica proposta.

Referências

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.