Network testing through grammars : towards the analysis of property violation on computer networks

Abstract

A clear trend within the context of computer networks is the use of software as an alternative to the use of specialized hardware. The benefit of this trend is an enhancement of flexibility, modularity, and maintainability of network components. Concurrently, it is challenging to de termine if everything is happening correctly in a computer network where software, possibly with bugs, is very present. To deal with this challenge, network testing is frequently used to check if a network component respects a given property and consequently performs its actions correctly. As there is a variety of causes for the abnormal operation of the network, ranging from human mistakes (inserting misconfiguration) to malicious activities, there are many chal lenges to network testing to achieve satisfactory results. Research in this field frequently tries to improve network testing by the use of formal verification techniques and network monitoring to detect property violations, such as configuration errors and policy conflicts. However, formal verification by itself cannot detect a property violation that was not anticipated and included in the model. Similarly, network monitoring needs to wait for a property violation to occur to de tect it. Consequently, both enhancement efforts fail to achieve a complete result. In this thesis, we investigate the problem of achieve the absence of property violations by combining the ad vantages of network monitoring for detecting property violations with the advantages of formal verification to model the network and prove the existence or absence of property violations. A highlight related to the success of such a combination is the use of a model based on grammars to capture the communication patterns existing on the network. Our analysis allows the eval uation of high-level properties such as "Can network component x send HTTP packets? " and the detection of property violations, such as conflicting forwarding rules, as soon they occurred in the network. As future research, we intend to further investigate how our grammar-based model can be extended to support temporal logic operators and how we can trace the effects of property violations in the network.

Uma tendência clara no contexto das redes de computadores é o uso de software como uma alternativa ao uso de hardware especializado. O benefício dessa tendência é um aprimora mento da flexibilidade, modularidade e capacidade de manutenção de componentes de rede. Ao mesmo tempo, é desafiador determinar se tudo está acontecendo corretamente em uma rede de computadores onde o software, possivelmente com erros (bugs), está muito presente. Para lidar com este desafio, teste de rede é freqüentemente usado para verificar se um componente de rede respeita uma determinada propriedade e conseqüentemente executa suas ações corretamente. Como há uma variedade de causas para o funcionamento anormal da rede, variando de erros humanos (inserir configuração incorreta) para atividades maliciosas, existem muitos desafios para o teste de rede alcançar resultados satisfatórios. Pesquisas neste campo freqüentemente tenta melhorar os testes de rede pelo uso de técnicas de verificação formal e monitoramento de rede para detectar violações de propriedade, como erros de configuração e conflitos de política. No entanto, verificação formal por si só não consegue detectar uma violação de propriedade que não foi antecipada e incluída no modelo. Da mesma forma, monitoramento de rede precisa aguardar a ocorrência de uma violação de propriedade para detectá-la. Consequentemente, ambos esforços de aprimoramento falham em alcançar um resultado completo. Nesta tese, nós investigamos o problema de garantir a ausência de violações de propriedade de rede combi nando as vantagens do monitoramento de rede para detecção de violações de propriedade com as vantagens de verificação formal para modelar a rede e provar a existência ou ausência de vi olações de propriedade. Um destaque relacionado ao sucesso de tal combinação é o uso de um modelo baseado em gramáticas para capturar os padrões de comunicação existentes na rede. Nossa análise preliminar permite a avaliação de propriedades de rede de alto nível, como "É possível que o componente x envie pacotes HTTP?"e a detecção de violações de propriedade, como regras de encaminhamento conflitantes assim que ocorreram na rede. Como próximas etapas, pretendemos investigar de forma mais profunda como nosso modelo baseado em gra mática pode ser estendido para suportar operadores lógicos temporais e como podemos rastrear o efeitos de violações de propriedade na rede.