| Processo: | 11/08947-1 |
| Modalidade de apoio: | Bolsas no Brasil - Pós-Doutorado |
| Data de Início da vigência: | 01 de setembro de 2011 |
| Data de Término da vigência: | 31 de janeiro de 2015 |
| Área de conhecimento: | Ciências Exatas e da Terra - Ciência da Computação - Teoria da Computação |
| Pesquisador responsável: | Arnaldo Vieira Moura |
| Beneficiário: | Rachid Rebiha |
| Instituição Sede: | Instituto de Computação (IC). Universidade Estadual de Campinas (UNICAMP). Campinas , SP, Brasil |
| Bolsa(s) vinculada(s): | 13/04734-9 - Métodos formais algébricos para verificação de programas, BE.EP.PD |
| Assunto(s): | Sistemas de detecção de intrusão |
| Palavra(s)-Chave do Pesquisador: | Análise de intrusão | Análise estática | Detecção de Intrusão | Métodos Formais | Sistema Híbridos | Verificação de Sistemas | Métodos Formais |
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". | |
| Matéria(s) publicada(s) na Agência FAPESP sobre a bolsa: | |
| Mais itensMenos itens | |
| TITULO | |
| Matéria(s) publicada(s) em Outras Mídias ( ): | |
| Mais itensMenos itens | |
| VEICULO: TITULO (DATA) | |
| VEICULO: TITULO (DATA) | |