FAST

Foundations and Applications of Software Technology

Overview


Events

  • MOMPES 2008 - Model-based Methodologies for Pervasive and Embedded Software
  • Interacção 2008 - 3ª Conferência Interacção Pessoa-Máquina
  • XATA 2008 - 6th national conference of XML: Applications and Technologies. Évora, 14,15 February 2008

                        (more...)


News

  • New Project: FAST members participate in EFACEC's InPACT project
  • Co-chair: J. C. Campos was designated co-chair of the programme committee of INTERACÇÃO'08.
  • New Paper: Simulation and Formal Verification of Industrial Systems Controllers
  • New Paper: Formal analysis of interactive systems: opportunities and weaknesses
  • New Paper: Connecting rigorous system analysis to experience centred design

                        (more...)

Propostas de Temas para Dissertações de Mestrado


Extensões de Alto-Nivel Para uma Linguagem de Programação Criptográfica

ÁREA CIENTÍFICA:

  • SECURITY AND PROTECTION
  • ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

PROPONENTES:

Manuel Bernardo Barbosa

DESCRIÇÃO:

No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.

Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.

LOCAL

Dep. Informática


Suporte para raciocínio sobre estruturas algébricas

ÁREA CIENTÍFICA:

  • SECURITY AND PROTECTION
  • ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

PROPONENTES:

Carlos Bacelar Almeida

DESCRIÇÃO:

As estruturas algébricas são um ingrediente fundamental na codificação e na demonstração de segurança das técnicas criptográficas. Raciocinar formalmente sobre elas é assim um aspecto crítico quando está em causa a demonstração de correcção e segurança de software criptográfico.

