Titulo Estágio
Geração Automática de Mecanismos de Segurança a Partir de Modelos Formais
Área Tecnológica
Engenharia de Software
Local do Estágio
Departamento de Engenharia Informática da Universidade de Coimbra
Enquadramento
A engenharia de software tem vindo a dar uma importância cada vez mais acentuada à utilização de métodos formais na fase de verificação dos sistemas. Existem presentemente diversos standards que recomendam a aplicação de métodos formais de verificação em domínios aplicacionais específicos (ainda que o teste de software continue a ser a forma mais comum de verificação). A motivação principal para tal consiste no facto do teste de software poder apenas provar a presença de defeitos, mas não provar a ausência dos mesmos. Isto prende-se com o facto de ser habitualmente impraticável testar exaustivamente um sistema, não permitindo provar a ausência de defeitos no software.
Uma das técnicas de verificação formal que tem tido mais sucesso é a verificação de modelos ("model checking"). Esta técnica consiste em determinar automaticamente se um modelo, que representa um sistema, cumpre uma dada especificação. O modelo do sistema é escrito numa linguagem de descrição formal (isto é, sem ambiguidades e clara) e a especificação consiste num conjunto de propriedades às quais se pretende que o sistema obedeça.
Existem diversas ferramentas capazes de analisar exaustivamente os modelos formais e determinar se cumprem a especificação ou, caso contrário, mostrar um contraexemplo no qual as propriedades não se verifiquem. Uma das ferramentas mais conhecidas para verificação de modelos é o Spin, que será a plataforma de base para esta tese de mestrado.
Um dos desafios fundamentais que é necessário resolver consiste em traduzir o modelo formal do sistema em código que possa ser executado no sistema real. Por outras palavras, a verificação de modelos dá, por si, apenas a garantia de que o modelo cumpre a especificação, mas não dá informação acerca do que acontecerá ao código, mesmo que este se baseie inteiramente no modelo formal.
Recentemente, foi desenvolvida no DEI uma ferramenta capaz de traduzir um modelo formal (sujeito a diversas restrições) em código fonte para execução num sistema real. O objectivo deste estágio consiste na extensão dessa mesma ferramenta (disponível em https://code.google.com/p/promnetpp/) com vista a gerar automaticamente mecanismos de segurança para proteger sistemas distribuídos de falhas e intrusões com intenções maliciosas.
Por questões práticas, é necessário restringir o âmbito dos modelos formais possíveis a algo suficientemente concreto, uma vez que o caso geral é demasiado abrangente. Assim, esta tese de mestrado irá focar nos protocolos de comunicação baseados em rondas. Esta classe de protocolo é bastante comum na literatura, sendo portanto de interesse geral, mas suficientemente restrita para ser possível traduzir automaticamente um modelo em código fonte, incluindo os mecanismos de segurança.
Pretende-se que o código gerado automaticamente pela ferramenta a desenvolver seja executável num simulador de protocolos de comunicação já que isto permitirá não só demonstrar a geração automática de código fonte de mecanismos de segurança a partir de modelos formais de sistemas, mas também avaliar o desempenho desse mesmo código fonte.
Objetivo
O objectivo principal do estágio é o desenho e a implementação de uma ferramenta que faça geração automática de mecanismos de segurança para sistemas distribuídos, a partir de modelos formais aceites pelo Spin. Esses modelos serão restringidos ao caso particular dos protocolos de comunicação baseados em rondas. A aplicação a desenvolver fará a extensão da ferramenta disponível em https://code.google.com/p/promnetpp desenvolvida no DEI.
Isto tornará possível colmatar uma das principais falhas apontadas à verificação de modelos, que consiste na dificuldade em provar que o código que é colocado a executar no sistema real corresponde efectivamente ao modelo formal do sistema. Este objectivo será concretizado neste estágio focando o âmbito nos protocolos baseados em rondas, que apesar de serem bastante comuns na literatura possuem uma estrutura clara e bem definida que propicia uma fácil tradução para código fonte.
O código fonte dos mecanismos de segurança, gerado pela ferramenta, deverá poder ser executado num simulador de protocolos já existente, sendo portanto um objectivo do estágio que o código gerado pela ferramenta possa ser directamente colocado num ambiente de simulação.
No final do estágio deverá ser possível demonstrar a execução de protocolos de comunicação, juntamente com os mecanismos de segurança, no simulador. Partindo do modelo original no Spin, que deverá ser possível verificar para um determinado conjunto de configurações do sistema, a ferramenta deverá gerar código que possa ser observado a executar no simulador bem como obter métricas do desempenho do protocolo num ambiente mais próximo da realidade do que a verificação de modelos.
Plano de Trabalhos - Semestre 1
- Estudo do estado da arte e levantamento de requisitos (meses 1 e 2).
A primeira fase consistirá em tomar contacto com a ferramenta de verificação de modelos Spin, bem como a familiarização com o ambiente de desenvolvimento. Isto resultará igualmente numa formulação clara dos objectivos a alcançar por parte do estagiário.
- Desenvolvimento do ambiente de simulação (meses 3 e 4).
Esta tarefa consiste na instalação de uma plataforma de simulação de protocolos de comunicação (a utilização do simulador OMNeT++ é recomendada). Pretende-se que o resultado desta tarefa seja a execução de pelo menos um protocolo de comunicação baseado em rondas, sendo que a simulação de mecanismos de segurança é considerada fundamental nesta tarefa.
- Escrita do relatório intermédio (mês 5).
O estagiário deve apresentar as tarefas efectuadas durante o primeiro semestre e descrever o trabalho a realizar no segundo semestre, escrevendo para esse efeito um relatório intermédio e preparando uma apresentação pública para discussão dos resultados.
Plano de Trabalhos - Semestre 2
- Desenho e implementação da geração automática de código (meses 6 e 7).
Nesta tarefa o estagiário irá implementar a geração do código fonte de mecanismos de segurança a partir de código aceite pelo Spin. A linguagem final deverá ser compatível com o simulador de protocolos usado, sendo que a linguagem aceite pelo Spin é semelhante à linguagem C e consequentemente poderá haver vantagens em que esta seja a linguagem escolhida.
- Integração da ferramenta com o simulador e demonstração (meses 8 e 9).
Esta tarefa consiste na continuação do desenvolvimento da ferramenta de geração automática de código, com vista à integração com o simulador de protocolos de comunicação. Em paralelo, pretende-se demonstrar os conceitos propostos através da geração de mecanismos de segurança para protocolos existentes na literatura. Isto resultará não apenas numa prova de conceito mas também numa avaliação do desempenho do código gerado automaticamente.
- Escrita do relatório final (mês 10).
O estagiário deve apresentar todo o trabalho levado a cabo no decorrer do estágio. Para tal, irá escrever uma tese descrevendo o problema abordado pela tese e a sua solução, bem como preparar a apresentação e discussão pública dos resultados.
Condições
O trabalho irá ser realizado no Departamento de Engenharia Informática da Universidade de Coimbra, sendo que o estagiário irá receber formação adequada na área da verificação de modelos, em particular com o Spin, tendo a oportunidade de participar no módulo acerca deste tópico leccionado no programa doutoral do DEI.
Observações
Dar-se-á preferência a alunos que tenham tido um bom desempenho às disciplinas no âmbito do trabalho proposto (nomeadamente Sistemas Distribuídos, Sistemas Operativos, Integração de Sistemas, e Computação de Alto Desempenho).
Orientador
Raul Barbosa
rbarbosa@dei.uc.pt 📩