Thesis proposals
TAGUS
e-voting System Project
Promoters
Ana
Almeida Matos and Jan
Cederquist
The TAGUS
e-voting system Project aims to create an
e-voting solution that is adequate, security and
usability-wise,
for academic environments such as Universities
or other similar organizations.
Our team is composed of a group of
master students that are contributing to
different components of the system, its
verification and deployment.
Research
in cryptography has provided a range of tools for
implementing electronic voting systems, that enable
people to vote remotely, e.g. through the Internet,
while providing the required security guarantees
such as anonymous communication, public
verifiability and everlasting privacy. Different
voting contexts have different security
requirements, and suitable voting protocols place
trust on different elements of a system. Fernando Marques has chosen
and adapted an e-voting protocol having our
particular requirements in mind, and has
implemented a functional prototype of the
system.
Invariably,
in practice, protocol security relies on that
certain software components are correctly
implemented, and are free from coding errors that
introduce undesirable behavior in the form of
security vulnerabilities. Such vulnerabilities can
ultimately be exploited by attackers in order to
hack an election. Currently, André Ribeiro and João
Lopes are working on the verification of security
properties of different components of the system.
The
next two tasks, which we describe below, consist of
verifying the cryptographic implementations that are
in use in the client side of the system, the
extension of the system with specific security and
usability features, and the deployment of the system
to be used in a real election. An important part of
all tasks is to present the results to the
community, in order to increase awareness and trust
over the security guarantees that are provided.
Extension and
deployment of an i-voting system
Advisors
Ana
Almeida Matos and Jan
Cederquist
Description and objectives
The aim of this thesis is to extend and deploy an
existing implementation of an i-voting (internet
voting) system that is based on the H-Belenios
protocol. This will include incorporating additional
relevant security features in the H-Belenios procol
(receipt freeness, threshold for key-sharing),
presenting the system to the academic community, and
organising an election that uses it.
Outline
1- Study of the system and identification of its
current most important limitations.
2- Study of the state of the art of existing solutions
for identified limitations.
3- Design and implementation of the extension.
4- Presentation of the system to the academic
community.
5- Organization of an election.
Expected result
This will be an important phase of a larger project,
which consists of the development of a secure and
robust i-voting system to be presented to the academic
community with the purpose of integrating it in Fenix.
Requirements
Successful attendance of a masters-level course in
security, verification or quality of software.
Verification
of an i-voting system (cryptographic
implementations)
Advisors
Ana
Almeida Matos and Jan
Cederquist
Description and objectives
The aim of this thesis is to contribute to the
verification of an implementation of an i-voting
(internet voting) system that is based on a version of
the Helios protocol. This will require identifying the
relevant security properties that the implementation
must fulfill, as well as the appropriate verification
techniques that can be applied to that end. The focus
will be on providing strong guarantees of correctness
of aspects of an implementation of the client, and in
particular of the implementation and usage of
cryptographic primitives.
Outline
1- Study of the state of the art in verification of
cryptographic primitives.
2- Study of an existing tool framework for
verification of JavaScript using separation logic.
3- Application of the tool framework to the client of
the system.
4- Presentation of the results.
Expected result
Verification of crucial components of an i-voting
system, in order to guarantee that the implementation
behaves as intended from a security standpoint. This
will be an important phase of a larger project, which
consists of the development of a secure and robust
i-voting system to be presented to the academic
community with the purpose of integrating it in Fenix.
Requirements
Successful attendance of a masters-level course in
security, verification or quality of software.
Automatic Synthesis of Information
Flow Models for Web APIs: An Application to the DOM
API
Advisors
Ana
Almeida Matos , Jan
Cederquist and José
Fragoso Santos
Description
In recent years, a lot of work has been dedicated to
the study of information flow security in Web
applications with the double aim of preventing
classified user information from falling into the
hands of unauthorized servers and preventing high
integrity information from being updated by untrusted
scripts. JavaScript is the current lingua franca
for implementing client-side Web applications. Hence,
the great majority of the proposed mechanisms for
securing client-side Web applications target
JavaScript-like languages which capture different
aspects of the real language.
Client-side JavaScript
programs interact with the Web page in which they are
included as well as with their runtime environment via
a large number of external APIs provided by the
browser. Although these APIs are not part of the
language specification, any realistic mechanism for
securing JavaScript programs must take them into
account (as malicious programs can encode illegal
information flows through the use of Web APIs).
However, the continuous emergence and heterogeneity of
different APIs renders the problem of specifying
information flow models for Web APIs extremely
challenging. Concretely, there are hundreds of APIs
available to JavaScript programs that execute in the
browser and this number is continuously growing.
Hence, the task of developing a sound information flow
models for each one of these APIs is a huge project
that begs to be automated.
Objectives
This thesis aims at the design of a mechanism for
automating the generation of information flow models
for Web APIs.
Outline
The student will be expected to design and implement:
1. a language for formally describing the behavior of
APIs;
2. a language for specifying information flow models
for APIs;
3. a sound inference mechanism that given the
specification of an API generates its corresponding
information flow model.
In order to illustrate the
applicability of the proposed inference mechanism, the
student is expected to formalize a fragment of the
Core DOM Level 1 API using the language designed for
that purpose (1). Then, one should be able to apply
the inference mechanism (3) to the formalized Core DOM
Level 1 API in order to generate the corresponding
information flow models (2). These models are then to
be integrated in a state-of-the-art information flow
inlining compiler for JavaScript.
References
• D. Hedin, A. Birgisson, L. Bello, and A. Sabelfeld.
JSFlow: Tracking Information Flow in JavaScript and
its APIs. SEC 2014
• D. Hedin and A. Sabelfeld. Information-Flow Security
for a Core of JavaScript. CSF 2012
• A. Russo and A. Sabelfeld. Dynamic vs. Static
Flow-Sensitive Security Analysis. CSF 2010
• S. Hunt and D. Sands. On Flow-sensitive Security
Types. CSF2006
• A. Chudnov and D. Naumann. Information Flow Monitor
Inlining. CSF 2010
• José Fragoso Santos. Enforcing Secure Information
Flow in Client-Side Web Applications. PhD Thesis
Generating Efficient
JavaScript Code - A type-directed transformation
from TypeScript to asm.js
Advisors
Ana
Almeida Matos, Jan
Cederquist and José
Fragoso Santos
Description
Nowadays, Web applications are increasingly more
ubiquitous. They run in all kinds of devices, from
cell phones to tablets among many others. While it is
true that the processing power of these devices has
been continuously growing, it is also true that it is
much smaller than that of traditional PCs or laptops.
This raises the challenge of developing more
performant JavaScript code capable of being executed
in devices with low processing power without
compromising the user experience.
The dynamic nature of
JavaScript - the lingua franca for
implementing client-side Web applications - makes it a
very difficult language to compile. Hence, JavaScript
programs are typically much less performant than
programs implemented in strongly typed imperative
languages such as C or C++. However, a very restricted
low-level subset of JavaScript called asm.js has been
shown to be as performant as C and C++ in a broad
variety of benchmarks. This begs the question of how
to generate asm.js programs from arbitrary JavaScript
programs. In other words, is it possible to design a
mechanism to project arbitrary JavaScript programs
into asm.js in an efficient way?
The dynamicity of JavaScript
programs will definitely compromise the efficiency of
a general translation mechanism from JavaScript to
asm.js. However, one may try to overcome such
difficulties by the use of type information regarding
the programs to compile. In fact, the TypeScript
programming language is an extension of JavaScript
that adds optional types to JavaScript code. The main
idea of this language is to harness the flexibility of
real JavaScript, while at the same time providing some
of the advantages otherwise reserved to statically
typed languages, such as type directed compilation.
Objectives
This thesis aims at the design of an efficient and
proven correct type-directed transformation from
TypeScript to asm.js. The idea is to take advantage of
type information to improve the performance of the
original code.
Outline
Concretely, the student will be expected to:
1. Formalize a fragment of TypeScript that includes
its main features;
2. Formalize a fragment of asm.js that includes its
main features;
3. Design a translation of the formalized fragment of
TypeScript to the formalized fragment
of asm.js;
4. Prove the translation to be correct.
References
• Greg Morrisett. Compiling with Types. PhD Thesis
(CMU)
• Microsoft. TypeScript Language Specification.
• Mozilla. asm.js Specification.
• A. Rastogi, N. Swamy, C. Fournet, B. Bierman, P.
Vekris. Safe and Efficient Gradual Typing for
TypeScript. POPL 2015
• A. Feldthaus and A. Moller. Checking Correctness of
TypeScript Interfaces for JavaScript Libraries. OOPSLA
2014
• S. Jensen, A. Moller, P. Thiemann. Type Analysis for
JavaScript. SAS 2009
• P. Thiemann. Towards a Type System for Analysing
JavaScript Programs. ESOP2005
Security Resilience
to Dynamic Policy Updates
(Sorry -- in Portuguese. Please contact us for
information in English)
Advisors
Ana
Almeida Matos, Jan
Cederquist
Description
Este trabalho incide sobre o problema da segurança de
fluxos de informação, recorrendo a técnicas de análise
de linguagens de programação. Estamos em particular
interessados em estudar formas de lidar com modelos em
que as políticas de fluxo em vigor podem mudar durante
a execução de programas.
Objectives
Desenvolver um mecanismo de controlo de fluxos de
informação que é resiliente a mudanças dinâmicas das
políticas de fluxos em vigor.
Os objectivos aqui definidos poderão ser adaptados
aos interesses do aluno, conforme o desenrolar dos
seus estudos nesta área.
Outline
1) Estudo das soluções existentes para o problema
proposto.
2) Estudo de técnicas de extracção estática de fluxos
de informação inseguros em programas
3) Desenvolvimento de uma aplicação das técnicas em 2)
ao contexto em que as políticas de fluxo em vigor
podem mudar durante a execução de programas.
Expected
result
Desenvolvimento de um protótipo. Participação na
elaboração de um artigo científico.
References
• A. Sabelfeld and A. C.
Myers.
Language-Based Information-Flow Security. IEEE
Journal on Selected Areas in Communications 2006
Requirements
Frequência de uma cadeira de mestrado em segurança,
verificação ou qualidade de software.
Controlling
Information Flow in Logic Programming
Advisors
Ana
Almeida Matos, Jan
Cederquist
Description
Information flow security regards the study of how
information that is classified with different levels
of confidentiality or integrity is transferred between
computation resources throughout the execution of a
program. Information flow analyses have been
extensively studied for a variety of programming
language paradigms, ranging through imperative,
functional and even web programming languages.
However, the subject of studying information flow in
logic programming languages is just emerging.
Objectives
The aim of this project is to propose information flow
control techniques for programs written in a logic
programming language such as Prolog.
Outline
The student will be expected to:
1. survey existing program analysis techniques for
Prolog programs;
2. collaborate in the proposal of a mechanism for
controlling information flow in Prolog programs;
3. participate in the formalization and proof of
soundness of the proposal
References
• A. Sabelfeld and A. C. Myers.
Language-Based Information-Flow Security. IEEE
Journal on Selected Areas in Communications 2006
• A. Yaacoub. Towards an information
flow in logic programming. IJCSI 2012
Requirements
Successful attendance of a
masters-level course in security, verification or
quality of software.
From Programming Languages
to Computational Biology
(Sorry -- in Portuguese. Please contact us for
information in English)
Aims
Nas últimas décadas
verificou-se uma explosão em investigação com o fim de
compreender os mecanismos que intervêm na resiliência
de sistemas, ao longo de diferentes escalas
temporais. O objectivo é o de aumentar o
conhecimento sobre formas de fortalecer a capacidade
de lidar com stress causado por mudanças ambientais,
de lidar com crises e eventos inesperados, e em última
análise de identificar soluções para os humanos
viverem dentro dos limites do Planeta.
Partindo da Álgebra de Processos, uma área fundamental
em Linguagens de Programação e Sistemas Concorrentes,
pretende-se com este projeto contribuir para a
compreensão de problemas que ultrapassam os horizontes
clássicos da ciência de computadores, nomeadamente
problemas nucleares em Resiliência e Ecologia Evolutiva,
mais concretamente:
- Oferecer um novo ângulo no estudo da
emergência (e extinção) de espécies e da
biodiversidade resultante, da linguagem e dos
mecanismos linguísticos subjacentes, e da cooperação.
- Contribuir para a
investigação na área da modelação de sistemas
complexos e, mais genericamente, da Computação
Científica.
De seguida argumenta-se a
favor do papel crucial que a investigação em
Linguagens de Programação pode ter no estudo destes
desafios prementes e de interesse crucial para a vida
humana no planeta. As suas propostas concretas (Modelling
Evolution Ecology using Concurrent Processes, Modelling
Ecosystem Resilience using Concurrent Processes)
são de natureza exploratório e podem ser adaptados aos
interesses do aluno, conforme o desenrolar dos seus
estudos nesta área.
Motivation
A par da mudança de foco nas Ciências da Vida da
estrutura dos constituintes de sistemas biológicos a
favor da sua funcionalidade, tem-se verificado o
crescimento da importância de formas de abstrair e
modelar computacionalmente a evolução dinâmica dos
sistemas em questão.
Uma área das Ciências da Vida que depende fortemente da
modelação computacional é a Ecologia das Populações, uma
sub-área da Ecologia que se dedica ao estudo de
dinâmicas populacionais e sua interacção com o
ambiente. O seu principal objectivo é compreender
como é que populações de espécies se desenvolvem no
tempo e espaço, e em particular as interdependências de
relevo entre as suas características e as do ambiente em
que vivem. Nesta área, é difícil ou mesmo
impossível conduzir experiências no mundo real, dados os
constrangimentos de escalas de tempo e espaço
comportáveis, de ética, e complexidade e dimensão das
variáveis e dados que são tratados.
A modelação computacional de dinâmicas de populações e
comunidades permite formaliza-las de forma rigorosa,
sendo os modelos resultantes utilizados para analisar a
forma como indivíduos, populações e comunidades
respondem a alterações ambientais, bem como a evolução
de atributos comportamentais, entre outros.
Através da modelação abstracta é possível isolar e
combinar diversas componentes de um ecossistema, e
subsequentemente, através de simulações, automatizar a
análise da progressão dos modelos de forma a conduzir
experiências que não são praticáveis em sistemas reais.
Uma vertente importante da modelação de dinâmicas de
populações baseia-se na definição explícita de
populações como colecções discretas de indivíduos (ou
grupos de indivíduos) que habitam determinados
ambientes, dos quais emerge o comportamento macroscópico
das população que compõem. Numa perspectiva
computacional, o conceito de indivíduo pode ser
identificado com o de processo: uma entidade
computacional, de execução concorrente, e cujo
comportamento se descreve com base na composição e
interacção com outros processos e respectivo contexto
por forma a formar um sistema ecológico completo.
Esta observação sublinha uma relação existente entre o
estudo de sistemas ecológicos de populações, na
Ecologia, e o estudo de sistemas de processos
concorrentes, na Ciência de Computadores.
A Álgebra de Processos é uma sub-área das Linguagens de
Programação que aborda o estudo de sistemas concorrentes
através da sua abstracção com recurso a linguagens
simbólicas, conhecidas por cálculos de processos, que
representam os aspectos essenciais da comunicação e
partilha de informação entre processos
concorrentes. Um processo, ou agente, consiste
assim numa entidade computacional ao qual se associam
diferentes capacidades, estados e atributos, e sobre o
qual se estabelece uma teoria de comportamento.
Através de regras que estabelecem as formas de
comunicação e computação de processos, é possível
analisar, formular e verificar propriedades acerca do
comportamento de colecções de processos.
Tendo sido originalmente concebidos com o fim de estudar
a comunicação e concorrência entre processos
informáticos, os cálculos de processos têm vindo
progressivamente a ser utilizados na biologia
computacional para modelar entidades biológicas que
abrangem organização de moléculas e células, o
funcionamento do cérebro, ou populações de
espécies. De facto, os cálculos de processos
comportam precisamente a possibilidade de descrever e
estudar o comportamentos de sistemas biológicos e
ecológicos em geral que assentam na interacção entre
componentes com comportamento concorrente e interactivo.
Características tais como tempo, probabilidade, e
comportamento estocástico, que se encontram
extensivamente estudados dentro do contexto dos cálculos
de processos, podem ser explorados no contexto dos
sistemas biológicos modelados, enquanto que ferramentas
de análise já existentes podem ser usadas no estudo do
comportamento que estes sistemas exibem. Não é por
isso de estranhar que a investigação das aplicações da
teoria comportamental da Álgebra de Processos na
modelação de Populações se encontre em expansão.
Modelling
Evolution Ecology using Concurrent Processes
Advisors
Ana
Almeida Matos, Jan
Cederquist
Description
A Ecologia Evolutiva estuda os mecanismos subjacentes
ao fenómeno da evolução numa perspectiva ecológica.
Por outras palavras, debruça-se sobre os princípios
segundo os quais as interacções dentro de populações e
entre elas e o seu ambiente moldam as características
de espécies ao longo de selecção e adaptação.
Do ponto de vista da modelação de dinâmicas de
populações, com o fim de poder caracterizar mudanças
em atributos de espécies ao longo das dimensões tempo
e espaço, é necessário introduzir no modelo uma
representação dos atributos em estudo. Na
representação de indivíduo com base num processo, esse
atributo pode ser qualquer objecto representável
computacionalmente.
Objectives
Abordar experiências de modelação que endereçam os
problemas em Ecologia Evolutiva, como por exemplo:
- Evolução de espécies: Que
factores afectam os mecanismos que dão origem à
biodiversidade observável em ecossistemas e
comunidades?
A ideia base será a de modelar a noção de espécie
como um conjunto de indivíduos, cada um deles
contendo uma representação dos seus traços
genéticos, que manifestam um determinado grau de
semelhança genética entre si. O ciclo de vida e
comportamento em geral destes indivíduos é
programável usando cálculos de processos, podendo
incluir reprodução e morte. A criação dinâmica de
novos indivíduos pode incorporar o fenómeno da
mutação genética, bem como o da reprodução sexuada,
como uma forma de interacção entre processos que
permite originar um novo indivíduo com traços
genéticos resultantes da combinação dos dos seus
progenitores.
- Evolução da linguagem: Como
se processa o desenvolvimento de uma linguagem
dentro de uma comunidade de indivíduos?
A ideia base será a de associar a cada indivíduo uma
representação do seu conhecimento de uma língua
(vocabulário, regras gramaticais), bem como da
capacidade de aprendizagem, através da codificação
de um algoritmo de aprendizagem automática.
Associando a cada comunicação entre processos um
input a ser tratado.
- Evolução de relações --
cooperação: Que factores influenciam a adopção de
estratégias de cooperação por indivíduos de uma
população?
A ideia base será a de utilizar o conceito de
política (policy) da Álgebra de Processos para
representar uma estratégia comportamental, neste
caso um mecanismos de decisão, a ser associado a
cada indivíduo um atributo dinâmico que representa
uma estratégia comportamental. A observação do
comportamento e sucesso de outros indivíduos pode
então ser representada através da comunicação
assíncrona entre processos.
Requirements
Frequência de uma disciplina de
mestrado em linguagens de programação, verificação ou
simulação.
Modelling
Ecosystem Resilience using Concurrent Processes
Advisors
Ana
Almeida Matos, Jan
Cederquist
Motivation
Resiliência de um sistema é a capacidade de um
sistema lidar com uma disrupção, mantendo-se ou
recuperando o estado de equilíbrio em que se
encontrava. Este conceito encontra-se interligado ao
de auto-regulação, uma vez que a capacidade de
auto-regulação contribui para a resiliência de um
sistema. Um dos mais conhecidos modelos que
incorporam os princípios da auto-regulação é o
Daisyworld, um modelo planetário simples que permite
modelar sistemas de feedback entre populações e o
seu ambiente.
Uma variedade de abstracções matemáticas têm sido
propostas para representar este modelo, sendo a
distribuição espacial bidimensional tipicamente
organizada numa matriz. Enquanto que por um lado a
simplicidade deste modelo é atractiva, ele apresenta
algumas reconhecidas limitações na representação de
estruturas na relação de feedback estabelecidas
entre os indivíduos (neste caso as margaridas) e o
ambiente.
Neste contexto, os cálculos de processos
distribuídos, que permitem descrever diferentes
estruturas de localização, oferecem outros formas de
expressividade na organização de localizações,
incluindo o conceito de membrana, e de hierarquias
de localizações encaixadas, que permitem estudar
auto-regulação de sistemas de indivíduos que se
organizam espacialmente em diferentes níveis.
Objectives
Investigar a modelação de sistemas de populações e
seu ambiente, análogos ao Daisyworld, com base em
cálculos de processos distribuídos com noção
estruturada de localização. Esta ideia afigura-se
como um ponto de partida interessante para estudar
quais os factores que afectam a capacidade de
auto-regulação de sistemas com uma variedade de
estruturas de feedback que divergem em diferentes
aspectos das premissas do Daisyworld.
Requirements
Frequência de uma disciplina
de mestrado em linguagens de programação,
verificação ou simulação.
|