Propostas de Temas para Dissertações de Mestrado

Um animador para a linguagem CALF.

ÁREA CIENTÍFICA:

• SECURITY AND PROTECTION
• ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY

PROPONENTES:

Carlos Bacelar Almeida / Manuel Alcino Cunha

DESCRIÇÃO:

A linguagem CALF está a ser desenvolvida no âmbito do projecto europeu CACE. Trata-se de uma linguagem de domínio específico para o desenvolvimento de aplicações criptográficas que concilia, por um lado, abstracções poderosas ao nível do sistema de tipos (e.g. tipos parametrizados por valores) e, por outro, matém presente preocupações relativas à eficiência do código resultante.

O tema proposto é o desenvolvimento de um interpretador e de um mini-compilador para essa linguagem.

• análise sintáctica do código fonte;
• verificação/inferência de tipos;
• codificação de uma "shell" que permita o teste rápido de programas;
• tradutor da representação interna para código C++ (fazendo uso da biblioteca NTL)

Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).

Esta proposta enquadra-se no projecto FP7 CACE.

INFORMAÇÃO ADICIONAL:

No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).

LOCAL:

Dep. Informática

Gerador de Condições de Verificação

ÁREA CIENTÍFICA:

Program Verification LOGICS AND MEANINGS OF PROGRAMS

PROPONENTES:

Jorge Sousa Pinto / Carlos Bacelar Almeida

DESCRIÇÃO:

As abordagens recentes à verificação de programas envolvem duas componentes:

• a utilização de um demonstrador de teoremas (automático ou interactivo);
• uma aplicação designada por "Gerador de Condições de Verificação" (VCGen).

A ideia é que o VCGen transforma um programa (anotado com a respectiva especificação) num conjunto de "obrigações de prova" de primeira ordem que possam ser verificadas pelo demonstrador de teoremas considerado. O VCGen é "correcto" na medida em que, se todas as obrigações de prova se verificarem, existe garantia que o programa se encontra "conforme" a especificação apresentada.

O objectivo deste projecto é o de implementar um VCGen para uma linguagem imperativa "C-like". Pretende-se que esse VCGen seja modular, na medida em que diferentes características da linguagem (e.g. utilização de "arrays"; memória dinâmica; etc.) sejam consideradas incrementalmente.

Esta proposta enquadra-se no projecto FCT Rescue e no projecto FP7 CACE.

INFORMAÇÃO ADICIONAL:

Está aberto um concurso para uma bolsa de investigação do projecto Rescue em que este tema se enquadra. Recomenda-se assim que potenciais interessados submetam a respectiva candidatura (mais informações em http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=11685).

Descrição detalhada: VCGen.pdf

No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).

LOCAL:

Dep. Informática

Computação Multipartida Segura do Logaritmo

ÁREA CIENTÍFICA:

• SECURITY AND PROTECTION
• Distributed Systems

PROPONENTES:

Carlos Bacelar Almeida

DESCRIÇÃO:

Em "Computação Multipartida Segura" (SMC) existem várias partes que pretendem contribuir com dados para uma dada computação (e.g. alguma estatística sobre a agregação desses dados), mas com garantias que a confidencialidade desses dados não é comprometida. Um domínio onde essas técnicas encontram aplicação é o da "Mineração de Dados com Preservação de Privacidade" (PPDM) - nesse caso cada uma das partes contribui com a sua Base de Dados para uma dada técnica de Mineração de Dados, tendo garantias que as outras partes não obtém qualquer conhecimento desses dados (para além do resultado da técnica executada).

O objectivo deste projecto é a codificação de um algoritmo SMC específico: o cálculo do logaritmo. Esse algoritmo é uma peça fundamental numa grande quantidade de técnicas PPDM, e constitui por si só um excelente exemplo combinação de técnicas específicas de SMC (avaliação segura de circuitos; partilha de segredos; etc.). Pretende-se assim utilizar a codificação do algoritmo proposto como pretexto para apresentar o domínio da SMC.

Linguagens de programação a utilizar: C/C++, Java.

INFORMAÇÃO ADICIONAL:

No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).

LOCAL:

Dep. Informática

Correcção perante implementação de referência

ÁREA CIENTÍFICA:

• Program Verification
• LOGICS AND MEANINGS OF PROGRAMS

PROPONENTES:

Jorge Sousa Pinto / Carlos Bacelar Almeida

DESCRIÇÃO:

Para se aferir a correcção de um programa é necessário saber qual a funcionalidade que supostamente ele codifica, i.e. a sua "especificação". Tipicamente, essa especificação é expressa por propriedades lógicas embebidas no próprio código do programa (sob a forma de "anotações"). No entanto, e em domínios específicos como na codificação de técnicas criptográficas, é conveniente apresentar uma "implementação de referência" cujo comportamento é adoptado como modelo.

O objectivo deste projecto consiste em implementar uma metodologia, que tem vindo a ser desenvolvida no grupo de investigação FAST, que permite um certo grau de automatização na verificação da correcção perante implementações de referência.

Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).

Esta proposta enquadra-se no projecto FP7 CACE.

INFORMAÇÃO ADICIONAL:

No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).

LOCAL:

Dep. Informática

Verificação estática de programas CALF/CAO

ÁREA CIENTÍFICA:

• SECURITY AND PROTECTION
• Program Verification

PROPONENTES:

Carlos Bacelar Almeida / Jorge Sousa Pinto

DESCRIÇÃO:

Os ataques a bibliotecas que implementam funcionalidade criptográfica são tipicamente orientados a pequenas falhas na codificação. Assim se explicam os numerosos "vulnerability reports" que nos dão conta de ataques que exploram "stack/heap buffer overflow", etc. Esse facto justifica que no desenho de uma linguagem orientada à codificação de técnicas criptográficas se invista em mecanismos que minimizem os problemas referidos.

Com a "análise estática" de programas pretende-se antecipar potenciais problemas na sua execução por análise do seu código. Um exemplo clássico é a verificação dos limites nos acessos a vectores - nesse caso, pretende-se garantir que esses acessos serão realizados sempre dentro da gama declarada.

Este projecto consiste em desenvolver um módulo de análise estática para a linguagem CALF/CAO --- uma linguagem de domínio específico orientada para a codificação de técnicas criptográficas, desenvolvido no projecto europeu CACE. Esse módulo deverá ser responsável por realizar a análise simbólica do programa e, com o auxílio de um demonstrador automático, fornecer garantias relativas à segurança do programa considerado.

Recomenda-se a utilização de uma linguagem funcional na realização do projecto (e.g. Haskell ou OCaml).

Esta proposta enquadra-se no projecto FP7 CACE.

INFORMAÇÃO ADICIONAL:

No âmbito do projecto CACE está prevista a possibilidade de atribuição de financiamento para suportar a realização desta dissertação em regime de tempo integral (contactar mbb(AT)di(DOT)uminho(DOT)pt).

LOCAL:

Dep. Informática