Neste projecto pretende-se definir uma biblioteca para o Sistema de Prova COQ que incorpore factos e propriedades sobre as estruturas algébricas utilizadas em software criptográfico (grupos, grupos cíclicos, corpos finitos, etc.). Essa bibliotecas terá um papel importante na infra-estrutura de verificação na "toolbox CACE" na medida em que realizará a ponte entre as abstracções disponibilizadas pelas linguagens CAO/CALF, e as demonstrações de correcção/segurança que decorrem das propriedades matemáticas dessas estruturas. Como base de trabalho, pretende-se adoptar o projecto "Math Components" (http://www.msr-inria.inria.fr/Projects/math-components), biblioteca construída sobre uma extensão da linguagem de tácticas do Coq (SSreflect) que incorpora facilidades avançadas para a gestão de scripts de prova e construção de provas por reflexão. Assim, e numa primeira fase, o projecto consistirá em dominar essa extensão e os conceitos associados. Numa segunda fase, o trabalho incidirá sobre a integração da biblioteca com o gerador de obrigações de prova para a linguagem CALF (desenvolvido no âmbito de outras tarefas do projecto CACE), e com a "toolbox" desenvolvida por David Nowak orientada para a demonstração de segurança de técnicas criptográficas.

Esta proposta enquadra-se no projecto FP7 CACE.

LOCAL:

Dep. Informática


Avaliação de Protocolos de Acordo de Chaves com Autenticação Baseada em Segredos Fracos

ÁREA CIENTÍFICA:

  • DATA ENCRYPTION

PROPONENTES:

Manuel Bernardo Barbosa

DESCRIÇÃO:

A execução de um protocolo de acordo de chaves tipicamente exige a existência de uma infra-estrutura de chave-pública para garantir a autenticação dos agentes. Quando isto não é possível, a autenticação é garantida pela pré-distribuição de um segredo partilhado que, muitas vezes é relativamente fraco no que respeita à informação que permanece desconhecida para os atacantes. As palavras-chave são um exemplo destes segredos, bem como as variáveis aleatórias partilhadas geradas a partir da exploração das características dos canais físicos em redes wireless.

No contexto do projecto de investigação Wireless Information Theoretic Security (WITS) pretende-se avaliar a aplicabilidade prática dos protocolos de acordo de chaves com autenticação baseada em segredos fracos já propostos na literatura. Para além da implementação dos protocolos, e dado que as soluções existentes são justificadas de formas distintas e com base em aproximações variadas que incluem a Teoria da Informação e a Segurança Computacional, será necessário estabelecer uma metodologia que permita medir a performance das diferentes soluções para níveis de segurança comparáveis.

LOCAL:

Dep. Informática


Exploração de Algorítmos de Anonimização de Bases de Dados

ÁREA CIENTÍFICA:

  • DATA ENCRYPTION

PROPONENTES:

Manuel Bernardo Barbosa

DESCRIÇÃO:

As técnicas de anonimização de bases de dados são uma tecnologia emergente. O seu objectivo é permitir a divulgação de listagens com informação útil para data mining, mas sujeitas a restrições devido a questões de privacidade. Um exemplo clássico é a divulgação de uma listagem com um conjunto de pacientes que deram entrada num hospital num dado período de tempo, conjuntamente com as condições médicas de que padeciam. A omissão da identidade do paciente, sendo necessária à preservação da sua privacidade, não elimina a possibilidade da sua identificação. De facto, campos como o código-postal, a idade e o sexo podem permitir, só por si, identificar um indivíduo univocamente. São, por este motivo, chamados de quasi-identificadores. No entanto, a eliminação de todos estes quasi-identificadores torna os dados inúteis de um ponto de vista estatístico.

A anonimização consiste em processar os dados, agrupando os registos que tenham valores suficientemente próximos dos quasi-identificadores, de maneira a que um número suficiente de indivíduos em questão se tornem indistinguíveis a um observador, mesmo que este tenha algum conhecimento externo. Pretende-se com este projecto a validação, implementação e benchmarking de um algoritmo desenvolvido no âmbito de um projecto de transferência de tecnologia terminado recentemente.

LOCAL:

Dep. Informática


Reutilização de alietoridade entre diversas primitivas criptográficas

ÁREA CIENTÍFICA:

  • DATA ENCRYPTION

PROPONENTES:

Manuel Bernardo Barbosa

DESCRIÇÃO:

A disponibilidade de bits perfeitamente aleatórios na implementação de algoritmos criptográficos é um dos pressupostos fundamentais à sua segurança. No entanto, a geração de bits aleatórios com qualidade adequada é uma operação custosa, que pode mesmo colocar em causa a viabilidade de implementação de determinados algoritmos criptográficos em plataformas com recursos limitados.

Uma das soluções para este problema, que permite obter ganhos significativos em termos do peso computacional e largura de banda, é amortizar esse custo reutilizando a mesma aleatoriedade em diversas execuções de um mesmo algoritmo. No entanto, este tipo de optimização tem de ser cuidadosamente analisado a nível teórico, para garantir que não implica perdas de segurança.

Pretende-se com este projecto estender os resultados teóricos existentes para o caso em que se reutiliza aleatoriedade entre algoritmos de natureza diferentes, nomeadamente entre algoritmos de cifra e assinatura digital.

LOCAL:

Dep. Informática


Extensões de Alto-Nível Para uma Linguagem de Programação Criptográfica

ÁREA CIENTÍFICA:

  • DATA ENCRYPTION
  • LANGUAGE CONSTRUCTS AND FEATURES

PROPONENTES:

Manuel Bernardo Barbosa

DESCRIÇÃO:

No âmbito do Projecto FP7 CACE (Computer Aided Cryptography Engineering) está a ser desenvolvida a linguagem de programação CAO. Esta linguagem foi desenhada com o objectivo de facilitar a implementação de algoritmos criptográficos numa notação que se aproxime daquela utilizada nas publicações científicas e normas criptográficas, e será suportada por um compilador que automatizará algumas optimizações e contra-medidas de segurança.

Pretende-se com este projecto explorar algumas extensões de alto-nível à linguagem CAO, que permitirão melhorar a usabilidade da linguagem, nomeadamente na implementação de bibliotecas criptográficas genéricas, que poderão ser instanciadas com parametrizações diferentes. Incluem-se nos objectivos deste trabalho a exploração de sistemas de tipos dependentes, funções de ordem superior, etc. A implementação das ferramentas de suporte a esta linguagem deverão ser realizadas na linguagem OCaml.

r2 - 29 Sep 2009 - 16:49:44 - ManuelBernardoBarbosa
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
Syndicate this site RSSATOM