Thesis proposals

• TAGUS e-voting System Project
  
• Verification of an i-voting system (cryptographic implementations)
• Extension and deployment of an i-voting system
• Security Resilience to Dynamic Policy Updates
• Controlling Information Flow in Logic Programming
• From Programming Languages to Computational Biology
• Modelling Evolution Ecology using Concurrent Processes
• Modelling Ecosystem Resilience using Concurrent Processes
  
  

  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.

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.

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.

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