Relatorio Parcial de Atividades de Bolsa de Iniciacao Cientıfica

Instituto de Informatica

Universidade Federal do Rio Grande do Sul

Levindo Neto

Dados de Identificacao

Projeto

Tıtulo do Projeto: NetMan Patterns:Padroes de Gerenciamento para Resiliencia e Seguranca de Redes

Vigencia da Bolsa: 01/01/2016 a 31/07/2016Orientador: Alberto Egon Schaeffer Filho

Bolsista

Nome: Levindo Gabriel Taschetto NetoCurso: Bachalerado em Engenharia de ComputacaoCPF: ***.***.***-**E-mail: levindo.neto@inf.ufrgs.br

Perıodo de Atuacao: 01/01/2016 a 31/07/2016Local de Realizacao: Instituto de Informatica

Universidade Federal do Rio Grande do Sul

1

1

1.1 Introducao

Esse relatorio descreve as atividades desenvolvidas ate o presente momento por Levindo GabrielTaschetto Neto durante o perıodo de vigencia da bolsa de iniciacao cientıfica, a qual e de 01/01/2016a 31/07/2016. Esse documento contem descritos todos os trabalhos realizados ate o momento,resultados obtidos, proximas etapas e resultados esperados.

No projeto estao sendo desenvolvidos estudos na area de redes de computadores e logica apli-cada a computacao visando resiliencia. Resiliencia em redes de computadores esta relacionada acapacidade da rede manter nıveis aceitaveis de operacao frente a anomalias, tais como ataques ma-liciosos, sobrecarga operacional, problemas de configuracao ou falhas de equipamento. O projeto“Net Patterns : Padroes de Gerenciamento para Resiliencia e Seguranca de Redes” esta sendo de-senvolvido em colaboracao com pesquisadores da Lancaster University, situada na Inglaterra, ondeo coordenador do projeto fez seu pos-doutorado, entre 2009 e 2012.

1.2 Estudos iniciais

No inıcio da bolsa de iniciacao cientıfica adquiri conhecimentos na area de redes de computadores,na qual eu nao havia tido contato anteriormente em outros trabalhos na universidade. Os conheci-mentos na area foram adquiridos com o auxılio de artigos cientıficos, videoaulas, conversas com oscolegas do grupo e com a pratica ao mexer nas ferramentas utilizadas, Mininet e Floodlight.

Os artigos cientıficos lidos inicialmente foram focados na area de virtualizacao de redes de com-putadores [3] e na area de redes definidas por software (SDN ) [5]. As videoaulas assistidas foramas do curso ”Computer Networks” da University of Washington por meio da plataforma de ensinoonline Coursera (www.coursera.org/course/comnetworks). As ferramentas utilizadas no projetodesde o inıcio da bolsa, sao o emulador de rede, Mininet (www.mininet.org) em conjunto com ocontrolador SDN, Floodlight (www.projectfloodlight.org).

1.3 Problema abordado no projeto e meios de resolucao

O problema no qual estao sendo desenvolvidos os trabalhos e o de encontrar um ou mais metodospara verificacao formal em redes definidas por software. Antes de iniciar os trabalhos na area deresiliencia de redes de computadores com verificacao formal, pesquisas foram realizadas em artigoscientıficos [4, 2, 1], a fim de obter informacoes do estado da arte na area e saber como pesquisadoresao redor do mundo lidam com o mesmo problema. Um dos problemas que foi resolvido e o deencontrar redundancias e conflitos em uma rede e em regras de um Firewall, o que e detalhado naproxima secao.

2

1.4 Resultados

Obtencao, manipulacao e verificacao formal dos dados de Flowtable

Inicialmente foi desenvolvida uma aplicacao, desenvolvida na linguagem de programacao Python,que dada uma topologia de rede qualquer, retorna os dados referentes a cada switch OpenFlowdessa rede, como por exemplo match(dados de partida) e action(dados de acoes a serem tomadaspor cada switch). Esses dados ficam contidos em uma tabela (Flowtable), a qual pode ser acessadapor o controlador da rede SDN utilizado, que nessa aplicacao e o Floodlight OpenFlow Controller.

Na aplicacao desenvolvida e possıvel fazer a coleta de todos esses dados da flowtable, manipularesses dados para formar uma tabela de facil visualizacao para manipula-la a fim de encontrar re-gras redundantes e conflitantes, para por fim gerar um arquivo atualizado com todas as regras daflowtable, regras conflitantes e regras redundantes, no formato de expressoes logicas. O algoritmoproposto para verificacao formal dos dados da flowtable possui complexidade O(n2), e seu funciona-mento esta baseado na comparacao de todas as regras entre si, diminuindo uma comparacao a cadaiteracao. Apos a execucao da aplicacao, todas as regras redundantes e conflitantes sao salvas emuma tabela, e podem ser removidas.

Verificacao formal em regras do firewall

Depois de obter os dados da flowtable, foi incrementado na aplicacao a funcionalidade de adicionarregras no firewall (regra a regra), adicionar regras no firewall (string com um conjunto de regras),deletar regra no firewall, visualizar todas as regras contidas no firewall, geracao da tabela de dadoscontidos no firewall e manipulacao desses dados para verificar redundancias e conflitos logicos.

Depois de ter essa parte da aplicacao pronta, foram feitos testes para adicionar regras ao firewallda topologia, forcando conflitos e redundancias logicas para verificar que a aplicacao cumpre asespecificacoes definidas. O algoritmo utilizado na verificacao logica das regras do firewall e o mesmoespecificado para a verificacao logica das regras da flowtable.

1.5 Conclusao

Esse relatorio descreveu as atividades realizadas ate o momento durante o perıodo de vigencia dabolsa de iniciacao cientıfica com seus devidos resultados. Na bolsa, assim como mostrado, tem-setrabalhado com verificacao formal de redes de computadores definidas por software.

As proximas etapas serao adicionar novas funcionalidades de verificacao na rede, tais comoreachability(verificar se um determinado pacote que sai de um switch A chega em um switch B), everificar se ha loops em alguma parte da rede. Para fazer essas verificacoes na rede, sera utilizadanovamente formalismos logicos, de maneira a provar a consistencia da rede de forma rapida e precisa.

3

Bibliografia

[1] Arjun Guha; Mark Reitblatt; Nate Foster. Machine-verified network controllers. SIGPLANNot., 48(6):483–494, June 2013.

[2] Nikolaj Bjørner; Karthick Jayaraman. Checking cloud contracts in microsoft azure. In Dis-tributed Computing and Internet Technology - 11th International Conference, ICDCIT 2015,Bhubaneswar, India, February 5-8, 2015. Proceedings, pages 21–32, 2015.

[3] Bo Han; Vijay Gopalakrishnan; Lusheng Ji; Seungjoon Lee. Network function virtualization:Challenges and opportunities for innovations. In IEEE Communications Magazine (2015), 2014.

[4] Aurojit Panda; Katerina Argyraki; Mooly Sagiv; Michael Schapira; Scott Shenker. New direc-tions for network verification. In SNAPL (2015), 2015.

[5] Nick Feamster; Jennifer Rexford; Ellen Zegura. The road to sdn: An intellectual history ofprogrammable networks. SIGCOMM Comput. Commun. Rev., 44(2):87–98, April 2014.

4