VERIFICAÇÃO FORMAL DE PROTOCOLOS DE SEGURANÇA

Resumo

Um dos maiores desafios no desenvolvimento de protocolos de segurança (e.g., TLS, SSH, IKEv2) é garantir a corretude do próprio protocolo, desde o projeto até a implementação. Como forma de vencer este desafio, a verificação formal de protocolos, utilizando métodos formais e matemáticos, vem ganhando força na comunidade de segurança (Chudnov et al. 2018, Li et al. 2018, Kreutz et al. 2019). No entanto, estas ferramentas ainda são pouco conhecidas e utilizadas pela comunidade. Os incidentes envolvendo quebras de protocolos estão ocorrendo com uma frequência cada vez maior, levando a ataques (bem sucedidos) cada vez mais frequentes e vazamentos com impacto social e econômico significativo (Machado et al. 2019). Com este cenário real e crítico em mente, o principal objetivo deste trabalho é contribuir para a difusão do conhecimento e enfatizar a importância da utilização de ferramentas de verificação formal de protocolos de segurança. Com relação a metodologia, num primeiro momento foi realizado um levantamento do estado da arte das ferramentas e técnicas de verificação formal de protocolos de segurança. O resultado desta etapa foi a escolha da ferramenta de verificação automática de protocolos denominada Scyther. Num segundo momento, foram escolhidos os algoritmos a serem formalmente verificados e demonstrados através da ferramenta. O primeiro algoritmo a ser formalmente verificado foi o protocolo de Needham-Schroeder (Needham e Schroeder 1978). O primeiro resultado do trabalho foi um tutorial de apresentação da ferramenta Scyther, em português, e a discussão didática da verificação e correção do protocolo Needham-Schroeder. O tutorial, publicado no Workshop Regional de Segurança (WRSeg 2019) (Jenuario et al. 2019), destaca a importância do conhecimento e da utilização da verificação formal como ferramenta para garantir a corretude de protocolos. Numa segunda etapa do trabalho, a ferramenta Scyther está sendo utilizada na verificação formal de outros protocolos, como os protocolos da SAAS (Fernandes et al. 2019). A expectativa é que a verificação formal de protocolos faça parte crucial e regular do grupo de pesquisa LEA e das disciplinas de segurança de sistemas e dados da instituição.