Métodos Formais Algébricos para Gerção de Invariantes.

Resumo

Invariante é uma propriedade sempre vericada a cada execução de um sistema, em um local especíco. E bem sabido que a ecácia de métodos de vericação formal de programas, sistemas embarcados, ou sistemas híbridos, depende da geração automática e eciente de invariantes precisas. Esta proposta visa, primordialmente, investigar a redução de problemas de geração de invariantes para problemas algébricos lineares. Logrando este intuito, poderíamos ultrapassar as deciências dos mais modernos métodos de geração de invariante hoje conhecidos, permitindo, assim, a geração eciente de invariantes para programas, sistemas híbridos e embarcados não lineares. Os algoritmos algébricos que temos em vista apresentam complexidades signicativamente inferiores aqueles que suportam as demais abordagens usadas hoje. Usando esses novos métodos, poderíamos fundamentar técnicas inéditas e ecientes que venham a formar o núcleo de novos algoritmos para a automação de processos dedutivos, e de novos algoritmos para vericação de modelos complexos. Em particular, propomo-nos investigar e desenvolver métodos pioneiros que automaticamente gerem bases de invariantes expressas por séries de potências multi-variáveis e por funções transcendentais. Essa contribuição seria bastante signicativa, uma vez que fundamentaria novos métodos para vericação automática de propriedades de softwares, e que seriam capazes de lidar com modelos atuais de sistemas híbridos críticos, ou de sistemas embarcados. Investigações iniciais nesse sentido já se mostraram bastante promissoras e já somos capazes de lidar com sistemas complexos que vão além dos limites alcançados hoje por outros métodos. Sob outro ponto de vista, e de posse desses novos métodos, pretendemos ampliar o domínio de aplicações da geração de invariantes para a area de segurança. Mais precisamente, gostaríamos de desenvolver uma plataforma extensível e que permitisse detectar os ataques mais virulentos de intrusões. Tendo como base invariantes pré-computadas, geradas automaticamente a partir do código de intrusos selecionados, estas seriam usadas como assinaturas semânticas, permitindo a detecção de intrusos, mesmo que estes se valessem das transformações hoje mais difíceis de detectar, tais como técnicas de "obfuscamento".